1.1 --- a/src/Tools/isac/ROOT.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,282 +0,0 @@
1.4 -(*.evaluate isac (all the code of the kernel) and isactest
1.5 - (c) Walther Neuper 1997
1.6 -
1.7 ---------------------------------------------------------old heap on new nb
1.8 - polyisac /home/neuper/devel/isac-10/heap/HOL-Real-Isac
1.9 ---------------------------------------------------------old heap on new nb
1.10 -
1.11 - poly /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/HOL-Real
1.12 - cd"/home/neuper/proto2/isac/src/sml"; use"ROOT.ML";
1.13 -
1.14 -############################# nb-setup 080917 broke the isabelle configuration; thus HOL-Real CANNOT BE RECOMPUTED todo !
1.15 -
1.16 - /usr/local/Isabelle2002/bin/isabelle HOL-Real
1.17 - cd"/home/neuper/proto2/isac/src/sml"; use"ROOT.ML";
1.18 -
1.19 -############################# Rational-SK070730.ML #############
1.20 -
1.21 - cd"/home/neuper/proto2/isac/src/sml"; use"RCODE-root.sml";
1.22 - cd"/home/neuper/proto2/isac/src/sml"; use"RTEST-root.sml";
1.23 -.*)
1.24 -
1.25 -(*.please change HERE and in RCODE-root accordingly,
1.26 - if you store a new heap ...*)
1.27 -val version_isac = "WN071206-applyTacticTW";
1.28 -
1.29 -print_depth 1;(*reduces verbosity of stdout*)
1.30 -
1.31 -(*.these functions from Isabelle2002/src/Pure/library.ML are overwritten
1.32 - by some Isabelle2002 theory file; thus reestablished for isac.*)
1.33 -fun find_first _ [] = NONE
1.34 - | find_first pred (x :: xs) =
1.35 - if pred x then SOME x else find_first pred xs;
1.36 -fun swap (x, y) = (y, x);
1.37 -(*HACK.WN080107*) val sstr = str;
1.38 -
1.39 -"**** build the isac kernel = math-engine + IsacKnowledge ";
1.40 -"**** build the math-engine ******************************";
1.41 -use"library.sml";
1.42 -use"calcelems.sml";
1.43 -check_guhs_unique := true;
1.44 -cd "Scripts";
1.45 - use"term_G.sml";
1.46 - use"calculate.sml";
1.47 - use"rewrite.sml";
1.48 - use_thy"Script";
1.49 -(* remove_thy"ListG";
1.50 - use_thy"~/proto2/isac/src/sml/Scripts/Script";
1.51 - *)
1.52 - use"scrtools.sml";
1.53 - cd "..";
1.54 -cd "ME";
1.55 - use"mstools.sml";
1.56 - use"ctree.sml";
1.57 - use"ptyps.sml";
1.58 - use"generate.sml";
1.59 - use"calchead.sml";
1.60 - use"appl.sml";
1.61 - use"rewtools.sml";
1.62 - use"script.sml";
1.63 - use"solve.sml";
1.64 - use"inform.sml";
1.65 - use"mathengine.sml";
1.66 - cd "..";
1.67 -cd "xmlsrc";
1.68 - use"mathml.sml";
1.69 - use"datatypes.sml";
1.70 - use"pbl-met-hierarchy.sml";
1.71 - use"thy-hierarchy.sml";
1.72 - use"interface-xml.sml";
1.73 - cd "..";
1.74 -cd"FE-interface";
1.75 - use"messages.sml";
1.76 - use"states.sml";
1.77 - use"interface.sml";
1.78 - cd "..";
1.79 -use"print_exn_G.sml";
1.80 -"**** build math-engine complete *************************";
1.81 -
1.82 -"**** build the IsacKnowledge ****************************";
1.83 - cd "IsacKnowledge";
1.84 - use_thy"Isac"; (*evaluates ALL thys depending on the root 'Isac'*)
1.85 -
1.86 - (* remove_thy"Typefix";
1.87 - use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";
1.88 - *)
1.89 - cd "..";
1.90 -"**** build IsacKnowledge complete ***********************";
1.91 -"**** build isac kernel complete *************************";
1.92 -check_guhs_unique := false;
1.93 -
1.94 -"**** run the tests **************************************";
1.95 -cd "systest";
1.96 -(*+ check kbtest/diffapp.sml for additional items in met-model*)
1.97 - use"root-equ.sml";
1.98 - use"script.sml";
1.99 - (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
1.100 - use"scriptnew.sml";
1.101 - use"subp-rooteq.sml";
1.102 - use"tacis.sml";
1.103 - use"interface-xml.sml";
1.104 - (* use"testdaten.sml"; no update after dropping 'errorBound'*)
1.105 - cd "../..";
1.106 -"**** run systests complete ******************************";
1.107 -(*TODO copy the whole filestructure from sml to smltest*)
1.108 -
1.109 -cd"smltest/Scripts";
1.110 - use"calculate-float.sml";
1.111 - use"calculate.sml";
1.112 - use"listg.sml";
1.113 - use"rewrite.sml";
1.114 - use"scrtools.sml";
1.115 - use"term_G.sml";
1.116 - use"tools.sml";
1.117 - cd "../..";
1.118 -cd"smltest/ME";
1.119 - use"ctree.sml";
1.120 - use"calchead.sml";
1.121 - use"rewtools.sml";
1.122 - use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
1.123 - use"inform.sml";
1.124 - use"me.sml";
1.125 - use"ptyps.sml";
1.126 - cd "../..";
1.127 -cd"smltest/xmlsrc";
1.128 - use"datatypes.sml";
1.129 - use"pbl-met-hierarchy.sml";
1.130 - use"thy-hierarchy.sml";
1.131 - cd "../..";
1.132 -cd"smltest/FE-interface";
1.133 - use"interface.sml";
1.134 - cd "../..";
1.135 -"**** run tests on math-engine complete ******************";
1.136 -cd"smltest/IsacKnowledge";
1.137 - use"atools.sml";
1.138 - use"complex.sml";
1.139 - use"diff.sml";
1.140 - use"diffapp.sml";
1.141 - use"integrate.sml";
1.142 - use"equation.sml";
1.143 - (*use"inssort.sml"; problems with recdef in Isabelle2002*)
1.144 - use"logexp.sml";
1.145 - use"poly.sml";
1.146 - use"polyminus.sml";
1.147 - use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
1.148 - ? also check others without check 'diff.behav.'*);
1.149 - use"rateq.sml";
1.150 - use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
1.151 - use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
1.152 - for simplification search MG
1.153 - erls: 98a(1) 104a(1) 104a(2) 68a *);
1.154 - use"root.sml";
1.155 - use"rooteq.sml";
1.156 - use"rootrateq.sml";
1.157 - use"termorder.sml";
1.158 - use"trig.sml";
1.159 - use"vect.sml";
1.160 - use"wn.sml";
1.161 - use"eqsystem.sml";
1.162 - use"biegelinie.sml";
1.163 - use"algein.sml";
1.164 - cd "../..";
1.165 -"**** run tests on IsacKnowledge complete ****************";
1.166 -
1.167 -val path = "/home/neuper/proto2/testsml2xml/";
1.168 -pbl_hierarchy2file (path ^ "pbl/");
1.169 -pbls2file (path ^ "pbl/");
1.170 -met_hierarchy2file (path ^ "met/");
1.171 -mets2file (path ^ "met/");
1.172 -thy_hierarchy2file (path ^ "thy/");
1.173 -thes2file (path ^ "thy/");
1.174 -"**** tested creation of xmldata *************************";
1.175 -
1.176 -cd"sml";
1.177 -states:=[];
1.178 -print_depth 3;
1.179 -"=========================================================";
1.180 -
1.181 -"**** build math-engine complete *************************";
1.182 -"**** build IsacKnowledge complete ***********************";
1.183 -"**** run systests complete ***************** re-organize!";
1.184 -"**** run tests on math-engine complete ******************";
1.185 -"**** run tests on IsacKnowledge complete ****************";
1.186 -"**** tested creation of xmldata *************************";
1.187 -"**** build isac kernel + run tests complete *************";
1.188 -
1.189 -
1.190 -
1.191 -(****************************************************************************
1.192 -WN.notebook: SMLNJ
1.193 ------------------------------------------------------------------------------
1.194 - cd ~/isabelle-smlnj/heaps/smlnj-110_x86-linux/
1.195 - sml @SMLload=02-HOL-Real-isac
1.196 - cd"~/develop/sml/";
1.197 - use"ROOT.ML";
1.198 -
1.199 -*****************************************************************************
1.200 -WN.notebook: create HTML representation for theory files für Isac
1.201 ------------------------------------------------------------------------------
1.202 -su
1.203 -cd /home/neuper/proto2/isac/src/
1.204 -mv sml Isac
1.205 -mv Isac/ROOT.ML Isac/ROOT.ML-save
1.206 -cp Isac/RCODE-root.sml Isac/ROOT.ML
1.207 -(*!!!cd"sml";!!! in ROOT.ML-save causes SysErr ("chdir failed", SOME ENOENT)*)
1.208 -
1.209 -/usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/proto2/isac/src/Isac/
1.210 -(*^^^ does not create a new heap and writes only NEW files ...
1.211 - ... to isab-installation vvv*)
1.212 -cd /usr/local/Isabelle2002/browser_info/HOL/HOL-Real/
1.213 -cp -r Isac/ /home/neuper/proto2/www/kbase/thy/browser_info/HOL/HOL-Real/
1.214 -
1.215 -cd /home/neuper/proto2/isac/src/
1.216 -mv Isac sml
1.217 -mv sml/ROOT.ML-save sml/ROOT.ML
1.218 -exit
1.219 -
1.220 -*****************************************************************************
1.221 -save and restore contents in *.xml-files; @ stands for thy | pbl | met
1.222 ------------------------------------------------------------------------------
1.223 -@> grep EXPLANATIONS *.xml > saveecex/EXPLANATIONS.tex
1.224 -@> emacs saveexec/EXPLANATIONS.tex &
1.225 -## there search with "<EXPLANATIONS> </EXPLANATIONS>" for missing lines ...
1.226 -@> cd saveexec
1.227 -## ... and check with ls -l file.xml
1.228 -@> cd ..
1.229 -@> rm *.xml
1.230 ------------------------------------------------------------------------------
1.231 -export of problems and methods from sml to xml ... see below ***
1.232 -restore contents in *.xml-files:
1.233 ------------------------------------------------------------------------------
1.234 -
1.235 -
1.236 -
1.237 -*****************************************************************************
1.238 -export of problems and methods from sml to xml
1.239 ------------------------------------------------------------------------------
1.240 -> val path = "/home/neuper/proto2/isac/xmldata/";
1.241 -
1.242 -> pbl_hierarchy2file (path ^ "pbl/");
1.243 -> pbls2file (path ^ "pbl/");
1.244 -
1.245 -> met_hierarchy2file (path ^ "met/");
1.246 -> mets2file (path ^ "met/");
1.247 -
1.248 -> thy_hierarchy2file (path ^ "thy/");
1.249 -> thes2file (path ^ "thy/");
1.250 -
1.251 -*****************************************************************************
1.252 -WN.notebook: create a new heap (which is used by java in eclipse)
1.253 -(PolyML overwrites HOL-Real-Isac !)
1.254 ------------------------------------------------------------------------------
1.255 - su
1.256 - cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux
1.257 - rm HOL-Real-Isac
1.258 - cp HOL-Real HOL-Real-Isac
1.259 - poly /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/HOL-Real-Isac
1.260 - cd"/home/neuper/proto2/isac/src/sml"; use"RCODE-root.sml";
1.261 - <ctrl><d>
1.262 - exit
1.263 -
1.264 -*****************************************************************************;
1.265 -IST has another linux + polyml: create another new heap
1.266 ------------------------------------------------------------------------------
1.267 -notebook:sml> scp -r ../sml wneuper@pear.ist.intra:del_graz/
1.268 -
1.269 - ssh ist
1.270 - cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/
1.271 - rm HOL-Real-Isac
1.272 - TYPE 'yes' !!!
1.273 - cp HOL-Real HOL-Real-Isac
1.274 - chmod u+w HOL-Real-Isac
1.275 - cd ~/del_graz/sml
1.276 - /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
1.277 - use"RCODE-root.sml";
1.278 - <ctrl><d>
1.279 - cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/
1.280 - chmod u-w HOL-Real-Isac
1.281 -
1.282 - logout
1.283 ------------------------------------------------------------------------------
1.284 -test ist> /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
1.285 -*****************************************************************************);