(*.evaluate isac (all the code of the kernel) and isactest

   (c) Walther Neuper 1997

--------------------------------------------------------old heap on new nb

  polyisac /home/neuper/devel/isac-10/heap/HOL-Real-Isac 

--------------------------------------------------------old heap on new nb

  poly /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/HOL-Real

  cd"/home/neuper/proto2/isac/src/sml"; use"ROOT.ML";

############################# nb-setup 080917 broke the isabelle configuration; thus HOL-Real CANNOT BE RECOMPUTED todo !

  /usr/local/Isabelle2002/bin/isabelle HOL-Real

  cd"/home/neuper/proto2/isac/src/sml"; use"ROOT.ML";

############################# Rational-SK070730.ML #############

  cd"/home/neuper/proto2/isac/src/sml"; use"RCODE-root.sml";

  cd"/home/neuper/proto2/isac/src/sml"; use"RTEST-root.sml";

.*)

(*.please change HERE and in RCODE-root accordingly, 

   if you store a new heap ...*)

val version_isac = "WN071206-applyTacticTW";

print_depth 1;(*reduces verbosity of stdout*)

(*.these functions from Isabelle2002/src/Pure/library.ML are overwritten

  by some Isabelle2002 theory file; thus reestablished for isac.*)

fun find_first _ [] = NONE

  | find_first pred (x :: xs) =

    if pred x then SOME x else find_first pred xs;

fun swap (x, y) = (y, x);

(*HACK.WN080107*) val sstr = str;

"**** build the isac kernel = math-engine + IsacKnowledge ";

"**** build the math-engine ******************************";

use"library.sml";

use"calcelems.sml";

check_guhs_unique := true;

cd "Scripts";

 	use"term_G.sml";

 	use"calculate.sml";

 	use"rewrite.sml";

 	use_thy"Script";

(*      remove_thy"ListG";

 	use_thy"~/proto2/isac/src/sml/Scripts/Script";

 	*)

 	use"scrtools.sml";

 	cd ".."; 

cd "ME";

 	use"mstools.sml";

 	use"ctree.sml";

 	use"ptyps.sml"; 

 	use"generate.sml";

 	use"calchead.sml";

 	use"appl.sml";

 	use"rewtools.sml";

 	use"script.sml";

 	use"solve.sml";

	use"inform.sml"; 

 	use"mathengine.sml";

 	cd ".."; 

cd "xmlsrc";

 	use"mathml.sml";

 	use"datatypes.sml";        

 	use"pbl-met-hierarchy.sml";    

 	use"thy-hierarchy.sml";    

 	use"interface-xml.sml";

 	cd "..";

cd"FE-interface";

 	use"messages.sml";

	use"states.sml";

	use"interface.sml";

 	cd "..";

use"print_exn_G.sml";

"**** build math-engine complete *************************";

"**** build the IsacKnowledge ****************************";

 cd "IsacKnowledge";

 	use_thy"Isac"; (*evaluates ALL thys depending on the root 'Isac'*)

 (*     remove_thy"Typefix";

 	use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";

        *)

 	cd "..";

"**** build IsacKnowledge complete ***********************";

"**** build isac kernel complete *************************";

check_guhs_unique := false;

"**** run the tests **************************************";

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 "../..";

"**** run systests complete ******************************";

(*TODO copy the whole filestructure from sml to smltest*)

cd"smltest/Scripts";

 	use"calculate-float.sml";

 	use"calculate.sml";

	use"listg.sml";

	use"rewrite.sml";

 	use"scrtools.sml";

 	use"term_G.sml";

 	use"tools.sml";

 	cd "../.."; 

cd"smltest/ME";

        use"ctree.sml";

       	use"calchead.sml";

	use"rewtools.sml";

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

        use"inform.sml";

	use"me.sml";

       	use"ptyps.sml"; 

 	cd "../.."; 

cd"smltest/xmlsrc";

 	use"datatypes.sml";        

       	use"pbl-met-hierarchy.sml"; 

       	use"thy-hierarchy.sml";

 	cd "../.."; 

cd"smltest/FE-interface";

      	use"interface.sml";

 	cd "../.."; 

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

