1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
2 Author: Walther Neuper 101001
3 (c) copyright due to license terms.
5 Isac's tests are organised parallel to sources:
6 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
8 ~~/test/Tools/isac/ADDTESTS
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
12 section \<open>Notes on running tests\<close>
13 subsection \<open>Switch between running tests and updating code\<close>
15 Isac encapsulates code as much as possible in structures without open.
16 This policy conflicts with those tests, which go into functions to details
17 not declared in the signatures.
19 In order to maintain these tests without changes, this has to be done before running tests:
20 (1) Extend signatures for tests by
21 ~~$ ./xcoding-to-test.sh
22 ~~$ ./zcoding-to-test.sh # --"-- + go back to Test_Isac.thy
23 Running Test_Isac.thy opens all structures, see code after "begin" below.
24 (2) Clean signatures for coding
25 ~~$ ./xtest-to-coding.sh
26 ~~$ ./ztest-to-coding.sh # --"-- + go back to coding (!update thy!)
28 ********************* don't forget (2) BEFORE pushing to repository ****************************
30 subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
32 Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
33 if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
34 This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
35 A model is in the repository at ~~/etc/preferences.
36 These preferences have drawbacks, however:
37 * they claim more memory such that Isabelle instances canNOT run in parallel.
38 * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
40 So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
41 From time to time full testing in Test_Isac.thy is recommended. For that purpose
42 * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
44 ********************* don't forget to re-set defaults BEFORE updating code *********************
46 Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
47 ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
50 section \<open>Run the tests\<close>
52 * say "OK" to the popup asking for theories to be loaded
53 * watch the <Theories> window for errors in the "imports" below
56 theory Test_Isac_Short
57 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
58 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
59 "ADDTESTS/accumulate-val/Thy_All"
61 "ADDTESTS/test-depend/Build_Test"
64 "ADDTESTS/course/phst11/T1_Basics"
65 "ADDTESTS/course/phst11/T2_Rewriting"
66 "ADDTESTS/course/phst11/T3_MathEngine"
67 "ADDTESTS/file-depend/BuildC_Test"
68 "ADDTESTS/session-get_theory/Foo"
69 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
70 ADDTESTS/------------------------------------------- see end of tests *)
71 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
72 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
73 "~~/test/Pure/Isar/Test_Parse_Term"
74 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
75 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
76 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
77 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
78 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
79 (*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
80 (*"~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*)
81 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
85 ML \<open>open ML_System\<close>
87 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
88 (* these vvv test, if funs are intermediately opened in structure
89 in case of errors here consider ~~/xtest-to-coding.sh *)
92 open Test_Code; CalcTreeTEST;
93 open LItool; arguments_from_model;
100 open Error_Fill_Pattern;
103 open Rtools; trtas2str;
104 open Chead; pt_extract;
105 open Generate; (* NONE *)
106 open Ctree; append_problem;
112 open Auto_Prog; rule2stac;
114 open Specify; show_ptyps;
116 open Applicable; mk_set;
120 open Solve; (* NONE *)
122 open Stool; (* NONE *)
123 open ContextC; transfer_asms_from_to;
124 open Tactic; (* NONE *)
125 open Model; (* NONE *)
131 open Rule_Set; Sequence;
138 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
142 "~~~~~ fun xxx , args:"; val () = ();
143 "~~~~~ and xxx , args:"; val () = ();
144 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
145 (*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
147 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
164 KEStore_Elems.set_ref_thy @{theory};
165 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
168 (*---------------------- check test file by testfile -------------------------------------------
169 ---------------------- check test file by testfile -------------------------------------------*)
170 section \<open>trials with Isabelle's functions\<close>
171 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
172 ML_file "~~/test/Pure/General/alist.ML"
173 ML_file "~~/test/Pure/General/basics.ML"
174 ML_file "~~/test/Pure/General/scan.ML"
175 ML_file "~~/test/Pure/PIDE/xml.ML"
176 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
178 section \<open>test ML Code of isac\<close>
179 subsection \<open>basic code first\<close>
180 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
181 ML_file "BaseDefinitions/libraryC.sml"
182 ML_file "BaseDefinitions/rule-def.sml"
183 ML_file "BaseDefinitions/exec-def.sml"
184 ML_file "BaseDefinitions/rewrite-order.sml"
185 ML_file "BaseDefinitions/theoryC.sml"
186 ML_file "BaseDefinitions/rule.sml"
187 ML_file "BaseDefinitions/thmC-def.sml"
188 ML_file "BaseDefinitions/error-fill-def.sml"
189 ML_file "BaseDefinitions/rule-set.sml"
190 ML_file "BaseDefinitions/check-unique.sml"
195 (* Title: "BaseDefinitions/check-unique.sml"
196 Author: Walther Neuper
197 (c) due to copyright terms
200 "-----------------------------------------------------------------------------------------------";
201 "table of contents -----------------------------------------------------------------------------";
202 "-----------------------------------------------------------------------------------------------";
203 "----------- re-build check_pblguh_unique with high order funs ---------------------------------";
204 "-----------------------------------------------------------------------------------------------";
205 "-----------------------------------------------------------------------------------------------";
206 "-----------------------------------------------------------------------------------------------";
209 "----------- re-build check_pblguh_unique with high order funs ---------------------------------";
210 "----------- re-build check_pblguh_unique with high order funs ---------------------------------";
211 "----------- re-build check_pblguh_unique with high order funs ---------------------------------";
212 (*------- auxiliary format for fn*)
213 fun pbl_select_guh pbt =
215 val {guh, ...} = (**)(pbt: pbt)(** )(pbt: met)( **)
217 pbl_select_guh: pbt -> guh;(**)
219 fun met_select_guh pbt =
221 val {guh, ...} = (pbt: met)
223 met_select_guh: met -> guh;(**)
225 (*------- hint: build higher order functions be replacing the selector by a variable argument *)
227 fun collect select_guh pbls =
229 fun node coll (Store.Ptyp (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
230 | node _ _ = raise ERROR "collect_guhs: too general Store.Ptyp"
231 and nodes coll [] = coll
232 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
233 in nodes [] pbls end;
238 collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
239 collect pbl_select_guh: pbt Store.ptyp list -> guh list;
240 collect met_select_guh: met Store.ptyp list -> guh list;
242 fun message select store guh =
243 if member op = (select store) guh
244 then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
245 "use \"sort_guhs()\" for a list of guhs;\n" ^
246 "consider setting \"Check_Unique.on := false\"")
249 message: ('a -> guh list ) -> 'a -> guh -> unit;
250 (message (collect pbl_select_guh)): pbt Store.ptyp list -> guh -> unit;
251 (message (collect met_select_guh)): met Store.ptyp list -> guh -> unit;
253 (Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
254 (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh)): met Store.ptyp list -> guh list;
256 val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh));
257 check_pblguh_unique: pbt Store.ptyp list -> guh -> unit
259 val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh));
260 check_metguh_unique: met Store.ptyp list -> guh -> unit
269 ML_file "BaseDefinitions/calcelems.sml"
270 ML_file "BaseDefinitions/termC.sml"
271 ML_file "BaseDefinitions/contextC.sml"
272 ML_file "BaseDefinitions/environment.sml"
273 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
274 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
275 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
276 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
277 ML_file "ProgLang/listC.sml"
278 ML_file "ProgLang/prog_expr.sml"
279 ML_file "ProgLang/program.sml"
280 ML_file "ProgLang/prog_tac.sml"
281 ML_file "ProgLang/tactical.sml"
282 ML_file "ProgLang/auto_prog.sml"
283 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
284 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
286 subsection \<open>basic functionality on simple example first\<close>
287 ML_file "Minisubpbl/000-comments.sml"
288 ML_file "Minisubpbl/100-init-rootpbl.sml"
289 ML_file "Minisubpbl/150-add-given.sml"
290 ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
291 ML_file "Minisubpbl/200-start-method.sml"
292 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
293 ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
294 ML_file "Minisubpbl/300-init-subpbl.sml"
295 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
296 ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
297 ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
298 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
299 ML_file "Minisubpbl/500-met-sub-to-root.sml"
300 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
301 ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
302 ML_file "Minisubpbl/600-postcond.sml"
303 ML_file "Minisubpbl/700-interSteps.sml"
304 ML_file "Minisubpbl/710-interSteps-short.sml"
305 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
306 ML_file "Minisubpbl/790-complete.sml"
307 ML_file "Minisubpbl/800-append-on-Frm.sml"
309 subsection \<open>further functionality alongside batch build sequence\<close>
310 ML_file "MathEngBasic/thmC.sml"
311 ML_file "MathEngBasic/rewrite.sml"
312 ML_file "MathEngBasic/model.sml"
313 ML_file "MathEngBasic/mstools.sml"
314 ML_file "MathEngBasic/specification-elems.sml"
315 ML_file "MathEngBasic/tactic.sml"
316 ML_file "MathEngBasic/ctree.sml"
317 ML_file "MathEngBasic/calculation.sml"
319 ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *)
320 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
321 ML_file "Specify/generate.sml"
322 ML_file "Specify/calchead.sml"
323 ML_file "Specify/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
324 ML_file "Specify/step-specify.sml"
325 ML_file "Specify/specify.sml"
327 ML_file "Interpret/istate.sml"
328 ML_file "Interpret/sub-problem.sml"
329 ML_file "Interpret/rewtools.sml"
330 ML_file "Interpret/error-fill-pattern.sml"
331 ML_file "Interpret/li-tool.sml"
332 ML_file "Interpret/lucas-interpreter.sml"
333 ML_file "Interpret/step-solve.sml"
335 ML_file "MathEngine/fetch-tactics.sml"
336 ML_file "MathEngine/solve.sml"
337 ML_file "MathEngine/step.sml"
338 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
339 ML_file "MathEngine/messages.sml"
340 ML_file "MathEngine/states.sml"
342 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
343 ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
344 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
345 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
346 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
347 ML_file "BridgeLibisabelle/interface.sml"
348 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
349 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
351 ML_file "Knowledge/delete.sml"
352 ML_file "Knowledge/descript.sml"
353 ML_file "Knowledge/simplify.sml"
354 ML_file "Knowledge/poly.sml"
355 ML_file "Knowledge/gcd_poly_ml.sml"
356 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
357 (*ML_file "Knowledge/rational.sml" Test_Isac_Short*)
358 ML_file "Knowledge/equation.sml"
359 ML_file "Knowledge/root.sml"
360 ML_file "Knowledge/lineq.sml"
361 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
362 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
363 ML_file "Knowledge/rootrat.sml"
364 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
365 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
366 ML_file "Knowledge/polyeq-1.sml"
367 (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
368 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
369 ML_file "Knowledge/calculus.sml"
370 ML_file "Knowledge/trig.sml"
371 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
372 ML_file "Knowledge/diff.sml"
373 ML_file "Knowledge/integrate.sml"
374 ML_file "Knowledge/eqsystem.sml"
375 ML_file "Knowledge/test.sml"
376 ML_file "Knowledge/polyminus.sml"
377 ML_file "Knowledge/vect.sml"
378 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
379 ML_file "Knowledge/biegelinie-1.sml"
380 (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
381 (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)
382 (*ML_file "Knowledge/biegelinie-4.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
383 ML_file "Knowledge/algein.sml"
384 ML_file "Knowledge/diophanteq.sml"
385 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
386 ML_file "Knowledge/inssort.sml"
387 ML_file "Knowledge/isac.sml"
388 ML_file "Knowledge/build_thydata.sml"
390 ML_file "Test_Code/test-code.sml"
392 section \<open>further tests additional to src/.. files\<close>
393 ML_file "BridgeLibisabelle/use-cases.sml"
394 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
395 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
397 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
398 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
399 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
413 section \<open>history of tests\<close>
415 Systematic regression tests have been introduced to isac development in 2003.
416 Sanity of the regression tests suffers from updates following Isabelle development,
417 which mostly exceeded the resources available in isac's development.
419 The survey below shall support to efficiently use the tests for isac
420 on different Isabelle versions. Conclusion in most cases will be:
422 !!! Use most recent tests or go back to the old notebook
423 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
427 subsection \<open>isac on Isabelle2017\<close>
428 subsubsection \<open>Summary of development\<close>
430 * Add further signatures, separate structures and cleanup respective files.
431 * Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
432 * Clean theory dependencies.
433 * Start preparing shift from isac-java to Isabelle/jEdit.
435 subsubsection \<open>State of tests: unchanged\<close>
436 subsubsection \<open>Changesets of begin and end\<close>
438 last changeset with Test_Isac 925fef0f4c81
439 first changeset with Test_Isac bbb414976dfe
442 subsection \<open>isac on Isabelle2015\<close>
443 subsubsection \<open>Summary of development\<close>
445 * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
446 This complicates Test_Isac, see "Prepare running tests" above.
447 * Remove TTY interface.
448 * Re-activate insertion sort.
450 subsubsection \<open>State of tests: unchanged\<close>
451 subsubsection \<open>Changesets of begin and end\<close>
453 last changeset with Test_Isac 2f1b2854927a
454 first changeset with Test_Isac ???
457 subsection \<open>isac on Isabelle2014\<close>
458 subsubsection \<open>Summary of development\<close>
460 migration from "isabelle tty" --> libisabelle
463 subsection \<open>isac on Isabelle2013-2\<close>
464 subsubsection \<open>Summary of development\<close>
466 reactivated context_thy
468 subsubsection \<open>State of tests\<close>
472 subsubsection \<open>Changesets of begin and end\<close>
476 : isac on Isablle2013-2
478 Changeset: 55318 (03826ceb24da) merged
479 User: Walther Neuper <neuper@ist.tugraz.at>
480 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
483 subsection \<open>isac on Isabelle2013-1\<close>
484 subsubsection \<open>Summary of development\<close>
486 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
487 no significant development steps for ISAC.
489 subsubsection \<open>State of tests\<close>
491 See points in subsection "isac on Isabelle2011", "State of tests".
493 subsubsection \<open>Changesets of begin and end\<close>
495 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
496 User: Walther Neuper <neuper@ist.tugraz.at>
497 Date: 2013-12-03 18:13:31 +0100 (8 days)
499 : isac on Isablle2013-1
501 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
502 User: Walther Neuper <neuper@ist.tugraz.at>
503 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
507 subsection \<open>isac on Isabelle2013\<close>
508 subsubsection \<open>Summary of development\<close>
510 # Oct.13: replaced "axioms" by "axiomatization"
511 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
512 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
513 simplification of multivariate rationals (without improving the rulesets involved).
515 subsubsection \<open>Run tests\<close>
517 Is standard now; this subsection will be discontinued under Isabelle2013-1
519 subsubsection \<open>State of tests\<close>
521 See points in subsection "isac on Isabelle2011", "State of tests".
522 # re-activated listC.sml
524 subsubsection \<open>Changesets of begin and end\<close>
526 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
527 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
528 Date: Tue Nov 19 22:23:30 2013 +0000
530 : isac on Isablle2013
532 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
533 User: Walther Neuper <neuper@ist.tugraz.at>
534 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
537 subsection \<open>isac on Isabelle2012\<close>
538 subsubsection \<open>Summary of development\<close>
540 isac on Isabelle2012 is considered just a transitional stage
541 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
542 For considerations on the transition see
543 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
545 subsubsection \<open>Run tests\<close>
547 $ cd /usr/local/isabisac12/
548 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
549 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
551 subsubsection \<open>State of tests\<close>
553 At least the tests from isac on Isabelle2011 run again.
554 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
555 in parallel with evaluation.
557 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
558 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
559 (i.e. on the old notebook from 2002).
561 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
562 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
563 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
564 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
565 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
567 Some tests have been re-activated (e.g. error patterns, fill patterns).
569 subsubsection \<open>Changesets of begin and end\<close>
571 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
572 User: Walther Neuper <neuper@ist.tugraz.at>
573 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
575 : isac on Isablle2012
577 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
578 User: Walther Neuper <neuper@ist.tugraz.at>
579 Date: 2012-09-24 18:35:13 +0200 (8 months)
580 ------------------------------------------------------------------------------
581 Changeset: 48756 (7443906996a8) merged
582 User: Walther Neuper <neuper@ist.tugraz.at>
583 Date: 2012-09-24 18:15:49 +0200 (8 months)
586 subsection \<open>isac on Isabelle2011\<close>
587 subsubsection \<open>Summary of development\<close>
589 isac's mathematics engine has been extended by two developments:
590 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
591 (2) Z_Transform was introduced by Jan Rocnik, which revealed
592 further errors introduced by (1).
593 (3) "error patterns" were introduced by Gabriella Daroczy
594 Regressions tests have been added for all of these.
596 subsubsection \<open>Run tests\<close>
598 $ cd /usr/local/isabisac11/
599 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
600 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
602 subsubsection \<open>State of tests\<close>
604 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
605 and sometimes give reasons for failing tests.
606 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
607 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
609 The most signification tests (in particular Frontend/interface.sml) run,
610 however, many "error in kernel" are not caught by an exception.
611 ------------------------------------------------------------------------------
612 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
613 ------------------------------------------------------------------------------
614 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
615 User: Walther Neuper <neuper@ist.tugraz.at>
616 Date: 2012-08-06 10:38:11 +0200 (11 months)
619 The list below records TODOs while producing an ISAC kernel for
620 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
621 (so to be resumed with Isabelle2013-1):
622 ############## WNxxxxxx.TODO can be found in sources ##############
623 --------------------------------------------------------------------------------
624 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
625 --------------------------------------------------------------------------------
626 WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with
627 this special case (see) --- why not nxt = Model_Problem here ? ---
628 --------------------------------------------------------------------------------
629 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
631 # simplify_* , *_simp_*
633 # calc_* , calculate_* ... require iteration over all rls ...
634 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
635 --------------------------------------------------------------------------------
636 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
637 --------------------------------------------------------------------------------
638 WN120314 changeset a393bb9f5e9f drops root equations.
639 see test/Tools/isac/Knowledge/rootrateq.sml
640 --------------------------------------------------------------------------------
641 WN120317.TODO changeset 977788dfed26 dropped rateq:
642 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
643 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
644 investigation Check_elementwise stopped due to too much effort finding out,
645 why Check_elementwise worked in 2002 in spite of the error.
646 --------------------------------------------------------------------------------
647 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
648 --------------------------------------------------------------------------------
649 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
650 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
651 --------------------------------------------------------------------------------
652 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
653 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
654 --------------------------------------------------------------------------------
655 WN120320.TODO check-improve rlsthmsNOTisac:
656 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
657 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
658 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
659 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
660 --------------------------------------------------------------------------------
661 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
662 --------------------------------------------------------------------------------
663 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
664 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
665 --------------------------------------------------------------------------------
666 WN120321.TODO rearrange theories:
670 ///Descript.thy --> ProgLang
671 Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*)
672 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
673 Interpret.thy are generated (simplifies xml structure for theories)
676 ListC.thy <--- first_Proglang_thy
677 --------------------------------------------------------------------------------
678 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
679 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
680 broken during work on thy-hierarchy
681 --------------------------------------------------------------------------------
682 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
683 test --- the_hier (get_thes ()) (collect_thydata ())---
684 --------------------------------------------------------------------------------
685 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
686 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
687 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
688 --------------------------------------------------------------------------------
689 WN120409.TODO replace "op mem" (2002) with member (2011) ...
690 ... an exercise interesting for beginners !
691 --------------------------------------------------------------------------------
692 WN120411 scanning html representation of newly generated knowledge:
694 ** Theorems: only "Proof of the theorem" (correct!)
695 and "(c) isac-team (math-autor)"
696 ** Rulesets: only "Identifier:///"
697 and "(c) isac-team (math-autor)"
698 ** IsacKnowledge: link to dependency graph (which needs to be created first)
699 ** IsacScripts --> ProgramLanguage
700 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
705 ** Z-Transform is missing !!!
706 ** type-constraints !!!
707 --------------------------------------------------------------------------------
708 WN120417: merging xmldata revealed:
709 ..............NEWLY generated:........................................
711 <GUH> thy_isab_Fun-thm-o_apply </GUH>
713 <STRING> Isabelle </STRING>
714 <STRING> Fun </STRING>
715 <STRING> Theorems </STRING>
716 <STRING> o_apply </STRING>
719 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
722 <TEXT> Proof of the theorem </TEXT>
723 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
726 <EXPLANATIONS> </EXPLANATIONS>
728 <STRING> Isabelle team, TU Munich </STRING>
733 ..............OLD FORMAT:.............................................
735 <GUH> thy_isab_Fun-thm-o_apply </GUH>
737 <STRING> Isabelle </STRING>
738 <STRING> Fun </STRING>
739 <STRING> Theorems </STRING>
740 <STRING> o_apply </STRING>
745 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
750 <TEXT> Proof of the theorem </TEXT>
751 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
754 <EXPLANATIONS> </EXPLANATIONS>
756 <STRING> Isabelle team, TU Munich </STRING>
761 --------------------------------------------------------------------------------
763 subsubsection \<open>Changesets of begin and end\<close>
765 isac development was done between these changesets:
766 ------------------------------------------------------------------------------
767 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
768 User: Walther Neuper <neuper@ist.tugraz.at>
769 Date: 2012-09-24 16:39:30 +0200 (8 months)
771 : isac on Isablle2011
773 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
774 Branch: decompose-isar
775 User: Walther Neuper <neuper@ist.tugraz.at>
776 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
777 ------------------------------------------------------------------------------
780 subsection \<open>isac on Isabelle2009-2\<close>
781 subsubsection \<open>Summary of development\<close>
783 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
784 The update was painful (bridging 7 years of Isabelle development) and cut short
785 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
786 going on to Isabelle2011 although most of the tests did not run.
788 subsubsection \<open>Run tests\<close>
790 WN131021 this is broken by installation of Isabelle2011/12/13,
791 because all these write their binaries to ~/.isabelle/heaps/..
793 $ cd /usr/local/isabisac09-2/
794 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
795 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
796 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
798 subsubsection \<open>State of tests\<close>
800 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
802 subsubsection \<open>Changesets of begin and end\<close>
804 isac development was done between these changesets:
805 ------------------------------------------------------------------------------
806 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
807 Branch: decompose-isar
808 User: Marco Steger <m.steger@student.tugraz.at>
809 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
811 : isac on Isablle2009-2
813 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
814 Branch: isac-from-Isabelle2009-2
815 User: Walther Neuper <neuper@ist.tugraz.at>
816 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
817 ------------------------------------------------------------------------------
820 subsection \<open>isac on Isabelle2002\<close>
821 subsubsection \<open>Summary of development\<close>
823 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
824 of isac's mathematics engine has been implemented.
826 subsubsection \<open>Run tests\<close>
827 subsubsection \<open>State of tests\<close>
829 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
830 recent Linux versions)
832 subsubsection \<open>Changesets of begin and end\<close>
834 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
835 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
839 (*========== inhibit exn 130719 Isabelle2013 ===================================
840 ============ inhibit exn 130719 Isabelle2013 =================================*)
842 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
843 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)