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