1.1 --- a/src/Tools/isac/RTEST-root.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,103 +0,0 @@
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 *************************";