wneuper/isa: src/Tools/isac/ROOT.ML@6c53fe2519e5

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

     2    (c) Walther Neuper 1997

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

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

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

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

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

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

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

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

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

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

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

    20 .*)

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

    23    if you store a new heap ...*)

    24 val version_isac = "WN071206-applyTacticTW";

    26 print_depth 1;(*reduces verbosity of stdout*)

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

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

    30 fun find_first _ [] = None

    31   | find_first pred (x :: xs) =

    32     if pred x then Some x else find_first pred xs;

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

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

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

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

    38 use"library.sml";

    39 use"calcelems.sml";

    40 check_guhs_unique := true;

    41 cd "Scripts";

    42  	use"term_G.sml";

    43  	use"calculate.sml";

    44  	use"rewrite.sml";

    45  	use_thy"Script";

    46 (*      remove_thy"ListG";

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

    48  	*)

    49  	use"scrtools.sml";

    50  	cd "..";

    51 cd "ME";

    52  	use"mstools.sml";

    53  	use"ctree.sml";

    54  	use"ptyps.sml";

    55  	use"generate.sml";

    56  	use"calchead.sml";

    57  	use"appl.sml";

    58  	use"rewtools.sml";

    59  	use"script.sml";

    60  	use"solve.sml";

    61 	use"inform.sml";

    62  	use"mathengine.sml";

    63  	cd "..";

    64 cd "xmlsrc";

    65  	use"mathml.sml";

    66  	use"datatypes.sml";

    67  	use"pbl-met-hierarchy.sml";

    68  	use"thy-hierarchy.sml";

    69  	use"interface-xml.sml";

    70  	cd "..";

    71 cd"FE-interface";

    72  	use"messages.sml";

    73 	use"states.sml";

    74 	use"interface.sml";

    75  	cd "..";

    76 use"print_exn_G.sml";

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

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

    80  cd "IsacKnowledge";

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

    83  (*     remove_thy"Typefix";

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

    85         *)

    86  	cd "..";

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

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

    89 check_guhs_unique := false;

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

    92 cd "systest";

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

    94        	use"root-equ.sml";

    95        	use"script.sml";

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

    97        	use"scriptnew.sml";

    98        	use"subp-rooteq.sml";

    99 	use"tacis.sml";

   100 	use"interface-xml.sml";

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

   102  	cd "../..";

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

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

   106 cd"smltest/Scripts";

   107  	use"calculate-float.sml";

   108  	use"calculate.sml";

   109 	use"listg.sml";

   110 	use"rewrite.sml";

   111  	use"scrtools.sml";

   112  	use"term_G.sml";

   113  	use"tools.sml";

   114  	cd "../..";

   115 cd"smltest/ME";

   116         use"ctree.sml";

   117        	use"calchead.sml";

   118 	use"rewtools.sml";

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

   120         use"inform.sml";

   121 	use"me.sml";

   122        	use"ptyps.sml";

   123  	cd "../..";

   124 cd"smltest/xmlsrc";

   125  	use"datatypes.sml";

   126        	use"pbl-met-hierarchy.sml";

   127        	use"thy-hierarchy.sml";

   128  	cd "../..";

   129 cd"smltest/FE-interface";

   130       	use"interface.sml";

   131  	cd "../..";

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

   133 cd"smltest/IsacKnowledge";

   134         use"atools.sml";

   135  	use"complex.sml";

   136  	use"diff.sml";

   137  	use"diffapp.sml";

   138 	use"integrate.sml";

   139 	use"equation.sml";

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

   141  	use"logexp.sml";

   142  	use"poly.sml";

   143  	use"polyminus.sml";

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

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

   146  	use"rateq.sml";

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

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

   149  			     for simplification search MG

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

   151  	use"root.sml";

   152  	use"rooteq.sml";

   153  	use"rootrateq.sml";

   154  	use"termorder.sml";

   155  	use"trig.sml";

   156  	use"vect.sml";

   157 	use"wn.sml";

   158 	use"eqsystem.sml";

   159 	use"biegelinie.sml";

   160 	use"algein.sml";

   161  	cd "../..";

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

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

   165 pbl_hierarchy2file (path ^ "pbl/");

   166 pbls2file          (path ^ "pbl/");

   167 met_hierarchy2file (path ^ "met/");

   168 mets2file          (path ^ "met/");

   169 thy_hierarchy2file (path ^ "thy/");

   170 thes2file          (path ^ "thy/");

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

   173 cd"sml";

   174 states:=[];

   175 print_depth 3;

   176 "=========================================================";

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

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

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

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

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

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

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

   188 (****************************************************************************

   189 WN.notebook: SMLNJ

   190 -----------------------------------------------------------------------------

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

   192   sml @SMLload=02-HOL-Real-isac

   193   cd"~/develop/sml/";

   194   use"ROOT.ML";

   196 *****************************************************************************

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

   198 -----------------------------------------------------------------------------

   199 su

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

   201 mv sml Isac

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

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

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

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

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

   208       ... to isab-installation vvv*)

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

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

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

   213 mv Isac sml

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

   215 exit

   217 *****************************************************************************

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

   219 -----------------------------------------------------------------------------

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

   221 @> emacs saveexec/EXPLANATIONS.tex &

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

   223 @> cd saveexec

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

   225 @> cd ..

   226 @> rm *.xml

   227 -----------------------------------------------------------------------------

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

   229 restore contents in *.xml-files:

   230 -----------------------------------------------------------------------------

   234 *****************************************************************************

   235 export of problems and methods from sml to xml

   236 -----------------------------------------------------------------------------

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

   239 > pbl_hierarchy2file (path ^ "pbl/");

   240 > pbls2file          (path ^ "pbl/");

   242 > met_hierarchy2file (path ^ "met/");

   243 > mets2file          (path ^ "met/");

   245 > thy_hierarchy2file (path ^ "thy/");

   246 > thes2file          (path ^ "thy/");

   248 *****************************************************************************

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

   250 (PolyML overwrites HOL-Real-Isac !)

   251 -----------------------------------------------------------------------------

   252   su

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

   254   rm HOL-Real-Isac

   255   cp HOL-Real HOL-Real-Isac

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

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

   258   <ctrl><d>

   259   exit

   261 *****************************************************************************;

   262 IST has another linux + polyml: create another new heap

   263 -----------------------------------------------------------------------------

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

   266  ssh ist

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

   268  rm HOL-Real-Isac

   269 		          TYPE 'yes' !!!

   270  cp HOL-Real HOL-Real-Isac

   271 			  chmod u+w HOL-Real-Isac

   272  cd ~/del_graz/sml

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

   274  use"RCODE-root.sml";

   275  <ctrl><d>

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

   277 			  chmod u-w HOL-Real-Isac

   279  logout

   280 -----------------------------------------------------------------------------

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

   282 *****************************************************************************);

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 18 Aug 2010 13:40:09 +0200
branch	isac-update-Isa09-2
changeset 37924	6c53fe2519e5
parent 37906	e2b23ba9df13
child 37926	e6fc98fbcb85
permissions	-rw-r--r--