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

     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"ptyps.sml";

   108  	use"generate.sml";

   109  	use"modspec.sml";

   110  	use"appl.sml";

   111  	use"script.sml";

   112  	use"solve.sml";

   113 	use"inform.sml";

   114  	cd "..";

   115  "******* build Kernel complete *******";

   116  use"states";

   117  cd "xmlsrc";

   118  	use"mathml.sml";

   119  	use"datatypes.sml";

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

   121  	use"interface-xml.sml";

   122  	cd "..";

   123  cd"FE-interface";

   124  	use"messages.sml";

   125  	use"sml.sml";

   126 	use"interface.sml";

   127  	cd "..";

   128  use"print_exn_G.sml";

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

   131  cd "IsacKnowledge";

   132  (*MG: Poly, Rational*)

   133  	use_thy"Isac";

   134  (*     remove_thy"Typefix";

   135  	remove_thy"Rational";

   136  	use_thy"IsacKnowledge/Isac";

   137 	use_thy"Isac";

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

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

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

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

   144 *)

   145  	cd "../";

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

   148  (* export of knowledge to xml

   149     > pwd();

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

   151  pbl_hierarchy2file "../xml/pbl/";

   152  pbls2file "../xml/pbl/";

   153  met_hierarchy2file "../xml/met/";

   154  mets2file "../xml/met/";

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

   156  *)

   158 (*=======================================================================**)

   160  cd "systest";

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

   162  (**       use"ctree.sml";

   163      **)

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

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

   186  cd "systest";

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

   188  	use"FE-interface.sml";

   189         use"auto-inform.sml";

   190  	use"calculate.sml";

   191 val me = meOLD;

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

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

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

   195         use"ptree.sml";

   196  	use"refine.sml";

   197  	use"root-equ.sml";

   198  	use"script.sml";

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

   200  	use"scriptnew.sml";

   201  	use"subp-rooteq.sml";

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

   203  	"******* systests complete *******";

   204  	cd "../";

   205 ----------------------------------------------------------------------*)

   207  cd"kbtest";

   208  	use"complex.sml";

   209  	use"diff.sml";

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

   211  	use"float.sml";

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

   213  	use"logexp.sml";

   214  	use"poly.sml";

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

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

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

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

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

   220  			     for simplification search MG

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

   222  	use"root.sml";

   223  	use"rooteq.sml";

   224  	use"rootrateq.sml";

   225  	use"termorder.sml";

   226  	use"trig.sml";

   227  	use"vect.sml";

   228 	use"wn.sml";

   229  	"******* kbtests complete *******";

   230  	"******* build and tests complete *******";

   231  	cd "../";

   233 (*

   234   print_depth 3;

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

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

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

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

   240 *)

   241 (**=======================================================================*)

   243  states:=[];

author	wneuper
	Thu, 03 Mar 2005 17:54:09 +0100
changeset 2143	e184eeada244
parent 2112	77696a7cf084
child 2146	de62f4a39c04
permissions	-rw-r--r--