author | Walther Neuper <wneuper@ist.tugraz.at> |
Tue, 06 Feb 2018 15:24:03 +0100 | |
changeset 59346 | bf5ca91db537 |
parent 59320 | 4549c6062b30 |
child 59423 | e1b34eb27309 |
permissions | -rw-r--r-- |
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@59320 | 5 |
$ export ISABELLE_VERSION=2015 # 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 |
neuper@52062 | 15 |
*) |
neuper@52062 | 16 |
|
neuper@52062 | 17 |
session Isac in "~~/src/Tools/isac" = HOL + |
neuper@52062 | 18 |
description {* |
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 |
|
neuper@52062 | 22 |
The java front-end is under development at TU Graz, |
neuper@52062 | 23 |
the PolyML math-engine and Isabelle knowledge at RISC Linz. |
neuper@52062 | 24 |
See http://www.ist.tugraz.at/isac/. |
neuper@52062 | 25 |
*} |
neuper@52139 | 26 |
options [document = false (*, browser_info = true*)] |
neuper@52062 | 27 |
theories Build_Isac |
wneuper@59207 | 28 |
|
wneuper@59207 | 29 |
session libisabelle_Isac = HOL + |
wneuper@59207 | 30 |
description {* |
wneuper@59207 | 31 |
Isac core, prototype of a math-engine and knowledge for engineering math |
wneuper@59207 | 32 |
+ libisabelle by Lars Hupel as interface to the java front-end: |
wneuper@59207 | 33 |
https://github.com/larsrh/libisabelle |
wneuper@59207 | 34 |
|
wneuper@59207 | 35 |
The java front-end is under development at TU Graz and at FH Hagenberg, |
wneuper@59207 | 36 |
the SML math-engine and Isabelle knowledge at RISC Linz. |
wneuper@59207 | 37 |
For installation see http://www.ist.tugraz.at/isac |
wneuper@59207 | 38 |
*} |
wneuper@59207 | 39 |
options [document = false (*, browser_info = true*)] |
wneuper@59216 | 40 |
theories Isac_Protocol |
wneuper@59346 | 41 |
"~~/libisabelle-protocol/libisabelle/protocol/Protocol" |