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
10 -------------------------------------------------------------------------------
12 Prepare running tests: see below
14 $ cd /usr/local/isabisac/
15 $ export ISABELLE_VERSION=2015 # for libisabelle
16 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
19 section \<open>Prepare running tests\<close>
21 Isac encapsulates code as much as possible in structures without open. TODO ProgLang.
22 This policy conflicts with those tests, which go into functions to details
23 not declared in the signatures.
25 In order to maintain these tests without changes, this has to be done before running tests:
26 (1) Extend signatures for tests by
27 ~~$ ./xcoding-to-test.sh
28 ~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy
29 Running Test_Isac.thy opens all structures, see code after "begin" below.
30 (2) Clean signatures for coding
31 ~~$ ./xtest-to-coding.sh
32 ~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!)
34 ********************* don't forget (2) BEFORE pushing to repository *********************
36 The above bash files accomplish query replace in src/Tools/isac:
37 \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
38 \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
39 ^^^ in signature outcommented, ^^^ NOT outcommented,
40 this is status for coding this is status for tests
43 section \<open>code for copy & paste\<close>
45 "~~~~~ fun , args:"; val () = ();
46 "~~~~~ and , args:"; val () = ();
48 "~~~~~ to return val:"; val () = ();
51 section \<open>Run the tests\<close>
53 * say "OK" to the popup asking for theories to be loaded
54 * watch the <Theories> window for errors in the "imports" below
57 theory Test_Isac imports Build_Thydata (* 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*)
80 "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
81 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
82 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
83 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
84 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
85 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
90 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
91 (* these vvv test, if funs are intermediately opened in structure
92 in case of errors here consider ~~/./xtest-to-coding.sh *)
94 open Math_Engine; CalcTreeTEST;
96 open Inform; cas_input;
97 open Rtools; trtas2str;
98 open Chead; pt_extract;
99 open Generate; (* NONE *)
100 open Ctree; append_problem;
101 open Specify; show_ptyps;
102 open Applicable; mk_set;
103 open Solve; (* NONE *)
105 open Stool; transfer_asms_from_to;
107 open Model; (* NONE *)
108 open LTool; rule2stac;
109 open Rewrite; mk_thm;
113 open Rule; string_of_thm;
114 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
118 "~~~~~ fun xxx, args:"; val () = ();
124 KEStore_Elems.set_ref_thy @{theory};
125 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
128 (*---------------------- check test file by testfile -------------------------------------------
129 ---------------------- check test file by testfile -------------------------------------------*)
130 section {* trials with Isabelle's functions *}
131 ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}
132 ML_file "~~/test/Pure/General/alist.ML"
133 ML_file "~~/test/Pure/General/basics.ML"
134 ML_file "~~/test/Pure/General/scan.ML"
135 ML_file "~~/test/Pure/PIDE/xml.ML"
136 ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
138 section {* test ML Code of isac *}
139 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
140 ML_file "library.sml"
141 ML_file "calcelems.sml"
142 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
143 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
144 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
145 ML_file "ProgLang/termC.sml"
146 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
147 ML_file "ProgLang/rewrite.sml"
148 ML_file "ProgLang/listC.sml"
149 ML_file "ProgLang/scrtools.sml"
150 ML_file "ProgLang/tools.sml"
151 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
152 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
153 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
154 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
155 ML_file "Minisubpbl/000-comments.sml"
156 ML_file "Minisubpbl/100-init-rootpbl.sml"
157 ML_file "Minisubpbl/150-add-given.sml"
158 ML_file "Minisubpbl/200-start-method.sml"
159 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
160 ML_file "Minisubpbl/300-init-subpbl.sml"
161 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
162 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
163 ML_file "Minisubpbl/500-met-sub-to-root.sml"
164 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
165 ML_file "Minisubpbl/600-postcond.sml"
166 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
167 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
168 ML_file "Interpret/mstools.sml"
169 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
170 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
171 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
172 (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
173 ML_file "Interpret/generate.sml"
174 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
175 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
176 ML_file "Interpret/calchead.sml"
177 ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
178 ML_file "Interpret/rewtools.sml"
179 ML_file "Interpret/script.sml"
180 ML_file "Interpret/solve.sml"
181 ML_file "Interpret/inform.sml"
182 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
183 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
184 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
185 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
186 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
187 ML_file "xmlsrc/mathml.sml" (*part.*)
188 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
189 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
190 ML_file "xmlsrc/thy-hierarchy.sml"
191 ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
192 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
193 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
194 ML_file "Frontend/messages.sml"
195 ML_file "Frontend/states.sml"
196 ML_file "Frontend/interface.sml"
197 ML_file "Frontend/use-cases.sml"
198 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
199 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
200 ML_file "print_exn_G.sml"
201 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
202 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
203 ML_file "Knowledge/delete.sml"
204 ML_file "Knowledge/descript.sml"
205 ML_file "Knowledge/atools.sml"
206 ML_file "Knowledge/simplify.sml"
207 ML_file "Knowledge/poly.sml"
208 ML_file "Knowledge/gcd_poly_ml.sml"
209 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
210 ML_file "Knowledge/rational.sml"
211 ML_file "Knowledge/equation.sml"
212 ML_file "Knowledge/root.sml"
213 ML_file "Knowledge/lineq.sml"
214 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
215 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
216 ML_file "Knowledge/rootrat.sml"
217 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
218 ML_file "Knowledge/partial_fractions.sml"
219 ML_file "Knowledge/polyeq.sml"
220 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
221 ML_file "Knowledge/calculus.sml"
222 ML_file "Knowledge/trig.sml"
223 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
224 ML_file "Knowledge/diff.sml"
225 ML_file "Knowledge/integrate.sml"
226 ML_file "Knowledge/eqsystem.sml"
227 ML_file "Knowledge/test.sml"
228 ML_file "Knowledge/polyminus.sml"
229 ML_file "Knowledge/vect.sml"
230 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
231 ML_file "Knowledge/biegelinie-1.sml"
232 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *)
233 ML_file "Knowledge/algein.sml"
234 ML_file "Knowledge/diophanteq.sml"
235 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
236 ML_file "Knowledge/inssort.sml"
237 ML_file "Knowledge/isac.sml"
238 ML_file "Knowledge/build_thydata.sml"
239 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
240 ML {*"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";*}
241 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
242 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
243 ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
245 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
246 ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}
247 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
249 section {* history of tests *}
251 Systematic regression tests have been introduced to isac development in 2003.
252 Sanity of the regression tests suffers from updates following Isabelle development,
253 which mostly exceeded the resources available in isac's development.
255 The survey below shall support to efficiently use the tests for isac
256 on different Isabelle versions. Conclusion in most cases will be:
258 !!! Use most recent tests or go back to the old notebook
259 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
263 subsection {* isac on Isabelle2015 *}
264 subsubsection {* Summary of development *}
266 * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
267 This complicates Test_Isac, see "Prepare running tests" above.
268 * Remove TTY interface.
269 * Re-activate insertion sort.
271 subsubsection {* State of tests: unchanged *}
272 subsubsection {* Changesets of begin and end *}
274 last changeset with Test_Isac 2f1b2854927a
275 first changeset with Test_Isac ???
278 subsection {* isac on Isabelle2014 *}
279 subsubsection {* Summary of development *}
281 migration from "isabelle tty" --> libisabelle
284 subsection {* isac on Isabelle2013-2 *}
285 subsubsection {* Summary of development *}
287 reactivated context_thy
289 subsubsection {* State of tests *}
293 subsubsection {* Changesets of begin and end *}
297 : isac on Isablle2013-2
299 Changeset: 55318 (03826ceb24da) merged
300 User: Walther Neuper <neuper@ist.tugraz.at>
301 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
304 subsection {* isac on Isabelle2013-1 *}
305 subsubsection {* Summary of development *}
307 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
308 no significant development steps for ISAC.
310 subsubsection {* State of tests *}
312 See points in subsection "isac on Isabelle2011", "State of tests".
314 subsubsection {* Changesets of begin and end *}
316 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
317 User: Walther Neuper <neuper@ist.tugraz.at>
318 Date: 2013-12-03 18:13:31 +0100 (8 days)
320 : isac on Isablle2013-1
322 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
323 User: Walther Neuper <neuper@ist.tugraz.at>
324 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
328 subsection {* isac on Isabelle2013 *}
329 subsubsection {* Summary of development *}
331 # Oct.13: replaced "axioms" by "axiomatization"
332 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
333 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
334 simplification of multivariate rationals (without improving the rulesets involved).
336 subsubsection {* Run tests *}
338 Is standard now; this subsection will be discontinued under Isabelle2013-1
340 subsubsection {* State of tests *}
342 See points in subsection "isac on Isabelle2011", "State of tests".
343 # re-activated listC.sml
345 subsubsection {* Changesets of begin and end *}
347 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
348 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
349 Date: Tue Nov 19 22:23:30 2013 +0000
351 : isac on Isablle2013
353 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
354 User: Walther Neuper <neuper@ist.tugraz.at>
355 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
358 subsection {* isac on Isabelle2012 *}
359 subsubsection {* Summary of development *}
361 isac on Isabelle2012 is considered just a transitional stage
362 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
363 For considerations on the transition see
364 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
366 subsubsection {* Run tests *}
368 $ cd /usr/local/isabisac12/
369 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
370 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
372 subsubsection {* State of tests *}
374 At least the tests from isac on Isabelle2011 run again.
375 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
376 in parallel with evaluation.
378 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
379 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
380 (i.e. on the old notebook from 2002).
382 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
383 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
384 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
385 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
386 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
388 Some tests have been re-activated (e.g. error patterns, fill patterns).
390 subsubsection {* Changesets of begin and end *}
392 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
393 User: Walther Neuper <neuper@ist.tugraz.at>
394 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
396 : isac on Isablle2012
398 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
399 User: Walther Neuper <neuper@ist.tugraz.at>
400 Date: 2012-09-24 18:35:13 +0200 (8 months)
401 ------------------------------------------------------------------------------
402 Changeset: 48756 (7443906996a8) merged
403 User: Walther Neuper <neuper@ist.tugraz.at>
404 Date: 2012-09-24 18:15:49 +0200 (8 months)
407 subsection {* isac on Isabelle2011 *}
408 subsubsection {* Summary of development *}
410 isac's mathematics engine has been extended by two developments:
411 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
412 (2) Z_Transform was introduced by Jan Rocnik, which revealed
413 further errors introduced by (1).
414 (3) "error patterns" were introduced by Gabriella Daroczy
415 Regressions tests have been added for all of these.
417 subsubsection {* Run tests *}
419 $ cd /usr/local/isabisac11/
420 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
421 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
423 subsubsection {* State of tests *}
425 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
426 and sometimes give reasons for failing tests.
427 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
428 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
430 The most signification tests (in particular Frontend/interface.sml) run,
431 however, many "error in kernel" are not caught by an exception.
432 ------------------------------------------------------------------------------
433 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
434 ------------------------------------------------------------------------------
435 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
436 User: Walther Neuper <neuper@ist.tugraz.at>
437 Date: 2012-08-06 10:38:11 +0200 (11 months)
440 The list below records TODOs while producing an ISAC kernel for
441 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
442 (so to be resumed with Isabelle2013-1):
443 ############## WNxxxxxx.TODO can be found in sources ##############
444 --------------------------------------------------------------------------------
445 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
446 --------------------------------------------------------------------------------
447 WN111013.TODO: remove concept around "fun init_form", lots of troubles with
448 this special case (see) --- why not nxt = Model_Problem here ? ---
449 --------------------------------------------------------------------------------
450 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
452 # simplify_* , *_simp_*
454 # calc_* , calculate_* ... require iteration over all rls ...
455 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
456 --------------------------------------------------------------------------------
457 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
458 --------------------------------------------------------------------------------
459 WN120314 changeset a393bb9f5e9f drops root equations.
460 see test/Tools/isac/Knowledge/rootrateq.sml
461 --------------------------------------------------------------------------------
462 WN120317.TODO changeset 977788dfed26 dropped rateq:
463 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
464 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
465 investigation Check_elementwise stopped due to too much effort finding out,
466 why Check_elementwise worked in 2002 in spite of the error.
467 --------------------------------------------------------------------------------
468 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
469 --------------------------------------------------------------------------------
470 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
471 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
472 --------------------------------------------------------------------------------
473 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
474 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
475 --------------------------------------------------------------------------------
476 WN120320.TODO check-improve rlsthmsNOTisac:
477 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
478 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
479 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
480 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
481 --------------------------------------------------------------------------------
482 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
483 --------------------------------------------------------------------------------
484 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
485 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
486 --------------------------------------------------------------------------------
487 WN120321.TODO rearrange theories:
491 ///Descript.thy --> ProgLang
492 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
493 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
494 Interpret.thy are generated (simplifies xml structure for theories)
497 ListC.thy <--- first_Proglang_thy
498 --------------------------------------------------------------------------------
499 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
500 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
501 broken during work on thy-hierarchy
502 --------------------------------------------------------------------------------
503 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
504 test --- the_hier (get_thes ()) (collect_thydata ())---
505 --------------------------------------------------------------------------------
506 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
507 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
508 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
509 --------------------------------------------------------------------------------
510 WN120409.TODO replace "op mem" (2002) with member (2011) ...
511 ... an exercise interesting for beginners !
512 --------------------------------------------------------------------------------
513 WN120411 scanning html representation of newly generated knowledge:
515 ** Theorems: only "Proof of the theorem" (correct!)
516 and "(c) isac-team (math-autor)"
517 ** Rulesets: only "Identifier:///"
518 and "(c) isac-team (math-autor)"
519 ** IsacKnowledge: link to dependency graph (which needs to be created first)
520 ** IsacScripts --> ProgramLanguage
521 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
526 ** Z-Transform is missing !!!
527 ** type-constraints !!!
528 --------------------------------------------------------------------------------
529 WN120417: merging xmldata revealed:
530 ..............NEWLY generated:........................................
532 <GUH> thy_isab_Fun-thm-o_apply </GUH>
534 <STRING> Isabelle </STRING>
535 <STRING> Fun </STRING>
536 <STRING> Theorems </STRING>
537 <STRING> o_apply </STRING>
540 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
543 <TEXT> Proof of the theorem </TEXT>
544 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
547 <EXPLANATIONS> </EXPLANATIONS>
549 <STRING> Isabelle team, TU Munich </STRING>
554 ..............OLD FORMAT:.............................................
556 <GUH> thy_isab_Fun-thm-o_apply </GUH>
558 <STRING> Isabelle </STRING>
559 <STRING> Fun </STRING>
560 <STRING> Theorems </STRING>
561 <STRING> o_apply </STRING>
566 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
571 <TEXT> Proof of the theorem </TEXT>
572 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
575 <EXPLANATIONS> </EXPLANATIONS>
577 <STRING> Isabelle team, TU Munich </STRING>
582 --------------------------------------------------------------------------------
584 subsubsection {* Changesets of begin and end *}
586 isac development was done between these changesets:
587 ------------------------------------------------------------------------------
588 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
589 User: Walther Neuper <neuper@ist.tugraz.at>
590 Date: 2012-09-24 16:39:30 +0200 (8 months)
592 : isac on Isablle2011
594 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
595 Branch: decompose-isar
596 User: Walther Neuper <neuper@ist.tugraz.at>
597 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
598 ------------------------------------------------------------------------------
601 subsection {* isac on Isabelle2009-2 *}
602 subsubsection {* Summary of development *}
604 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
605 The update was painful (bridging 7 years of Isabelle development) and cut short
606 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
607 going on to Isabelle2011 although most of the tests did not run.
609 subsubsection {* Run tests *}
611 WN131021 this is broken by installation of Isabelle2011/12/13,
612 because all these write their binaries to ~/.isabelle/heaps/..
614 $ cd /usr/local/isabisac09-2/
615 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
616 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
617 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
619 subsubsection {* State of tests *}
621 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
623 subsubsection {* Changesets of begin and end *}
625 isac development was done between these changesets:
626 ------------------------------------------------------------------------------
627 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
628 Branch: decompose-isar
629 User: Marco Steger <m.steger@student.tugraz.at>
630 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
632 : isac on Isablle2009-2
634 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
635 Branch: isac-from-Isabelle2009-2
636 User: Walther Neuper <neuper@ist.tugraz.at>
637 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
638 ------------------------------------------------------------------------------
641 subsection {* isac on Isabelle2002 *}
642 subsubsection {* Summary of development *}
644 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
645 of isac's mathematics engine has been implemented.
647 subsubsection {* Run tests *}
648 subsubsection {* State of tests *}
650 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
651 recent Linux versions)
653 subsubsection {* Changesets of begin and end *}
655 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
656 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
660 (*========== inhibit exn 130719 Isabelle2013 ===================================
661 ============ inhibit exn 130719 Isabelle2013 =================================*)
663 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
664 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)