|
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@59423
|
5 |
$ export ISABELLE_VERSION=2017 # for libisabelle
|
|
neuper@52062
|
6 |
$ cd /usr/local/isabisac/
|
|
neuper@55280
|
7 |
$ ./bin/isabelle build -v -b Isac
|
|
wneuper@59346
|
8 |
$ ./bin/isabelle build -v -b libisabelle_Isac
|
|
neuper@52139
|
9 |
|
|
neuper@55280
|
10 |
see ~~/etc/settings
|
|
neuper@52139
|
11 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
|
|
neuper@52139
|
12 |
before out-outcommenting (*, browser_info = true*) below and ...
|
|
neuper@52139
|
13 |
$ ./bin/isabelle build -o browser_info -v -c HOL
|
|
neuper@55472
|
14 |
$ ./bin/isabelle build -o browser_info -v -b Isac
|
|
wneuper@59423
|
15 |
# this creates, among others:
|
|
wneuper@59423
|
16 |
# file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
|
|
neuper@52062
|
17 |
*)
|
|
neuper@52062
|
18 |
|
|
neuper@52062
|
19 |
session Isac in "~~/src/Tools/isac" = HOL +
|
|
neuper@52062
|
20 |
description {*
|
|
neuper@52062
|
21 |
Isac core, prototype of a math-engine and knowledge
|
|
neuper@52062
|
22 |
for a TP-based educational mathematics assistant.
|
|
neuper@52062
|
23 |
|
|
neuper@52062
|
24 |
The java front-end is under development at TU Graz,
|
|
neuper@52062
|
25 |
the PolyML math-engine and Isabelle knowledge at RISC Linz.
|
|
neuper@52062
|
26 |
See http://www.ist.tugraz.at/isac/.
|
|
neuper@52062
|
27 |
*}
|
|
neuper@52139
|
28 |
options [document = false (*, browser_info = true*)]
|
|
neuper@52062
|
29 |
theories Build_Isac
|
|
wneuper@59207
|
30 |
|
|
wneuper@59207
|
31 |
session libisabelle_Isac = HOL +
|
|
wneuper@59207
|
32 |
description {*
|
|
wneuper@59207
|
33 |
Isac core, prototype of a math-engine and knowledge for engineering math
|
|
wneuper@59207
|
34 |
+ libisabelle by Lars Hupel as interface to the java front-end:
|
|
wneuper@59207
|
35 |
https://github.com/larsrh/libisabelle
|
|
wneuper@59207
|
36 |
|
|
wneuper@59207
|
37 |
The java front-end is under development at TU Graz and at FH Hagenberg,
|
|
wneuper@59207
|
38 |
the SML math-engine and Isabelle knowledge at RISC Linz.
|
|
wneuper@59207
|
39 |
For installation see http://www.ist.tugraz.at/isac
|
|
wneuper@59207
|
40 |
*}
|
|
wneuper@59207
|
41 |
options [document = false (*, browser_info = true*)]
|
|
wneuper@59216
|
42 |
theories Isac_Protocol
|
|
wneuper@59346
|
43 |
"~~/libisabelle-protocol/libisabelle/protocol/Protocol"
|