(* Title: Run_Tests on isac

    Author: Walther Neuper 100808

    (c) due to copyright terms

 $ cd /usr/local/isabisac/src/Tools/isac

 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &

 $ /usr/local/isabisac/bin/isabelle emacs Test_Isac.thy &

 RESTART emacs after having created a new Isac heap with

 $ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac

 12345678901234567890123456789012345678901234567890123456789012345678901234567890

         10        20        30        40        50        60        70        80

 *)

 theory Test_Isac imports "Knowledge/Isac" begin

 ML{* writeln "**** run the tests **************************************" *};

 ML {* Toplevel.debug := true; *}

 (* 

 cd "systest";

 (*+ check kbtest/diffapp.sml for additional items in met-model*)

        	use"root-equ.sml"; 

        	use"script.sml";   

 	(* use"script_if.sml"; WN03 missing: is_rootequation_in*)

        	use"scriptnew.sml";     

        	use"subp-rooteq.sml";   

 	use"tacis.sml";

 	use"interface-xml.sml";

 	(* use"testdaten.sml"; no update after dropping 'errorBound'*)    

  	cd "../..";

 *)

 ML{* writeln "**** run systests complete ******************************" *};

 use"../../../test/Tools/isac/calcelems.sml"; (*complete*)

 (*

 cd"smltest/Scripts";

 *)

 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)

 use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)

 use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*)

 (*

 	use"listg.sml";

  	use"scrtools.sml";

  	use"tools.sml";

  	cd "../.."; 

 cd"smltest/ME";

 *)

 use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)

 (*      use"ctree.sml";

 *)

 use "../../../test/Tools/isac/Interpret/ptyps.sml";   (*TODO*)

 use "../../../test/Tools/isac/Interpret/calchead.sml";

 ML {*print_depth 999*}

 use "../../../test/Tools/isac/Interpret/rewtools.sml"; (**)

 (*

         use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);

         use"inform.sml";

 *)

 ML {*print_depth 5*}

 use "../../../test/Tools/isac/Interpret/mathengine.sml"; (*part.*)

 (*

 	use"me.sml";

  	cd "../.."; 

 cd"smltest/xmlsrc";

  	use"datatypes.sml";        

        	use"pbl-met-hierarchy.sml"; 

 use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml"; (**)

 *)

 use"../../../test/Tools/isac/Frontend/interface.sml"; (**)

 (*

  	cd "../..";

 *)

 ML{* writeln "**** run tests on math-engine complete ******************" *};

 (*

 cd"smltest/IsacKnowledge"; ---below the order as in theory Isac---

         use"atools.sml";

  	use"termorder.sml";

 *)

 ML {*

 print_depth 999

 *}

 ML {*print_depth 5*}

 use"../../../test/Tools/isac/Knowledge/simplify.sml"; (*part.*)

 (*

        use"poly.sml"

 *)

 use"../../../test/Tools/isac/Knowledge/rational.sml"; (*part.*)

 (*

 	use"equation.sml";

  	use"root.sml";

 *)

 use "../../../test/Tools/isac/Knowledge/inssort.sml"; (*part.*)

 (*

 	(*use"inssort.sml"; problems with recdef in Isabelle2002*)

  	use"rooteq.sml";

  	use"rateq.sml";

  	use"rootrateq.sml";

  	use"polyeq.sml";  (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN

  			     ? also check others without check 'diff.behav.'*);

  	use"rlang.sml";    (*WN.12.6.03: for TODOs search 'writeln', 

  			     for simplification search MG 

  		 erls:       98a(1) 104a(1) 104a(2) 68a *);

 	use"wn.sml";

  	use"trig.sml";

  	use"logexp.sml";

  	use"diff.sml";

 *)

 ML {*print_depth 5*}

 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*complete*)

 (*

 	use"eqsystem.sml";

 *)

 use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (* part. *)

 (*

  	use"vect.sml";  

  	use"diffapp.sml";

 	use"biegelinie.sml";

 	use"algein.sml";

 *)

 ML {*

 theory "Isac"

 *}

 use "../../../test/Tools/isac/Knowledge/isac.sml"; (**)

 ML {*print_depth 3*}

 ML {*111*}

 (*

  	cd "../..";

 *)

 (* TODO

 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"

 :

 *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"

 *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"

 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"

 *)

 use "../../../test/Pure/library.sml" (**)

 use_thy "../../../test/Pure/General/Basics"

 use_thy "../../../test/Pure/Isar/Test_Parse_Term"

 use_thy "../../../test/Pure/Isar/Test_Parsers"

 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};

 (*

 val path = "/home/neuper/proto3/testsml2xml/"; 

 pbl_hierarchy2file (path ^ "pbl/");

 pbls2file          (path ^ "pbl/");

 met_hierarchy2file (path ^ "met/");

 mets2file          (path ^ "met/");

 thy_hierarchy2file (path ^ "thy/");

 thes2file          (path ^ "thy/");

 cd"sml";

 *)

 ML{* writeln "**** tested creation of xmldata *************************" *};

 ML{*states:=[];

      writeln "=========================================================";

      writeln "**** run systests complete ***************** re-organize!";

      writeln "**** run tests on math-engine complete ******************";

      writeln "**** run tests on IsacKnowledge complete ****************";

      writeln "**** build isac kernel + run tests complete *************";

      writeln "**** tested creation of xmldata *************************";

 *}

 end

 (*=== inhibit exn ?=============================================================

 ===== inhibit exn ?===========================================================*)

 (*========== inhibit exn =======================================================

 "########### testcode inserted vvv ###########################################";

 "########### testcode inserted ^^^ ###########################################";

 ============ inhibit exn =====================================================*)

 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)