|
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
|
|
Walther@60506
|
9 |
$ ./bin/isabelle build -o browser_info -v -b Specify
|
|
Walther@60506
|
10 |
$ ./bin/isabelle build -o browser_info -v -b Interpret
|
|
neuper@55472
|
11 |
$ ./bin/isabelle build -o browser_info -v -b Isac
|
|
wneuper@59423
|
12 |
# this creates, among others:
|
|
Walther@60506
|
13 |
# file:///home/walthern/.isabelle/isabisac/browser_info/HOL/index.html
|
|
Walther@60506
|
14 |
# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/index.html
|
|
Walther@60506
|
15 |
# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Specify/session_graph.pdf
|
|
Walther@60506
|
16 |
# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Interpret/session_graph.pdf
|
|
Walther@60506
|
17 |
# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
|
|
neuper@52062
|
18 |
*)
|
|
walther@60077
|
19 |
|
|
walther@60182
|
20 |
(* run "./bin/isabelle build -v -b Specify" *)
|
|
wenzelm@60200
|
21 |
session Specify in Specify = HOL +
|
|
walther@60077
|
22 |
description "
|
|
walther@60182
|
23 |
Session covering code required for ~~/src/Tools/isac/Doc/Specify_Phase
|
|
walther@60077
|
24 |
"
|
|
wenzelm@60217
|
25 |
options [isac_test = false, document = false (** ), browser_info = true( **)]
|
|
walther@60077
|
26 |
directories
|
|
walther@60077
|
27 |
"../BaseDefinitions"
|
|
walther@60077
|
28 |
"../ProgLang"
|
|
walther@60077
|
29 |
"../MathEngBasic"
|
|
walther@60072
|
30 |
theories
|
|
walther@60077
|
31 |
"../BaseDefinitions/BaseDefinitions"
|
|
walther@60077
|
32 |
"../ProgLang/ProgLang"
|
|
walther@60077
|
33 |
"../MathEngBasic/MathEngBasic"
|
|
walther@60182
|
34 |
"Specify"
|
|
walther@60182
|
35 |
|
|
walther@60182
|
36 |
(* run "./bin/isabelle build -v -b Interpret" *)
|
|
walther@60182
|
37 |
session Interpret in Interpret = Specify +
|
|
walther@60182
|
38 |
description "
|
|
walther@60182
|
39 |
Session covering code required for ~~/src/Tools/isac/Doc/Lucas_Interpreter
|
|
walther@60182
|
40 |
"
|
|
wenzelm@60217
|
41 |
options [isac_test = false, document = false (** ), browser_info = true( **)]
|
|
walther@60182
|
42 |
theories
|
|
walther@60077
|
43 |
"Interpret"
|
|
walther@60077
|
44 |
|
|
walther@60080
|
45 |
(* run "./bin/isabelle build -v -b Isac" *)
|
|
walther@60098
|
46 |
session Isac = Interpret +
|
|
walther@60077
|
47 |
description "
|
|
neuper@52062
|
48 |
Isac core, prototype of a math-engine and knowledge
|
|
neuper@52062
|
49 |
for a TP-based educational mathematics assistant.
|
|
walther@60077
|
50 |
"
|
|
wenzelm@60217
|
51 |
options [isac_test = false, document = false (** ), browser_info = true( **)]
|
|
walther@60077
|
52 |
directories
|
|
walther@60077
|
53 |
"MathEngine"
|
|
walther@60077
|
54 |
"Test_Code"
|
|
walther@60077
|
55 |
"BridgeLibisabelle"
|
|
walther@60077
|
56 |
"BridgeJEdit"
|
|
walther@60077
|
57 |
"Knowledge"
|
|
walther@60077
|
58 |
theories
|
|
walther@60077
|
59 |
"MathEngine/MathEngine"
|
|
walther@60077
|
60 |
"Test_Code/Test_Code"
|
|
walther@60077
|
61 |
"BridgeLibisabelle/BridgeLibisabelle"
|
|
walther@60077
|
62 |
"BridgeJEdit/BridgeJEdit"
|
|
walther@60077
|
63 |
"Knowledge/Build_Thydata"
|
|
walther@60077
|
64 |
"Build_Isac"
|