equal
deleted
inserted
replaced
10 |
10 |
11 $ cd /usr/local/isabisac/ |
11 $ cd /usr/local/isabisac/ |
12 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & |
12 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & |
13 *) |
13 *) |
14 |
14 |
15 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
15 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
16 (* !!!!! wait a minute until Isac and the theories below are loaded !!!!! *) |
16 (* !!!!! wait a minute until session Isac and the theories below are loaded !!!!! *) |
17 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) |
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" |
73 ML_file "Interpret/script.sml" |
73 ML_file "Interpret/script.sml" |
74 ML_file "Interpret/solve.sml" |
74 ML_file "Interpret/solve.sml" |
75 ML_file "Interpret/inform.sml" |
75 ML_file "Interpret/inform.sml" |
76 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: |
76 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: |
77 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) |
77 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) |
78 ML_file "Interpret/mathengine.sml" (*!part.*) |
78 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*) |
79 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} |
79 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} |
80 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} |
80 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} |
81 ML_file "xmlsrc/mathml.sml" (*part.*) |
81 ML_file "xmlsrc/mathml.sml" (*part.*) |
82 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*) |
82 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*) |
83 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*) |
83 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*) |
116 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
116 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
117 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) |
117 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) |
118 ML_file "Knowledge/rootrat.sml" |
118 ML_file "Knowledge/rootrat.sml" |
119 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
119 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
120 ML_file "Knowledge/partial_fractions.sml" |
120 ML_file "Knowledge/partial_fractions.sml" |
121 ML_file "Knowledge/polyeq.sml" (*-----------------works if cut into parts !!!!!!!!!!!*) |
121 ML_file "Knowledge/polyeq.sml" |
122 (*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *) |
122 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *) |
123 ML_file "Knowledge/calculus.sml" |
123 ML_file "Knowledge/calculus.sml" |
124 ML_file "Knowledge/trig.sml" |
124 ML_file "Knowledge/trig.sml" |
125 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) |
125 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) |
126 ML_file "Knowledge/diff.sml" |
126 ML_file "Knowledge/diff.sml" |
127 ML_file "Knowledge/integrate.sml" |
127 ML_file "Knowledge/integrate.sml" |
136 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml" |
136 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml" |
137 ML_file "Knowledge/isac.sml" |
137 ML_file "Knowledge/isac.sml" |
138 ML_file "Knowledge/build_thydata.sml" |
138 ML_file "Knowledge/build_thydata.sml" |
139 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*} |
139 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*} |
140 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
140 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
141 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} |
|
142 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
|
143 |
141 |
144 section {* history of tests *} |
142 section {* history of tests *} |
145 text {* |
143 text {* |
146 Systematic regression tests have been introduced to isac development in 2003. |
144 Systematic regression tests have been introduced to isac development in 2003. |
147 Sanity of the regression test suffered from updates following Isabelle development, |
145 Sanity of the regression test suffered from updates following Isabelle development, |