1 (*.evaluate isac (all the code of the kernel) and isactest |
|
2 (c) Walther Neuper 1997 |
|
3 |
|
4 /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac |
|
5 |
|
6 /usr/local/Isabelle2002/bin/isabelle HOL-Real |
|
7 cd"~/proto2/isac/src/sml"; use"RCODE-root.sml"; |
|
8 |
|
9 use"ROOT.ML"; |
|
10 use"RTEST-root.sml"; |
|
11 .*) |
|
12 |
|
13 (*.please change HERE and in ROOT.ML accordingly, |
|
14 if you store a new heap ...*) |
|
15 val version_isac = "WN0710-calcResponse"; |
|
16 |
|
17 print_depth 1;(*reduces verbosity of stdout*) |
|
18 |
|
19 (*.this function from Isabelle2002/src/Pure/library.ML is overwritten |
|
20 by some Isabelle2002 theory file; thus reestablished for isac.*) |
|
21 fun find_first _ [] = NONE |
|
22 | find_first pred (x :: xs) = |
|
23 if pred x then SOME x else find_first pred xs; |
|
24 fun swap (x, y) = (y, x); |
|
25 (*HACK.WN080107*) val sstr = str; |
|
26 |
|
27 "**** build the isac kernel = math-engine + IsacKnowledge "; |
|
28 "**** build the math-engine ******************************"; |
|
29 use"library.sml"; |
|
30 use"calcelems.sml"; |
|
31 cd "Scripts"; |
|
32 use"term_G.sml"; |
|
33 use"calculate.sml"; |
|
34 use"rewrite.sml"; |
|
35 use_thy"Script"; |
|
36 (* remove_thy"ListG"; |
|
37 use_thy"~/proto2/isac/src/sml/Scripts/Script"; |
|
38 *) |
|
39 use"scrtools.sml"; |
|
40 cd ".."; |
|
41 cd "ME"; |
|
42 use"mstools.sml"; |
|
43 use"ctree.sml"; |
|
44 use"ptyps.sml"; |
|
45 use"generate.sml"; |
|
46 use"calchead.sml"; |
|
47 use"appl.sml"; |
|
48 use"rewtools.sml"; |
|
49 use"script.sml"; |
|
50 use"solve.sml"; |
|
51 use"inform.sml"; |
|
52 use"mathengine.sml"; |
|
53 cd ".."; |
|
54 cd "xmlsrc"; |
|
55 use"mathml.sml"; |
|
56 use"datatypes.sml"; |
|
57 use"pbl-met-hierarchy.sml"; |
|
58 use"thy-hierarchy.sml"; |
|
59 use"interface-xml.sml"; |
|
60 cd ".."; |
|
61 cd"FE-interface"; |
|
62 use"messages.sml"; |
|
63 use"states.sml"; |
|
64 use"interface.sml"; |
|
65 cd ".."; |
|
66 use"print_exn_G.sml"; |
|
67 "**** build math-engine complete *************************"; |
|
68 |
|
69 "**** build the IsacKnowledge ****************************"; |
|
70 cd "IsacKnowledge"; |
|
71 use_thy"Isac"; (*evaluates ALL thys depending on the root 'Isac'*) |
|
72 |
|
73 (* remove_thy"Typefix"; |
|
74 use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac"; |
|
75 *) |
|
76 cd ".."; |
|
77 "**** build IsacKnowledge complete ***********************"; |
|
78 "**** build isac kernel complete *************************"; |
|
79 |
|
80 states:=[]; |
|
81 print_depth 3; |
|