|
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 |
|
|
wneuper@59470
|
5 |
$ export ISABELLE_VERSION=2018 # for libisabelle
|
|
neuper@52139
|
6 |
|
|
neuper@55280
|
7 |
see ~~/etc/settings
|
|
neuper@52139
|
8 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
|
|
neuper@52139
|
9 |
before out-outcommenting (*, browser_info = true*) below and ...
|
|
neuper@52139
|
10 |
$ ./bin/isabelle build -o browser_info -v -c HOL
|
|
neuper@55472
|
11 |
$ ./bin/isabelle build -o browser_info -v -b Isac
|
|
wneuper@59423
|
12 |
# this creates, among others:
|
|
wneuper@59423
|
13 |
# file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
|
|
neuper@52062
|
14 |
*)
|
|
neuper@52062
|
15 |
|
|
wneuper@59462
|
16 |
(* run "./bin/isabelle build -v -b Isac" *)
|
|
neuper@52062
|
17 |
session Isac in "~~/src/Tools/isac" = HOL +
|
|
walther@59611
|
18 |
description \<open>
|
|
neuper@52062
|
19 |
Isac core, prototype of a math-engine and knowledge
|
|
neuper@52062
|
20 |
for a TP-based educational mathematics assistant.
|
|
neuper@52062
|
21 |
|
|
walther@59611
|
22 |
The java front-end is under development at FH Hagenberg,
|
|
wneuper@59470
|
23 |
the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
|
|
neuper@52062
|
24 |
See http://www.ist.tugraz.at/isac/.
|
|
walther@59611
|
25 |
\<close>
|
|
neuper@52139
|
26 |
options [document = false (*, browser_info = true*)]
|
|
wneuper@59470
|
27 |
sessions
|
|
wneuper@59470
|
28 |
Protocol (* Codec.encode etc required in mathml.sml only *)
|
|
wneuper@59470
|
29 |
theories
|
|
wneuper@59470
|
30 |
Build_Isac
|
|
wneuper@59207
|
31 |
|
|
wneuper@59470
|
32 |
(* run "./bin/isabelle build -v -b Protocol" (* generates Classy, too *)
|
|
wneuper@59470
|
33 |
"./bin/isabelle build -v -b libisabelle_Isac"
|
|
wneuper@59470
|
34 |
or just "./bin/isabelle jedit -l libisabelle_Isac & "
|
|
wneuper@59470
|
35 |
*)
|
|
wneuper@59470
|
36 |
session libisabelle_Isac in "~~/src/Tools/isac" = HOL +
|
|
walther@59611
|
37 |
description \<open>
|
|
wneuper@59207
|
38 |
Isac core, prototype of a math-engine and knowledge for engineering math
|
|
wneuper@59207
|
39 |
+ libisabelle by Lars Hupel as interface to the java front-end:
|
|
wneuper@59207
|
40 |
https://github.com/larsrh/libisabelle
|
|
wneuper@59207
|
41 |
|
|
walther@59611
|
42 |
The java front-end is under development at at FH Hagenberg,
|
|
wneuper@59470
|
43 |
the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
|
|
wneuper@59470
|
44 |
See http://www.ist.tugraz.at/isac/.
|
|
walther@59611
|
45 |
\<close>
|
|
wneuper@59207
|
46 |
options [document = false (*, browser_info = true*)]
|
|
wneuper@59469
|
47 |
sessions
|
|
wneuper@59470
|
48 |
Isac
|
|
wneuper@59469
|
49 |
theories
|
|
wneuper@59469
|
50 |
Isac_Protocol
|