1 (*.evaluate isac (all the code of the kernel) and isactest |
|
2 (c) Walther Neuper 1997 |
|
3 |
|
4 /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac |
|
5 |
|
6 /usr/local/Isabelle2002/bin/isabelle HOL-Real |
|
7 cd"~/proto2/isac/src/sml"; |
|
8 use"RTEST-root.sml"; |
|
9 |
|
10 use"ROOT.ML"; |
|
11 use"RCODE-root.sml"; |
|
12 .*) |
|
13 |
|
14 "**** run the tests **************************************"; |
|
15 cd "systest"; |
|
16 (*+ check kbtest/diffapp.sml for additional items in met-model*) |
|
17 use"root-equ.sml"; |
|
18 use"script.sml"; |
|
19 (* use"script_if.sml"; WN03 missing: is_rootequation_in*) |
|
20 use"scriptnew.sml"; |
|
21 use"subp-rooteq.sml"; |
|
22 use"tacis.sml"; |
|
23 use"interface-xml.sml"; |
|
24 (* use"testdaten.sml"; no update after dropping 'errorBound'*) |
|
25 cd "../.."; |
|
26 "**** run systests complete ******************************"; |
|
27 |
|
28 cd"smltest/Scripts"; |
|
29 use"calculate-float.sml"; |
|
30 use"calculate.sml"; |
|
31 use"listg.sml"; |
|
32 use"rewrite.sml"; |
|
33 use"scrtools.sml"; |
|
34 use"term_G.sml"; |
|
35 use"tools.sml"; |
|
36 cd "../.."; |
|
37 cd"smltest/ME"; |
|
38 use"ctree.sml"; |
|
39 use"calchead.sml"; |
|
40 use"rewtools.sml"; |
|
41 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); |
|
42 use"inform.sml"; |
|
43 use"me.sml"; |
|
44 use"ptyps.sml"; |
|
45 cd "../.."; |
|
46 cd"smltest/xmlsrc"; |
|
47 use"datatypes.sml"; |
|
48 use"pbl-met-hierarchy.sml"; |
|
49 use"thy-hierarchy.sml"; |
|
50 cd "../.."; |
|
51 cd"smltest/FE-interface"; |
|
52 use"interface.sml"; |
|
53 cd "../.."; |
|
54 "**** run tests on math-engine complete ******************"; |
|
55 cd"smltest/IsacKnowledge"; |
|
56 use"atools.sml"; |
|
57 use"complex.sml"; |
|
58 use"diff.sml"; |
|
59 use"diffapp.sml"; |
|
60 use"integrate.sml"; |
|
61 use"equation.sml"; |
|
62 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
|
63 use"logexp.sml"; |
|
64 use"poly.sml"; |
|
65 use"polyminus.sml"; |
|
66 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN |
|
67 ? also check others without check 'diff.behav.'*); |
|
68 use"rateq.sml"; |
|
69 use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*); |
|
70 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln', |
|
71 for simplification search MG |
|
72 erls: 98a(1) 104a(1) 104a(2) 68a *); |
|
73 use"root.sml"; |
|
74 use"rooteq.sml"; |
|
75 use"rootrateq.sml"; |
|
76 use"termorder.sml"; |
|
77 use"trig.sml"; |
|
78 use"vect.sml"; |
|
79 use"wn.sml"; |
|
80 use"eqsystem.sml"; |
|
81 use"biegelinie.sml"; |
|
82 use"algein.sml"; |
|
83 cd "../.."; |
|
84 "**** run tests on IsacKnowledge complete ****************"; |
|
85 |
|
86 val path = "/home/neuper/proto2/testsml2xml/"; |
|
87 pbl_hierarchy2file (path ^ "pbl/"); |
|
88 pbls2file (path ^ "pbl/"); |
|
89 met_hierarchy2file (path ^ "met/"); |
|
90 mets2file (path ^ "met/"); |
|
91 thy_hierarchy2file (path ^ "thy/"); |
|
92 thes2file (path ^ "thy/"); |
|
93 "**** tested creation of xmldata *************************"; |
|
94 |
|
95 cd"sml"; |
|
96 states:=[]; |
|
97 "========================================================="; |
|
98 |
|
99 "**** run systests complete ***************** re-organize!"; |
|
100 "**** run tests on math-engine complete ******************"; |
|
101 "**** run tests on IsacKnowledge complete ****************"; |
|
102 "**** build isac kernel + run tests complete *************"; |
|
103 "**** tested creation of xmldata *************************"; |
|