wneuper/isac: src/sml/ROOT.ML@de62f4a39c04

     1 (*

     2 1.9.03,15h

     4   heaps/polyml-4.1.3_x86-linux> pwd

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

     6   heaps/polyml-4.1.3_x86-linux> ../../bin/isabelle HOL-Real-Isac

     8   cd"/netshares/commons/isac/del/Isac";

     9   use"ROOT.ML";

    11 polyml + Isabelle2003

    12   /usr/local/bin/isabelle HOL-Complex

    14 WN.notebook: SMLNJ

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

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

    17   cd"~/develop/sml/";

    18   use"ROOT.ML";

    20 WN.notebook: make HOL-Real

    21 2.10.03: ----> isac/README-nb: re-install isabelle

    23 -----------------------------------------------------------------------------

    24 WN.notebook: HTML für Isac ... ERROR

    25 --------------------------

    26   su

    27   cd /home/neuper/develop

    28   mv sml IsacScripts

    29   in ROOT.ML ab IsacKnowledge alles wegkommentieren

    30 --------------------------

    31   /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/develop/IsacScripts/

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

    33   cd"/home/neuper/develop/IsacScripts";

    34   use"ROOT.ML";

    35   <ctrl><d>  --> schreibt HOL-Real (ACHTUNG: daher VORHER HOL-Real_alt!!!!!!)

    36   neuper:/usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux#

    37                                               mv HOL-Real HOL-Real-IsacScripts

    38   emacs killen vvv

    39 --------------------------

    40   mv IsacScripts IsacKnowledge

    41   cd /home/neuper/IsacKnowledge

    42   IsacKnowledge/IsacKnowledge/ROOT.ML: !!!vvv

    43   /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real-IsacScripts /home/neuper/develop/IsacKnowledge/IsacKnowledge/

    44   > *** Unfinished parent session "HOL-Real-IsacScripts" for "IsacKnowledge" ERROR. ?????????????????????????????????????????????????????????????????????????

    45 -----------------------------------------------------------------------------

    46 WN.notebook: HTML für Isac

    47 -----------------------------------------------------------------------------

    48   su

    49   cd /home/neuper/develop

    50   mv sml Isac

    51 --------------------------

    52   /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/develop/Isac/

    53   (*^^^ does not create a new heap !!!*)

    54 -----------------------------------------------------------------------------

    55 WN.notebook: DEVELOP

    56 -----------------------------------------------------------------------------

    57  neues binary abspeichern:

    58   su

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

    60   cp HOL-Real HOL-Real-Isac

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

    62   cd"/home/neuper/proto2/isac/src/sml";

    63   use"ROOT.ML";

    65   states:=[] (*all calcs into user 1: *);

    67 ##############dev-start######################################################

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

    69   cd"~/proto2/isac/src/sml";

    70   use"ROOT.ML";

    72 ############## unten: (*systest/ctree.sml*) wegen cut_tree in ME/ctree !!!

    73 *)

    75   val version_kernel = "sml-050217a-fetchApplicableTactics";

    77   print_depth 3;

    79 (*----- Isabelle2003/src/Pure/library.ML overwritten by later Isa-code*)

    80 fun find_first _ [] = None

    81   | find_first pred (x :: xs) =

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

    83 (*----- Isabelle2003/src/Pure/library.ML overwritten by subsequent Isa-code*)

    86  use"library.sml";

    87  use"definitions.sml";

    88  cd "Scripts";

    89  	use"term_G.sml";

    90  	use"calculate.sml";

    91  	use"rewrite.sml";

    92  	use"reverse-rew.sml";

    93  	use_thy"Script";

    94 (*      remove_thy"ListG";

    95  	remove_thy"Script";

    96  	use_thy"Scripts/Script";

    98         Script.thy = {ProtoPure, ..., Real, ListG, Tools, Script}

    99         Isabelle2003  ~~~~~~~~~~~~~~~~~~~~

   100  	*)

   101  	use"scrtools.sml";

   102  	cd "..";

   103  use"globals.sml"; (*skip if re-evaluate Scripts + ME*)

   104  cd "ME";

   105  	use"mstools.sml";

   106  	use"ctree.sml";

   107 (*##**)use"ctreeNEW.sml";(**@@@@@@@@@@ -> ctree.sml !!! @@@@@@@@@@@@@@@@@*)

   108  	use"ptyps.sml";

   109  	use"generate.sml";

   110  	use"modspec.sml";

   111  	use"appl.sml";

   112  	use"script.sml";

   113  	use"solve.sml";

   114 	use"inform.sml";

   115  	cd "..";

   116  "******* build Kernel complete *******";

   117  use"states";

   118  cd "xmlsrc";

   119  	use"mathml.sml";

   120  	use"datatypes.sml";

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

   122  	use"interface-xml.sml";

   123  	cd "..";

   124  cd"FE-interface";

   125  	use"messages.sml";

   126  	use"sml.sml";

   127 	use"interface.sml";

   128  	cd "..";

   129  use"print_exn_G.sml";

   130  "******* build Kernel & XML-interface complete *******";

   132  cd "IsacKnowledge";

   133  (*MG: Poly, Rational*)

   134  	use_thy"Isac";

   135  (*     remove_thy"Typefix";

   136  	remove_thy"Rational";

   137  	use_thy"IsacKnowledge/Isac";

   138 	use_thy"Isac";

   140         Isac.thy = {ProtoPure, ..., Real, ListG, Tools, Script, ///see above

   142         Typefix, Float, ComplexI, Descript, Atools, Equation, Poly,

   143         LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq, PolyEq,

   144 	Vect, Calculus, Trig, LogExp, Diff, DiffApp, Test, Isac}

   145 *)

   146  	cd "../";

   147  "******* build Kernel & XML complete, knowledge added *******";

   149  (* export of knowledge to xml

   150     > pwd();

   151     val it = "/home/neuper/develop/sml" : string

   152  pbl_hierarchy2file "../xml/pbl/";

   153  pbls2file "../xml/pbl/";

   154  met_hierarchy2file "../xml/met/";

   155  mets2file "../xml/met/";

   156  "******* build ME & DG complete, knowledge + XML added *******";

   157  *)

   159 (*=======================================================================**)

   161  cd "systest";

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

   163         use"ctree.sml";

   164        	use"calculate.sml";

   165         use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *);

   166        	use"root-equ.sml";

   167        	use"modspec.sml";

   168        	use"script.sml";

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

   170        	use"scriptnew.sml";

   171        	use"refine.sml";

   172        	use"subp-rooteq.sml";

   173        	use"list_rls.sml";

   174 (*        use"auto-inform.sml";*)

   175 	use"tacis.sml";

   176 	use"me.sml";

   177 	use"interface-xml.sml";

   178  	use"FE-interface.sml";

   179  	(**)

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

   181  	"******* systests complete *******";

   182  	cd "../";

   183 (**=======================================================================*)

   186 (*----------list_rls.sml---##########FIXXXME.040311.doesnt work at other pos

   187  cd "systest";

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

   189  	use"FE-interface.sml";

   190         use"auto-inform.sml";

   191  	use"calculate.sml";

   192 val me = meOLD;

   193         use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *)

   194 val me = meNEW; (*see FIXXXXXME.040216*)

   195  	use"list_rls.sml"; ##########FIXXXME.040311.doesnt work at other pos

   196         use"ptree.sml";

   197  	use"refine.sml";

   198  	use"root-equ.sml";

   199  	use"script.sml";

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

   201  	use"scriptnew.sml";

   202  	use"subp-rooteq.sml";

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

   204  	"******* systests complete *******";

   205  	cd "../";

   206 ----------------------------------------------------------------------*)

   208  cd"kbtest";

   209  	use"complex.sml";

   210  	use"diff.sml";

   211  	use"diffapp.sml"  (*meNEW: fmz <> []: nxt <> Add_Relation (a/2)^2..*);

   212  	use"float.sml";

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

   214  	use"logexp.sml";

   215  	use"poly.sml";

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

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

   218  	use"rateq.sml"    (*TODO //?  8.9.03: meOLD instead meNEW !!!*);

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

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

   221  			     for simplification search MG

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

   223  	use"root.sml";

   224  	use"rooteq.sml";

   225  	use"rootrateq.sml";

   226  	use"termorder.sml";

   227  	use"trig.sml";

   228  	use"vect.sml";

   229 	use"wn.sml";

   230  	"******* kbtests complete *******";

   231  	"******* build and tests complete *******";

   232  	cd "../";

   234 (*

   235   print_depth 3;

   236   Compiler.Control.Print.printDepth:=15; (*4 default*)

   237   Compiler.Control.Print.printDepth:=9; (*4 default*)

   238   Compiler.Control.Print.printDepth:=5; (*4 default*)

   239   Compiler.Control.Print.printDepth:=4; (*4 default*)

   241 *)

   242 (**=======================================================================*)

   244  states:=[];

author	wneuper
	Fri, 04 Mar 2005 19:02:06 +0100
changeset 2146	de62f4a39c04
parent 2143	e184eeada244
child 2149	6aebd2dc2b0a
permissions	-rw-r--r--