1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) |
1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) |
2 Author: Walther Neuper 101001 |
2 Author: Walther Neuper 101001 |
3 (c) copyright due to lincense terms. |
3 (c) copyright due to lincense terms. |
4 |
4 |
5 isac tests |
5 Isac's tests are organised parallel to sources: |
6 in ~~/test/Tools/isac are structured according |
6 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac" |
7 to ~~/src/Tools/isac |
7 plus |
8 Additional tests are in |
|
9 ~~/test/Tools/isac/ADDTESTS |
8 ~~/test/Tools/isac/ADDTESTS |
10 ~~/test/Tools/isac/Minisubpbl |
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality |
11 |
10 |
12 $ cd /usr/local/isabisac/ |
11 $ cd /usr/local/isabisac/ |
13 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & |
12 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & |
14 *) |
13 *) |
15 |
14 |
16 (*ATTENTION: "Knowledge/biegelinie.sml" NEEDS MANUAL INTERVENTION: |
15 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
17 Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?*) |
16 (* !!!!! wait a minute until Isac and the theories below are loaded !!!!! *) |
|
17 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
18 |
18 |
19 theory Test_Isac imports Isac |
19 theory Test_Isac imports Isac |
20 "ADDTESTS/Ctxt" |
20 "ADDTESTS/Ctxt" |
21 "ADDTESTS/test-depend/Build_Test" |
21 "ADDTESTS/test-depend/Build_Test" |
22 "ADDTESTS/All_Ctxt" |
22 "ADDTESTS/All_Ctxt" |
23 "ADDTESTS/course/phst11/T1_Basics" |
23 "ADDTESTS/course/phst11/T1_Basics" |
24 "ADDTESTS/course/phst11/T2_Rewriting" |
24 "ADDTESTS/course/phst11/T2_Rewriting" |
25 "ADDTESTS/course/phst11/T3_MathEngine" |
25 "ADDTESTS/course/phst11/T3_MathEngine" |
26 "ADDTESTS/file-depend/BuildC_Test" |
26 "ADDTESTS/file-depend/BuildC_Test" |
27 "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" |
27 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"*) |
28 "~~/test/Pure/Isar/Test_Parsers" |
28 "~~/test/Pure/Isar/Test_Parsers" |
29 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*) |
29 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*) |
30 "~~/test/Pure/Isar/Test_Parse_Term" |
30 "~~/test/Pure/Isar/Test_Parse_Term" |
31 "~~/test/HOL/Library/Test_Polynomial" |
31 "~~/test/HOL/Library/Test_Polynomial" |
32 |
32 |
33 "~~/src/Tools/isac/Knowledge/GCD_Poly" (*not imported by Isac.thy*) |
33 "~~/src/Tools/isac/Knowledge/GCD_Poly" (*not imported by Isac.thy*) |
34 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) |
34 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) |
35 |
|
36 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
|
37 (* !!!!! wait a minute until Isac and the above theories are loaded !!!!! *) |
|
38 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
|
39 (* !!!!! with this changeset evaluation doen't start < 7min; UG is busy ! *) |
|
40 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
|
41 |
35 |
42 begin |
36 begin |
43 section {* test ML Code of isac *} |
37 section {* test ML Code of isac *} |
44 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
38 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
45 ML_file "library.sml" |
39 ML_file "library.sml" |
121 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
115 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
122 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) |
116 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) |
123 ML_file "Knowledge/rootrat.sml" |
117 ML_file "Knowledge/rootrat.sml" |
124 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
118 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
125 ML_file "Knowledge/partial_fractions.sml" |
119 ML_file "Knowledge/partial_fractions.sml" |
126 (*ML_file "Knowledge/polyeq.sml" -----------------works if cut into parts !!!!!!!!!!!*) |
120 ML_file "Knowledge/polyeq.sml" (*-----------------works if cut into parts !!!!!!!!!!!*) |
127 (*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *) |
121 (*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *) |
128 ML_file "Knowledge/calculus.sml" |
122 ML_file "Knowledge/calculus.sml" |
129 ML_file "Knowledge/trig.sml" |
123 ML_file "Knowledge/trig.sml" |
130 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) |
124 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) |
131 ML_file "Knowledge/diff.sml" |
125 ML_file "Knowledge/diff.sml" |