cd"smltest/IsacKnowledge";

        use"atools.sml";

 	use"complex.sml";

 	use"diff.sml";

 	use"diffapp.sml";

	use"integrate.sml";

	use"equation.sml";

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

 	use"logexp.sml";

 	use"poly.sml";

 	use"polyminus.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"rateq.sml";

 	use"rational.sml" (*TODO add_fractions_p throws overflow-exn      WN*);

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

 			     for simplification search MG 

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

 	use"root.sml";

 	use"rooteq.sml";

 	use"rootrateq.sml";

 	use"termorder.sml";

 	use"trig.sml";

 	use"vect.sml";  

	use"wn.sml";

	use"eqsystem.sml";

	use"biegelinie.sml";

	use"algein.sml";

 	cd "../.."; 

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

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

pbl_hierarchy2file (path ^ "pbl/");

pbls2file          (path ^ "pbl/");

met_hierarchy2file (path ^ "met/");

mets2file          (path ^ "met/");

thy_hierarchy2file (path ^ "thy/");

thes2file          (path ^ "thy/");

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

cd"sml";

states:=[];

print_depth 3;

"=========================================================";

"**** build math-engine complete *************************";

"**** build IsacKnowledge complete ***********************";

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

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

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

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

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

(****************************************************************************

WN.notebook: SMLNJ

-----------------------------------------------------------------------------

  cd ~/isabelle-smlnj/heaps/smlnj-110_x86-linux/

  sml @SMLload=02-HOL-Real-isac

  cd"~/develop/sml/";

  use"ROOT.ML";

*****************************************************************************

WN.notebook: create HTML representation for theory files für Isac

-----------------------------------------------------------------------------

su

cd /home/neuper/proto2/isac/src/

mv sml Isac

mv Isac/ROOT.ML Isac/ROOT.ML-save

cp Isac/RCODE-root.sml Isac/ROOT.ML

(*!!!cd"sml";!!! in ROOT.ML-save causes SysErr ("chdir failed", SOME ENOENT)*)

/usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/proto2/isac/src/Isac/

(*^^^ does not create a new heap and writes only NEW files ...

      ... to isab-installation vvv*)

cd /usr/local/Isabelle2002/browser_info/HOL/HOL-Real/

cp -r Isac/  /home/neuper/proto2/www/kbase/thy/browser_info/HOL/HOL-Real/

cd /home/neuper/proto2/isac/src/

mv Isac sml

mv sml/ROOT.ML-save sml/ROOT.ML

exit

*****************************************************************************

save and restore contents in *.xml-files; @ stands for thy | pbl | met

-----------------------------------------------------------------------------

@> grep EXPLANATIONS *.xml > saveecex/EXPLANATIONS.tex

@> emacs saveexec/EXPLANATIONS.tex &

## there search with "<EXPLANATIONS> </EXPLANATIONS>" for missing lines ...

@> cd saveexec

## ... and check with ls -l file.xml

@> cd ..

@> rm *.xml

-----------------------------------------------------------------------------

export of problems and methods from sml to xml ... see below ***

restore contents in *.xml-files:

-----------------------------------------------------------------------------

*****************************************************************************

export of problems and methods from sml to xml

-----------------------------------------------------------------------------

> val path = "/home/neuper/proto2/isac/xmldata/"; 

> pbl_hierarchy2file (path ^ "pbl/");

> pbls2file          (path ^ "pbl/");

> met_hierarchy2file (path ^ "met/");

> mets2file          (path ^ "met/");

> thy_hierarchy2file (path ^ "thy/");

> thes2file          (path ^ "thy/");

*****************************************************************************

WN.notebook: create a new heap (which is used by java in eclipse)

(PolyML overwrites HOL-Real-Isac !)

-----------------------------------------------------------------------------

  su

  cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux

  rm HOL-Real-Isac

  cp HOL-Real HOL-Real-Isac

  poly /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/HOL-Real-Isac

  cd"/home/neuper/proto2/isac/src/sml"; use"RCODE-root.sml";

  <ctrl><d>

  exit

*****************************************************************************;

IST has another linux + polyml: create another new heap 

-----------------------------------------------------------------------------

notebook:sml> scp -r ../sml wneuper@pear.ist.intra:del_graz/

 ssh ist

 cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/

 rm HOL-Real-Isac

		          TYPE 'yes' !!!

 cp HOL-Real HOL-Real-Isac

			  chmod u+w HOL-Real-Isac

 cd ~/del_graz/sml

 /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac

 use"RCODE-root.sml";

 <ctrl><d>

 cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/

			  chmod u-w HOL-Real-Isac

 logout

-----------------------------------------------------------------------------

test ist> /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac

*****************************************************************************);