src/Tools/isac/RTEST-root.sml
branchisac-update-Isa09-2
changeset 37906 e2b23ba9df13
     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 *************************";