1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/RTEST-root.sml Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,103 @@
1.4 +(*.evaluate isac (all the code of the kernel) and isactest
1.5 + (c) Walther Neuper 1997
1.6 +
1.7 + /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
1.8 +
1.9 + /usr/local/Isabelle2002/bin/isabelle HOL-Real
1.10 + cd"~/proto2/isac/src/sml";
1.11 + use"RTEST-root.sml";
1.12 +
1.13 + use"ROOT.ML";
1.14 + use"RCODE-root.sml";
1.15 +.*)
1.16 +
1.17 +"**** run the tests **************************************";
1.18 +cd "systest";
1.19 +(*+ check kbtest/diffapp.sml for additional items in met-model*)
1.20 + use"root-equ.sml";
1.21 + use"script.sml";
1.22 + (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
1.23 + use"scriptnew.sml";
1.24 + use"subp-rooteq.sml";
1.25 + use"tacis.sml";
1.26 + use"interface-xml.sml";
1.27 + (* use"testdaten.sml"; no update after dropping 'errorBound'*)
1.28 + cd "../..";
1.29 +"**** run systests complete ******************************";
1.30 +
1.31 +cd"smltest/Scripts";
1.32 + use"calculate-float.sml";
1.33 + use"calculate.sml";
1.34 + use"listg.sml";
1.35 + use"rewrite.sml";
1.36 + use"scrtools.sml";
1.37 + use"term_G.sml";
1.38 + use"tools.sml";
1.39 + cd "../..";
1.40 +cd"smltest/ME";
1.41 + use"ctree.sml";
1.42 + use"calchead.sml";
1.43 + use"rewtools.sml";
1.44 + use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
1.45 + use"inform.sml";
1.46 + use"me.sml";
1.47 + use"ptyps.sml";
1.48 + cd "../..";
1.49 +cd"smltest/xmlsrc";
1.50 + use"datatypes.sml";
1.51 + use"pbl-met-hierarchy.sml";
1.52 + use"thy-hierarchy.sml";
1.53 + cd "../..";
1.54 +cd"smltest/FE-interface";
1.55 + use"interface.sml";
1.56 + cd "../..";
1.57 +"**** run tests on math-engine complete ******************";
1.58 +cd"smltest/IsacKnowledge";
1.59 + use"atools.sml";
1.60 + use"complex.sml";
1.61 + use"diff.sml";
1.62 + use"diffapp.sml";
1.63 + use"integrate.sml";
1.64 + use"equation.sml";
1.65 + (*use"inssort.sml"; problems with recdef in Isabelle2002*)
1.66 + use"logexp.sml";
1.67 + use"poly.sml";
1.68 + use"polyminus.sml";
1.69 + use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
1.70 + ? also check others without check 'diff.behav.'*);
1.71 + use"rateq.sml";
1.72 + use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
1.73 + use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
1.74 + for simplification search MG
1.75 + erls: 98a(1) 104a(1) 104a(2) 68a *);
1.76 + use"root.sml";
1.77 + use"rooteq.sml";
1.78 + use"rootrateq.sml";
1.79 + use"termorder.sml";
1.80 + use"trig.sml";
1.81 + use"vect.sml";
1.82 + use"wn.sml";
1.83 + use"eqsystem.sml";
1.84 + use"biegelinie.sml";
1.85 + use"algein.sml";
1.86 + cd "../..";
1.87 +"**** run tests on IsacKnowledge complete ****************";
1.88 +
1.89 +val path = "/home/neuper/proto2/testsml2xml/";
1.90 +pbl_hierarchy2file (path ^ "pbl/");
1.91 +pbls2file (path ^ "pbl/");
1.92 +met_hierarchy2file (path ^ "met/");
1.93 +mets2file (path ^ "met/");
1.94 +thy_hierarchy2file (path ^ "thy/");
1.95 +thes2file (path ^ "thy/");
1.96 +"**** tested creation of xmldata *************************";
1.97 +
1.98 +cd"sml";
1.99 +states:=[];
1.100 +"=========================================================";
1.101 +
1.102 +"**** run systests complete ***************** re-organize!";
1.103 +"**** run tests on math-engine complete ******************";
1.104 +"**** run tests on IsacKnowledge complete ****************";
1.105 +"**** build isac kernel + run tests complete *************";
1.106 +"**** tested creation of xmldata *************************";