|
neuper@52062
|
1 |
(* Title: create a heap image for isac on Isabelle2013
|
|
neuper@52062
|
2 |
Author: Walther Neuper, TU Graz, 130715
|
|
neuper@52062
|
3 |
(c) due to copyright terms
|
|
neuper@52062
|
4 |
|
|
neuper@55280
|
5 |
see ~~/etc/settings
|
|
neuper@52139
|
6 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
|
|
neuper@52139
|
7 |
before out-outcommenting (*, browser_info = true*) below and ...
|
|
neuper@52139
|
8 |
$ ./bin/isabelle build -o browser_info -v -c HOL
|
|
neuper@55472
|
9 |
$ ./bin/isabelle build -o browser_info -v -b Isac
|
|
wneuper@59423
|
10 |
# this creates, among others:
|
|
wneuper@59423
|
11 |
# file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
|
|
neuper@52062
|
12 |
*)
|
|
walther@60077
|
13 |
|
|
walther@60182
|
14 |
(* run "./bin/isabelle build -v -b Specify" *)
|
|
walther@60182
|
15 |
session Specify in Specify = "HOL-SPARK" +
|
|
walther@60077
|
16 |
description "
|
|
walther@60182
|
17 |
Session covering code required for ~~/src/Tools/isac/Doc/Specify_Phase
|
|
walther@60077
|
18 |
"
|
|
walther@60149
|
19 |
options [document = false (** ), browser_info = true( **)]
|
|
walther@60077
|
20 |
directories
|
|
walther@60077
|
21 |
"../BaseDefinitions"
|
|
walther@60077
|
22 |
"../ProgLang"
|
|
walther@60077
|
23 |
"../MathEngBasic"
|
|
walther@60072
|
24 |
theories
|
|
walther@60077
|
25 |
"../BaseDefinitions/BaseDefinitions"
|
|
walther@60077
|
26 |
"../ProgLang/ProgLang"
|
|
walther@60077
|
27 |
"../MathEngBasic/MathEngBasic"
|
|
walther@60182
|
28 |
"Specify"
|
|
walther@60182
|
29 |
|
|
walther@60182
|
30 |
(* run "./bin/isabelle build -v -b Interpret" *)
|
|
walther@60182
|
31 |
session Interpret in Interpret = Specify +
|
|
walther@60182
|
32 |
description "
|
|
walther@60182
|
33 |
Session covering code required for ~~/src/Tools/isac/Doc/Lucas_Interpreter
|
|
walther@60182
|
34 |
"
|
|
walther@60182
|
35 |
options [document = false (** ), browser_info = true( **)]
|
|
walther@60182
|
36 |
theories
|
|
walther@60077
|
37 |
"Interpret"
|
|
walther@60077
|
38 |
|
|
walther@60080
|
39 |
(* run "./bin/isabelle build -v -b Isac" *)
|
|
walther@60098
|
40 |
session Isac = Interpret +
|
|
walther@60077
|
41 |
description "
|
|
neuper@52062
|
42 |
Isac core, prototype of a math-engine and knowledge
|
|
neuper@52062
|
43 |
for a TP-based educational mathematics assistant.
|
|
walther@60077
|
44 |
"
|
|
walther@60149
|
45 |
options [document = false (** ), browser_info = true( **)]
|
|
walther@60077
|
46 |
directories
|
|
walther@60077
|
47 |
"MathEngine"
|
|
walther@60077
|
48 |
"Test_Code"
|
|
walther@60077
|
49 |
"BridgeLibisabelle"
|
|
walther@60077
|
50 |
"BridgeJEdit"
|
|
walther@60077
|
51 |
"Knowledge"
|
|
walther@60077
|
52 |
theories
|
|
walther@60077
|
53 |
"MathEngine/MathEngine"
|
|
walther@60077
|
54 |
"Test_Code/Test_Code"
|
|
walther@60077
|
55 |
"BridgeLibisabelle/BridgeLibisabelle"
|
|
walther@60077
|
56 |
"BridgeJEdit/BridgeJEdit"
|
|
walther@60077
|
57 |
"Knowledge/Build_Thydata"
|
|
walther@60077
|
58 |
"Build_Isac"
|
|
walther@60189
|
59 |
|
|
walther@60189
|
60 |
(*~~$ ./bin/isabelle build -v -b Doc #check ok, no output
|
|
walther@60189
|
61 |
*)
|
|
walther@60189
|
62 |
session Doc in Doc = Interpret +
|
|
walther@60189
|
63 |
description "
|
|
walther@60189
|
64 |
Formally checked documentation for Isac in analogy to ~~/Doc/.
|
|
walther@60189
|
65 |
"
|
|
walther@60189
|
66 |
options [document = false (*, browser_info = true*)]
|
|
walther@60189
|
67 |
directories
|
|
walther@60189
|
68 |
"Lucas_Interpreter"
|
|
walther@60189
|
69 |
"Specify_Phase"
|
|
walther@60189
|
70 |
theories
|
|
walther@60189
|
71 |
"Lucas_Interpreter/Lucas_Interpreter"
|
|
walther@60189
|
72 |
"Specify_Phase/Specify_Phase"
|
|
walther@60189
|
73 |
|