1 (* Title Run_Tests on isac
2 $ cd /usr/local/isabisac/test/Tools/isac
3 $ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
5 was sml/RTEST-root.sml in isac-2002
8 theory Test_Isac imports Isac begin
10 ML{* writeln "**** run the tests **************************************" *};
13 (*+ check kbtest/diffapp.sml for additional items in met-model*)
16 (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
20 use"interface-xml.sml";
21 (* use"testdaten.sml"; no update after dropping 'errorBound'*)
24 ML{* writeln "**** run systests complete ******************************" *};
27 use"calculate-float.sml";
38 use "Interpret/calchead.sml"
42 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
49 use"pbl-met-hierarchy.sml";
50 use"thy-hierarchy.sml";
52 cd"smltest/FE-interface";
56 ML{* writeln "**** run tests on math-engine complete ******************" *};
58 cd"smltest/IsacKnowledge";
65 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
69 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
70 ? also check others without check 'diff.behav.'*);
72 use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
73 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
74 for simplification search MG
75 erls: 98a(1) 104a(1) 104a(2) 68a *);
88 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
90 val path = "/home/neuper/proto2/testsml2xml/";
91 pbl_hierarchy2file (path ^ "pbl/");
92 pbls2file (path ^ "pbl/");
93 met_hierarchy2file (path ^ "met/");
94 mets2file (path ^ "met/");
95 thy_hierarchy2file (path ^ "thy/");
96 thes2file (path ^ "thy/");
99 ML{* writeln "**** tested creation of xmldata *************************" *};
102 writeln "=========================================================";
104 writeln "**** run systests complete ***************** re-organize!";
105 writeln "**** run tests on math-engine complete ******************";
106 writeln "**** run tests on IsacKnowledge complete ****************";
107 writeln "**** build isac kernel + run tests complete *************";
108 writeln "**** tested creation of xmldata *************************";