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
58 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
59 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
60 "ADDTESTS/accumulate-val/Thy_All"
62 "ADDTESTS/test-depend/Build_Test"
65 "ADDTESTS/course/phst11/T1_Basics"
66 "ADDTESTS/course/phst11/T2_Rewriting"
67 "ADDTESTS/course/phst11/T3_MathEngine"
68 "ADDTESTS/file-depend/BuildC_Test"
69 "ADDTESTS/session-get_theory/Foo"
70 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
71 ADDTESTS/------------------------------------------- see end of tests *)
72 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
73 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
74 "~~/test/Pure/Isar/Test_Parse_Term"
75 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
76 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
77 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
81 "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
82 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
83 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
84 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
85 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
86 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
91 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
92 (* these vvv test, if funs are intermediately opened in structure
93 in case of errors here consider ~~/./xtest-to-coding.sh *)
95 open Math_Engine; CalcTreeTEST;
97 open Inform; cas_input;
98 open Rtools; trtas2str;
99 open Chead; pt_extract;
100 open Generate; (* NONE *)
101 open Ctree; append_problem;
102 open Specify; show_ptyps;
103 open Applicable; mk_set;
104 open Solve; (* NONE *)
106 open Stool; transfer_asms_from_to;
108 open Model; (* NONE *)
109 open LTool; rule2stac;
110 open Rewrite; mk_thm;
114 open Rule; string_of_thm;
115 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
119 "~~~~~ fun xxx, args:"; val () = ();
125 KEStore_Elems.set_ref_thy @{theory};
126 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
129 (*---------------------- check test file by testfile -------------------------------------------
130 ---------------------- check test file by testfile -------------------------------------------*)
131 section \<open>trials with Isabelle's functions\<close>
132 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
133 ML_file "~~/test/Pure/General/alist.ML"
134 ML_file "~~/test/Pure/General/basics.ML"
135 ML_file "~~/test/Pure/General/scan.ML"
136 ML_file "~~/test/Pure/PIDE/xml.ML"
137 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
139 section \<open>test ML Code of isac\<close>
140 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
141 ML_file "library.sml"
142 ML_file "calcelems.sml"
143 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
144 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
145 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
146 ML_file "ProgLang/termC.sml"
147 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
148 ML_file "ProgLang/rewrite.sml"
149 ML_file "ProgLang/listC.sml"
150 ML_file "ProgLang/scrtools.sml"
151 ML_file "ProgLang/tools.sml"
152 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
153 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
154 ML \<open>"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";\<close>
155 ML \<open>"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";\<close>
156 ML_file "Minisubpbl/000-comments.sml"
157 ML_file "Minisubpbl/100-init-rootpbl.sml"
158 ML_file "Minisubpbl/150-add-given.sml"
159 ML_file "Minisubpbl/200-start-method.sml"
162 "~~~~~ fun xxx, args:"; val () = ();
168 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
169 ML_file "Minisubpbl/300-init-subpbl.sml"
170 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
171 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
172 ML_file "Minisubpbl/500-met-sub-to-root.sml"
173 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
174 ML_file "Minisubpbl/600-postcond.sml"
175 ML \<open>"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";\<close>
176 ML \<open>"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";\<close>
177 ML_file "Interpret/mstools.sml"
178 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
179 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
180 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
181 ML_file "Interpret/generate.sml"
182 ML_file "Interpret/calchead.sml"
183 ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
184 ML_file "Interpret/rewtools.sml"
185 ML_file "Interpret/script.sml"
186 ML_file "Interpret/solve.sml"
187 ML_file "Interpret/inform.sml"
188 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
189 ML \<open>"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";\<close>
190 ML \<open>"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";\<close>
191 ML_file "xmlsrc/mathml.sml" (*part.*)
192 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
193 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
194 ML_file "xmlsrc/thy-hierarchy.sml"
195 ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
196 ML \<open>"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";\<close>
197 ML \<open>"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";\<close>
198 ML_file "Frontend/messages.sml"
199 ML_file "Frontend/states.sml"
200 ML_file "Frontend/interface.sml"
201 ML_file "Frontend/use-cases.sml"
202 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
203 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
204 ML_file "print_exn_G.sml"
205 ML \<open>"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";\<close>
206 ML \<open>"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";\<close>
207 ML_file "Knowledge/delete.sml"
208 ML_file "Knowledge/descript.sml"
209 ML_file "Knowledge/atools.sml"
210 ML_file "Knowledge/simplify.sml"
211 ML_file "Knowledge/poly.sml"
212 ML_file "Knowledge/gcd_poly_ml.sml"
213 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
214 ML_file "Knowledge/rational.sml"
215 ML_file "Knowledge/equation.sml"
216 ML_file "Knowledge/root.sml"
217 ML_file "Knowledge/lineq.sml"
218 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
219 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
220 ML_file "Knowledge/rootrat.sml"
221 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
222 ML_file "Knowledge/partial_fractions.sml"
223 ML_file "Knowledge/polyeq.sml"
224 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
225 ML_file "Knowledge/calculus.sml"
226 ML_file "Knowledge/trig.sml"
227 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
228 ML_file "Knowledge/diff.sml"
229 ML_file "Knowledge/integrate.sml"
230 ML_file "Knowledge/eqsystem.sml"
231 ML_file "Knowledge/test.sml"
232 ML_file "Knowledge/polyminus.sml"
233 ML_file "Knowledge/vect.sml"
234 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
235 ML_file "Knowledge/biegelinie-1.sml"
236 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *)
237 ML_file "Knowledge/algein.sml"
238 ML_file "Knowledge/diophanteq.sml"
239 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
240 ML_file "Knowledge/inssort.sml"
241 ML_file "Knowledge/isac.sml"
242 ML_file "Knowledge/build_thydata.sml"
243 ML \<open>"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
244 ML \<open>"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";\<close>
245 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
246 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
247 ML \<open>"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
249 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
250 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
251 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
253 section \<open>history of tests\<close>
255 Systematic regression tests have been introduced to isac development in 2003.
256 Sanity of the regression tests suffers from updates following Isabelle development,
257 which mostly exceeded the resources available in isac's development.
259 The survey below shall support to efficiently use the tests for isac
260 on different Isabelle versions. Conclusion in most cases will be:
262 !!! Use most recent tests or go back to the old notebook
263 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
267 subsection \<open>isac on Isabelle2017\<close>
268 subsubsection \<open>Summary of development\<close>
270 * Add further signatures, separate structures and cleanup respective files.
271 * Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
272 * Clean theory dependencies.
273 * Start preparing shift from isac-java to Isabelle/jEdit.
275 subsubsection \<open>State of tests: unchanged\<close>
276 subsubsection \<open>Changesets of begin and end\<close>
278 last changeset with Test_Isac 925fef0f4c81
279 first changeset with Test_Isac bbb414976dfe
282 subsection \<open>isac on Isabelle2015\<close>
283 subsubsection \<open>Summary of development\<close>
285 * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
286 This complicates Test_Isac, see "Prepare running tests" above.
287 * Remove TTY interface.
288 * Re-activate insertion sort.
290 subsubsection \<open>State of tests: unchanged\<close>
291 subsubsection \<open>Changesets of begin and end\<close>
293 last changeset with Test_Isac 2f1b2854927a
294 first changeset with Test_Isac ???
297 subsection \<open>isac on Isabelle2014\<close>
298 subsubsection \<open>Summary of development\<close>
300 migration from "isabelle tty" --> libisabelle
303 subsection \<open>isac on Isabelle2013-2\<close>
304 subsubsection \<open>Summary of development\<close>
306 reactivated context_thy
308 subsubsection \<open>State of tests\<close>
312 subsubsection \<open>Changesets of begin and end\<close>
316 : isac on Isablle2013-2
318 Changeset: 55318 (03826ceb24da) merged
319 User: Walther Neuper <neuper@ist.tugraz.at>
320 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
323 subsection \<open>isac on Isabelle2013-1\<close>
324 subsubsection \<open>Summary of development\<close>
326 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
327 no significant development steps for ISAC.
329 subsubsection \<open>State of tests\<close>
331 See points in subsection "isac on Isabelle2011", "State of tests".
333 subsubsection \<open>Changesets of begin and end\<close>
335 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
336 User: Walther Neuper <neuper@ist.tugraz.at>
337 Date: 2013-12-03 18:13:31 +0100 (8 days)
339 : isac on Isablle2013-1
341 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
342 User: Walther Neuper <neuper@ist.tugraz.at>
343 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
347 subsection \<open>isac on Isabelle2013\<close>
348 subsubsection \<open>Summary of development\<close>
350 # Oct.13: replaced "axioms" by "axiomatization"
351 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
352 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
353 simplification of multivariate rationals (without improving the rulesets involved).
355 subsubsection \<open>Run tests\<close>
357 Is standard now; this subsection will be discontinued under Isabelle2013-1
359 subsubsection \<open>State of tests\<close>
361 See points in subsection "isac on Isabelle2011", "State of tests".
362 # re-activated listC.sml
364 subsubsection \<open>Changesets of begin and end\<close>
366 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
367 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
368 Date: Tue Nov 19 22:23:30 2013 +0000
370 : isac on Isablle2013
372 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
373 User: Walther Neuper <neuper@ist.tugraz.at>
374 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
377 subsection \<open>isac on Isabelle2012\<close>
378 subsubsection \<open>Summary of development\<close>
380 isac on Isabelle2012 is considered just a transitional stage
381 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
382 For considerations on the transition see
383 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
385 subsubsection \<open>Run tests\<close>
387 $ cd /usr/local/isabisac12/
388 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
389 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
391 subsubsection \<open>State of tests\<close>
393 At least the tests from isac on Isabelle2011 run again.
394 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
395 in parallel with evaluation.
397 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
398 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
399 (i.e. on the old notebook from 2002).
401 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
402 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
403 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
404 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
405 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
407 Some tests have been re-activated (e.g. error patterns, fill patterns).
409 subsubsection \<open>Changesets of begin and end\<close>
411 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
412 User: Walther Neuper <neuper@ist.tugraz.at>
413 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
415 : isac on Isablle2012
417 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
418 User: Walther Neuper <neuper@ist.tugraz.at>
419 Date: 2012-09-24 18:35:13 +0200 (8 months)
420 ------------------------------------------------------------------------------
421 Changeset: 48756 (7443906996a8) merged
422 User: Walther Neuper <neuper@ist.tugraz.at>
423 Date: 2012-09-24 18:15:49 +0200 (8 months)
426 subsection \<open>isac on Isabelle2011\<close>
427 subsubsection \<open>Summary of development\<close>
429 isac's mathematics engine has been extended by two developments:
430 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
431 (2) Z_Transform was introduced by Jan Rocnik, which revealed
432 further errors introduced by (1).
433 (3) "error patterns" were introduced by Gabriella Daroczy
434 Regressions tests have been added for all of these.
436 subsubsection \<open>Run tests\<close>
438 $ cd /usr/local/isabisac11/
439 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
440 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
442 subsubsection \<open>State of tests\<close>
444 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
445 and sometimes give reasons for failing tests.
446 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
447 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
449 The most signification tests (in particular Frontend/interface.sml) run,
450 however, many "error in kernel" are not caught by an exception.
451 ------------------------------------------------------------------------------
452 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
453 ------------------------------------------------------------------------------
454 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
455 User: Walther Neuper <neuper@ist.tugraz.at>
456 Date: 2012-08-06 10:38:11 +0200 (11 months)
459 The list below records TODOs while producing an ISAC kernel for
460 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
461 (so to be resumed with Isabelle2013-1):
462 ############## WNxxxxxx.TODO can be found in sources ##############
463 --------------------------------------------------------------------------------
464 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
465 --------------------------------------------------------------------------------
466 WN111013.TODO: remove concept around "fun init_form", lots of troubles with
467 this special case (see) --- why not nxt = Model_Problem here ? ---
468 --------------------------------------------------------------------------------
469 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
471 # simplify_* , *_simp_*
473 # calc_* , calculate_* ... require iteration over all rls ...
474 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
475 --------------------------------------------------------------------------------
476 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
477 --------------------------------------------------------------------------------
478 WN120314 changeset a393bb9f5e9f drops root equations.
479 see test/Tools/isac/Knowledge/rootrateq.sml
480 --------------------------------------------------------------------------------
481 WN120317.TODO changeset 977788dfed26 dropped rateq:
482 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
483 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
484 investigation Check_elementwise stopped due to too much effort finding out,
485 why Check_elementwise worked in 2002 in spite of the error.
486 --------------------------------------------------------------------------------
487 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
488 --------------------------------------------------------------------------------
489 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
490 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
491 --------------------------------------------------------------------------------
492 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
493 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
494 --------------------------------------------------------------------------------
495 WN120320.TODO check-improve rlsthmsNOTisac:
496 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
497 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
498 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
499 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
500 --------------------------------------------------------------------------------
501 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
502 --------------------------------------------------------------------------------
503 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
504 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
505 --------------------------------------------------------------------------------
506 WN120321.TODO rearrange theories:
510 ///Descript.thy --> ProgLang
511 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
512 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
513 Interpret.thy are generated (simplifies xml structure for theories)
516 ListC.thy <--- first_Proglang_thy
517 --------------------------------------------------------------------------------
518 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
519 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
520 broken during work on thy-hierarchy
521 --------------------------------------------------------------------------------
522 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
523 test --- the_hier (get_thes ()) (collect_thydata ())---
524 --------------------------------------------------------------------------------
525 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
526 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
527 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
528 --------------------------------------------------------------------------------
529 WN120409.TODO replace "op mem" (2002) with member (2011) ...
530 ... an exercise interesting for beginners !
531 --------------------------------------------------------------------------------
532 WN120411 scanning html representation of newly generated knowledge:
534 ** Theorems: only "Proof of the theorem" (correct!)
535 and "(c) isac-team (math-autor)"
536 ** Rulesets: only "Identifier:///"
537 and "(c) isac-team (math-autor)"
538 ** IsacKnowledge: link to dependency graph (which needs to be created first)
539 ** IsacScripts --> ProgramLanguage
540 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
545 ** Z-Transform is missing !!!
546 ** type-constraints !!!
547 --------------------------------------------------------------------------------
548 WN120417: merging xmldata revealed:
549 ..............NEWLY generated:........................................
551 <GUH> thy_isab_Fun-thm-o_apply </GUH>
553 <STRING> Isabelle </STRING>
554 <STRING> Fun </STRING>
555 <STRING> Theorems </STRING>
556 <STRING> o_apply </STRING>
559 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
562 <TEXT> Proof of the theorem </TEXT>
563 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
566 <EXPLANATIONS> </EXPLANATIONS>
568 <STRING> Isabelle team, TU Munich </STRING>
573 ..............OLD FORMAT:.............................................
575 <GUH> thy_isab_Fun-thm-o_apply </GUH>
577 <STRING> Isabelle </STRING>
578 <STRING> Fun </STRING>
579 <STRING> Theorems </STRING>
580 <STRING> o_apply </STRING>
585 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
590 <TEXT> Proof of the theorem </TEXT>
591 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
594 <EXPLANATIONS> </EXPLANATIONS>
596 <STRING> Isabelle team, TU Munich </STRING>
601 --------------------------------------------------------------------------------
603 subsubsection \<open>Changesets of begin and end\<close>
605 isac development was done between these changesets:
606 ------------------------------------------------------------------------------
607 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
608 User: Walther Neuper <neuper@ist.tugraz.at>
609 Date: 2012-09-24 16:39:30 +0200 (8 months)
611 : isac on Isablle2011
613 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
614 Branch: decompose-isar
615 User: Walther Neuper <neuper@ist.tugraz.at>
616 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
617 ------------------------------------------------------------------------------
620 subsection \<open>isac on Isabelle2009-2\<close>
621 subsubsection \<open>Summary of development\<close>
623 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
624 The update was painful (bridging 7 years of Isabelle development) and cut short
625 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
626 going on to Isabelle2011 although most of the tests did not run.
628 subsubsection \<open>Run tests\<close>
630 WN131021 this is broken by installation of Isabelle2011/12/13,
631 because all these write their binaries to ~/.isabelle/heaps/..
633 $ cd /usr/local/isabisac09-2/
634 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
635 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
636 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
638 subsubsection \<open>State of tests\<close>
640 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
642 subsubsection \<open>Changesets of begin and end\<close>
644 isac development was done between these changesets:
645 ------------------------------------------------------------------------------
646 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
647 Branch: decompose-isar
648 User: Marco Steger <m.steger@student.tugraz.at>
649 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
651 : isac on Isablle2009-2
653 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
654 Branch: isac-from-Isabelle2009-2
655 User: Walther Neuper <neuper@ist.tugraz.at>
656 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
657 ------------------------------------------------------------------------------
660 subsection \<open>isac on Isabelle2002\<close>
661 subsubsection \<open>Summary of development\<close>
663 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
664 of isac's mathematics engine has been implemented.
666 subsubsection \<open>Run tests\<close>
667 subsubsection \<open>State of tests\<close>
669 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
670 recent Linux versions)
672 subsubsection \<open>Changesets of begin and end\<close>
674 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
675 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
679 (*========== inhibit exn 130719 Isabelle2013 ===================================
680 ============ inhibit exn 130719 Isabelle2013 =================================*)
682 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
683 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)