|
1 (* Title Run_Tests on isac |
|
2 $ cd /usr/local/isabisac/test/Tools/isac |
|
3 $ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy & |
|
4 |
|
5 was sml/RTEST-root.sml in isac-2002 |
|
6 *) |
|
7 |
|
8 theory Test_Isac imports Isac begin |
|
9 |
|
10 ML{* writeln "**** run the tests **************************************" *}; |
|
11 (* |
|
12 cd "systest"; |
|
13 (*+ check kbtest/diffapp.sml for additional items in met-model*) |
|
14 use"root-equ.sml"; |
|
15 use"script.sml"; |
|
16 (* use"script_if.sml"; WN03 missing: is_rootequation_in*) |
|
17 use"scriptnew.sml"; |
|
18 use"subp-rooteq.sml"; |
|
19 use"tacis.sml"; |
|
20 use"interface-xml.sml"; |
|
21 (* use"testdaten.sml"; no update after dropping 'errorBound'*) |
|
22 cd "../.."; |
|
23 *) |
|
24 ML{* writeln "**** run systests complete ******************************" *}; |
|
25 (* |
|
26 cd"smltest/Scripts"; |
|
27 use"calculate-float.sml"; |
|
28 use"calculate.sml"; |
|
29 use"listg.sml"; |
|
30 use"rewrite.sml"; |
|
31 use"scrtools.sml"; |
|
32 use"term.sml"; |
|
33 use"tools.sml"; |
|
34 cd "../.."; |
|
35 cd"smltest/ME"; |
|
36 use"ctree.sml"; |
|
37 *) |
|
38 use "Interpret/calchead.sml" |
|
39 (* |
|
40 use"calchead.sml"; |
|
41 use"rewtools.sml"; |
|
42 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); |
|
43 use"inform.sml"; |
|
44 use"me.sml"; |
|
45 use"ptyps.sml"; |
|
46 cd "../.."; |
|
47 cd"smltest/xmlsrc"; |
|
48 use"datatypes.sml"; |
|
49 use"pbl-met-hierarchy.sml"; |
|
50 use"thy-hierarchy.sml"; |
|
51 cd "../.."; |
|
52 cd"smltest/FE-interface"; |
|
53 use"interface.sml"; |
|
54 cd "../.."; |
|
55 *) |
|
56 ML{* writeln "**** run tests on math-engine complete ******************" *}; |
|
57 (* |
|
58 cd"smltest/IsacKnowledge"; |
|
59 use"atools.sml"; |
|
60 use"complex.sml"; |
|
61 use"diff.sml"; |
|
62 use"diffapp.sml"; |
|
63 use"integrate.sml"; |
|
64 use"equation.sml"; |
|
65 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
|
66 use"logexp.sml"; |
|
67 use"poly.sml"; |
|
68 use"polyminus.sml"; |
|
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.'*); |
|
71 use"rateq.sml"; |
|
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 *); |
|
76 use"root.sml"; |
|
77 use"rooteq.sml"; |
|
78 use"rootrateq.sml"; |
|
79 use"termorder.sml"; |
|
80 use"trig.sml"; |
|
81 use"vect.sml"; |
|
82 use"wn.sml"; |
|
83 use"eqsystem.sml"; |
|
84 use"biegelinie.sml"; |
|
85 use"algein.sml"; |
|
86 cd "../.."; |
|
87 *) |
|
88 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}; |
|
89 (* |
|
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/"); |
|
97 cd"sml"; |
|
98 *) |
|
99 ML{* writeln "**** tested creation of xmldata *************************" *}; |
|
100 |
|
101 ML{*states:=[]; |
|
102 writeln "========================================================="; |
|
103 |
|
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 *************************"; |
|
109 *} |
|
110 |
|
111 end |