src/Tools/isac/ROOT
author Walther Neuper <wneuper@ist.tugraz.at>
Tue, 04 Sep 2018 14:50:30 +0200
changeset 59469 5c56f14bea53
parent 59464 d7d5ce50faf2
child 59470 e11233d9b98e
permissions -rw-r--r--
Isabelle2017->18: add libisabelle, PROBLEM with session management:

/usr/local/isabisac/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start:
*** Duplicate theory "Protocol.Protocol" vs. "/usr/local/isabisac/libisabelle-protocol/libisabelle/protocol/Protocol.thy"
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
wneuper@59462
    19
(* run "./bin/isabelle build -v -b Isac" *)
neuper@52062
    20
session Isac in "~~/src/Tools/isac" = HOL +
neuper@52062
    21
  description {*
neuper@52062
    22
    Isac core, prototype of a math-engine and knowledge 
neuper@52062
    23
    for a TP-based educational mathematics assistant.
neuper@52062
    24
neuper@52062
    25
    The java front-end is under development at TU Graz,
neuper@52062
    26
    the PolyML math-engine and Isabelle knowledge at RISC Linz.
neuper@52062
    27
    See http://www.ist.tugraz.at/isac/.
neuper@52062
    28
  *}
neuper@52139
    29
  options [document = false (*, browser_info = true*)]
neuper@52062
    30
  theories Build_Isac
wneuper@59207
    31
wneuper@59207
    32
session libisabelle_Isac  = HOL +
wneuper@59207
    33
  description {*
wneuper@59207
    34
    Isac core, prototype of a math-engine and knowledge for engineering math
wneuper@59207
    35
    + libisabelle by Lars Hupel as interface to the java front-end:
wneuper@59207
    36
    https://github.com/larsrh/libisabelle
wneuper@59207
    37
                              
wneuper@59207
    38
    The java front-end is under development at TU Graz and at FH Hagenberg,
wneuper@59207
    39
    the SML math-engine and Isabelle knowledge at RISC Linz.
wneuper@59207
    40
    For installation see http://www.ist.tugraz.at/isac
wneuper@59207
    41
  *}
wneuper@59207
    42
  options [document = false (*, browser_info = true*)]
wneuper@59469
    43
  sessions
wneuper@59469
    44
    Protocol
wneuper@59469
    45
  theories
wneuper@59469
    46
    Isac_Protocol