1 (*.evaluate isac (all the code of the kernel) and isactest |
|
2 (c) Walther Neuper 1997 |
|
3 |
|
4 --------------------------------------------------------old heap on new nb |
|
5 polyisac /home/neuper/devel/isac-10/heap/HOL-Real-Isac |
|
6 --------------------------------------------------------old heap on new nb |
|
7 |
|
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"; |
|
10 |
|
11 ############################# nb-setup 080917 broke the isabelle configuration; thus HOL-Real CANNOT BE RECOMPUTED todo ! |
|
12 |
|
13 /usr/local/Isabelle2002/bin/isabelle HOL-Real |
|
14 cd"/home/neuper/proto2/isac/src/sml"; use"ROOT.ML"; |
|
15 |
|
16 ############################# Rational-SK070730.ML ############# |
|
17 |
|
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 .*) |
|
21 |
|
22 (*.please change HERE and in RCODE-root accordingly, |
|
23 if you store a new heap ...*) |
|
24 val version_isac = "WN071206-applyTacticTW"; |
|
25 |
|
26 print_depth 1;(*reduces verbosity of stdout*) |
|
27 |
|
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; |
|
35 |
|
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 *************************"; |
|
78 |
|
79 "**** build the IsacKnowledge ****************************"; |
|
80 cd "IsacKnowledge"; |
|
81 use_thy"Isac"; (*evaluates ALL thys depending on the root 'Isac'*) |
|
82 |
|
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; |
|
90 |
|
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*) |
|
105 |
|
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 ****************"; |
|
163 |
|
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 *************************"; |
|
172 |
|
173 cd"sml"; |
|
174 states:=[]; |
|
175 print_depth 3; |
|
176 "========================================================="; |
|
177 |
|
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 *************"; |
|
185 |
|
186 |
|
187 |
|
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"; |
|
195 |
|
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)*) |
|
205 |
|
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/ |
|
211 |
|
212 cd /home/neuper/proto2/isac/src/ |
|
213 mv Isac sml |
|
214 mv sml/ROOT.ML-save sml/ROOT.ML |
|
215 exit |
|
216 |
|
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 ----------------------------------------------------------------------------- |
|
231 |
|
232 |
|
233 |
|
234 ***************************************************************************** |
|
235 export of problems and methods from sml to xml |
|
236 ----------------------------------------------------------------------------- |
|
237 > val path = "/home/neuper/proto2/isac/xmldata/"; |
|
238 |
|
239 > pbl_hierarchy2file (path ^ "pbl/"); |
|
240 > pbls2file (path ^ "pbl/"); |
|
241 |
|
242 > met_hierarchy2file (path ^ "met/"); |
|
243 > mets2file (path ^ "met/"); |
|
244 |
|
245 > thy_hierarchy2file (path ^ "thy/"); |
|
246 > thes2file (path ^ "thy/"); |
|
247 |
|
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 |
|
260 |
|
261 *****************************************************************************; |
|
262 IST has another linux + polyml: create another new heap |
|
263 ----------------------------------------------------------------------------- |
|
264 notebook:sml> scp -r ../sml wneuper@pear.ist.intra:del_graz/ |
|
265 |
|
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 |
|
278 |
|
279 logout |
|
280 ----------------------------------------------------------------------------- |
|
281 test ist> /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac |
|
282 *****************************************************************************); |
|