wneuper/isa: src/Tools/isac/ROOT@8fa678b678e8

     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 Specify

    10 $ ./bin/isabelle build -o browser_info -v -b Interpret

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

    12 # this creates, among others:

    13 # file:///home/walthern/.isabelle/isabisac/browser_info/HOL/index.html

    14 # file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/index.html

    15 # file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Specify/session_graph.pdf

    16 # file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Interpret/session_graph.pdf

    17 # file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf

    18 *)

    20 (* run "./bin/isabelle build -v -b Specify" *)

    21 session Specify in Specify = HOL +

    22   description "

    23     Session covering code required for ~~/src/Tools/isac/Doc/Specify_Phase

    24   "

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

    26   directories

    27     "../BaseDefinitions"

    28     "../ProgLang"

    29     "../MathEngBasic"

    30   theories

    31     "../BaseDefinitions/BaseDefinitions"

    32     "../ProgLang/ProgLang"

    33     "../MathEngBasic/MathEngBasic"

    34     "Specify"

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

    37 session Interpret in Interpret = Specify +

    38   description "

    39     Session covering code required for ~~/src/Tools/isac/Doc/Lucas_Interpreter

    40   "

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

    42   theories

    43     "Interpret"

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

    46 session Isac = Interpret +

    47   description "

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

    49     for a TP-based educational mathematics assistant.

    50   "

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

    52   directories

    53     "MathEngine"

    54     "Test_Code"

    55     "BridgeLibisabelle"

    56     "BridgeJEdit"

    57     "Knowledge"

    58   theories

    59     "MathEngine/MathEngine"

    60     "Test_Code/Test_Code"

    61     "BridgeLibisabelle/BridgeLibisabelle"

    62     "BridgeJEdit/BridgeJEdit"

    63     "Knowledge/Build_Thydata"

    64     "Build_Isac"

author	wneuper <Walther.Neuper@jku.at>
	Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789	8fa678b678e8
parent 60506	145e45cd7a0f
permissions	-rw-r--r--