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