1 (* Title Run_Tests on isac
2 $ cd /usr/local/isabisac/test/Tools/isac
3 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
5 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
6 !!!!!!! actual version is src/Tools/isac/Test_isac.thy !!!!!!!
7 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
9 RESTART emacs after having created a new Isac heap.
10 was sml/RTEST-root.sml in isac-2002
12 12345678901234567890123456789012345678901234567890123456789012345678901234567890
13 10 20 30 40 50 60 70 80
16 theory Test_Isac imports Isac begin
18 ML{* writeln "**** run the tests **************************************" *};
19 ML {* Toplevel.debug := true; *}
22 (*+ check kbtest/diffapp.sml for additional items in met-model*)
25 (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
29 use"interface-xml.sml";
30 (* use"testdaten.sml"; no update after dropping 'errorBound'*)
33 ML{* writeln "**** run systests complete ******************************" *};
36 val t1 = @{term "1+2::real"};
37 val t2 = @{term "abc"};
39 fun terms2str ts = (strs2str o (map term2str )) ts;
40 terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";
41 fun terms2str' ts = (strs2str' o (map term2str )) ts;
42 terms2str' [t1,t2] = "[1 + 2,abc]";
43 fun terms2strs ts = (map term2str) ts;
44 terms2strs [t1,t2] = ["1 + 2", "abc"];
49 use"calculate-float.sml";
51 use"ProgLang/calculate.sml"; (*part.*)
55 use"ProgLang/rewrite.sml"; (*part.*)
64 use "Interpret/calchead.sml" (*part.*)
68 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
75 use"pbl-met-hierarchy.sml";
76 use"thy-hierarchy.sml";
78 cd"smltest/FE-interface";
82 ML{* writeln "**** run tests on math-engine complete ******************" *};
84 cd"smltest/IsacKnowledge";
90 use "Knowledge/integrate.sml"; (*part.*)
93 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
96 use"Knowledge/poly.sml"; (*part.*)
99 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
100 ? also check others without check 'diff.behav.'*);
102 use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
103 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
104 for simplification search MG
105 erls: 98a(1) 104a(1) 104a(2) 68a *);
119 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
121 *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
122 *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
124 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
126 use_thy "../../Pure/Isar/Test_Parse_Term"
127 use_thy "../../Pure/Isar/Test_Parsers"
129 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
131 val path = "/home/neuper/proto2/testsml2xml/";
132 pbl_hierarchy2file (path ^ "pbl/");
133 pbls2file (path ^ "pbl/");
134 met_hierarchy2file (path ^ "met/");
135 mets2file (path ^ "met/");
136 thy_hierarchy2file (path ^ "thy/");
137 thes2file (path ^ "thy/");
140 ML{* writeln "**** tested creation of xmldata *************************" *};
143 writeln "=========================================================";
145 writeln "**** run systests complete ***************** re-organize!";
146 writeln "**** run tests on math-engine complete ******************";
147 writeln "**** run tests on IsacKnowledge complete ****************";
148 writeln "**** build isac kernel + run tests complete *************";
149 writeln "**** tested creation of xmldata *************************";