wneuper/isa: src/Tools/isac/ROOT@6b021e8cb8da

     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 Specify" *)

    15 session Specify in Specify = "HOL-SPARK" +

    16   description "

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

    18   "

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

    20   directories

    21     "../BaseDefinitions"

    22     "../ProgLang"

    23     "../MathEngBasic"

    24   theories

    25     "../BaseDefinitions/BaseDefinitions"

    26     "../ProgLang/ProgLang"

    27     "../MathEngBasic/MathEngBasic"

    28     "Specify"

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

    31 session Interpret in Interpret = Specify +

    32   description "

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

    34   "

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

    36   theories

    37     "Interpret"

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

    40 session Isac = Interpret +

    41   description "

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

    43     for a TP-based educational mathematics assistant.

    44   "

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

    46   directories

    47     "MathEngine"

    48     "Test_Code"

    49     "BridgeLibisabelle"

    50     "BridgeJEdit"

    51     "Knowledge"

    52   theories

    53     "MathEngine/MathEngine"

    54     "Test_Code/Test_Code"

    55     "BridgeLibisabelle/BridgeLibisabelle"

    56     "BridgeJEdit/BridgeJEdit"

    57     "Knowledge/Build_Thydata"

    58     "Build_Isac"

    60 (*~~$ ./bin/isabelle build -v -b Doc          #check ok, no output

    61   *)

    62 session Doc in Doc = Interpret +

    63   description "

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

    65   "

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

    67   directories

    68     "Lucas_Interpreter"

    69     "Specify_Phase"

    70   theories

    71     "Lucas_Interpreter/Lucas_Interpreter"

    72     "Specify_Phase/Specify_Phase"

author	Walther Neuper <walther.neuper@jku.at>
	Tue, 13 Apr 2021 13:20:05 +0200
changeset 60189	6b021e8cb8da
parent 60187	751b8a13c271
child 60190	df5045d244d1
permissions	-rw-r--r--