wneuper/isa: src/Tools/isac/ROOT@6103433242cb

     1 (*  Title:  create a heap image for isac on Isabelle2013

     2     Author: Walther Neuper, TU Graz, 130715

     3    (c) due to copyright terms

     5 see ~~/etc/settings

     6   ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"

     7 before out-outcommenting (*, browser_info = true*) below and ...

     8 $ ./bin/isabelle build -o browser_info -v -c HOL

     9 $ ./bin/isabelle build -o browser_info -v -b Isac

    10 # this creates, among others:

    11 # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf

    12 *)

    14 (* run "./bin/isabelle build -v -b Interpret" *)

    15 session Interpret in Interpret = HOL +

    16   description "

    17     Session covering code required for ~~/src/Tools/isac/Doc.

    18   "

    19   options [document = false (*, browser_info = true*)]

    20   directories

    21     "../BaseDefinitions"

    22     "../ProgLang"

    23     "../MathEngBasic"

    24     "../Specify"

    25   theories

    26     "../BaseDefinitions/BaseDefinitions"

    27     "../ProgLang/ProgLang"

    28     "../MathEngBasic/MathEngBasic"

    29     "../Specify/Specify"

    30     "Interpret"

    32 (* run "./bin/isabelle build -v -b Isac"  *)

    33 session Isac = Interpret +

    34   description "

    35     Isac core, prototype of a math-engine and knowledge

    36     for a TP-based educational mathematics assistant.

    37   "

    38   options [document = false (*, browser_info = true*)]

    39   directories

    40     "MathEngine"

    41     "Test_Code"

    42     "BridgeLibisabelle"

    43     "BridgeJEdit"

    44     "Knowledge"

    45   theories

    46     "MathEngine/MathEngine"

    47     "Test_Code/Test_Code"

    48     "BridgeLibisabelle/BridgeLibisabelle"

    49     "BridgeJEdit/BridgeJEdit"

    50     "Knowledge/Build_Thydata"

    51     "Build_Isac"

    53 (* run "./bin/isabelle build -v -b Doc" *)

    54 session Doc in Doc = Interpret +

    55   description "

    56     Formally checked documentation for Isac in analogy to ~~/Doc/.

    57   "

    58   options [document = false (*, browser_info = true*)]

    59   directories

    60     "Lucas_Interpreter"

    61   theories

    62     "Lucas_Interpreter/Lucas_Interpreter"

author	Walther Neuper <walther.neuper@jku.at>
	Tue, 06 Oct 2020 12:44:42 +0200
changeset 60080	6103433242cb
parent 60077	bd5be37901f8
child 60098	e0d05326a79e
permissions	-rw-r--r--