Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
README.md
author wneuper <Walther.Neuper@jku.at>
Mon, 18 Sep 2023 10:26:35 +0200
changeset 60748 d9bae125ba2a
parent 60621 dbb293ed4587
child 60756 b1ae5a019fa1
permissions -rw-r--r--
prepare 4: shift new code (previous CS was: intermediate I_Model.complete_method) 
     1 ## Platform prerequisites ##

     2 

     3 Ensure that "curl" and "hg" (Mercurial) are installed:

     4 

     5   (a) Linux: e.g. "sudo apt install curl mercurial"

     6 

     7   (b) macOS: e.g. "brew install mercurial" or download from https://www.mercurial-scm.org

     8 

     9   (c) Windows: use Cygwin64 with packages "curl" and "mercurial" (via Cygwin setup-x86_64.exe)

    10 

    11 

    12 ## Repository management ##

    13 

    14 Commands below assume the same current directory: "isabisac" and "isa" are

    15 put side-by-side.

    16 

    17 * initial clone:

    18 

    19     hg clone https://isabelle.in.tum.de/repos/isabelle isabisac

    20     hg clone https://hg.risc.uni-linz.ac.at/wneuper/isa

    21 

    22     isabisac/Admin/init -I isabisac -V ./isa

    23     isabisac/bin/isabelle components -u ./isa

    24 

    25 * later updates:

    26 

    27     hg -R ./isa pull -vu

    28     isabisac/Admin/init -V ./isa

    29 

    30 * parallel clone:

    31     hg clone https://isabelle.in.tum.de/repos/isabelle isabisac2

    32     hg clone https://hg.risc.uni-linz.ac.at/wneuper/isa isa2

    33     isabisac2/Admin/init -I isabisac2 -V ./isa2

    34     isabisac2/bin/isabelle components -u ./isa2

    35 * parallel updates:

    36     hg -R ./isa2 pull -vu

    37     isabisac2/Admin/init -V ./isa2

    38 * when repeating installation you may delete in

    39     ~/.isabelle/isabisac/etc/components

    40     the line with "isa2"

    41 

    42 

    43 ## Development ##

    44 

    45 * Build:

    46 

    47     isabisac/bin/isabelle build -D '$ISABELLE_ISAC'

    48 

    49     isabisac/bin/isabelle jedit -R Specify &

    50     isabisac/bin/isabelle jedit -R Interpret &

    51     isabisac/bin/isabelle jedit -R Isac &

    52 

    53     isabisac/bin/isabelle jedit -l HOL isa/src/Tools/isac/Build_Isac.thy &

    54 ====isabisac$ ./bin/isabelle jedit -l HOL ../isa/src/Tools/isac/Build_Isac.thy &

    55     isabisac$ ./bin/isabelle build -o browser_info -v -c Specify &

    56     isabisac$ ./bin/isabelle build -o browser_info -v -c Interpret &

    57     isabisac$ ./bin/isabelle build -o browser_info -v -c Isac &

    58 

    59 * Test:

    60 

    61     isabisac/bin/isabelle build -D '$ISABELLE_ISAC_TEST'

    62 

    63     isabisac/bin/isabelle jedit -R Isac_Test &

    64 

    65     isabisac/bin/isabelle jedit -l Isac_Test_Base isa/test/Tools/isac/Test_Isac_Short.thy &

    66 ====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Isac_Short.thy &

    67 ====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Some.thy &

    68 

    69 * Parallel Build

    70 ====isabisac2$ ./bin/isabelle jedit -l HOL ../isa2/src/Tools/isac/Build_Isac.thy &

    71 * Parallel Test

    72 ====isabisac2$ ./bin/isabelle jedit -l Isac_Test_Base ../isa2/test/Tools/isac/Test_Isac_Short.thy &

    73 ====isabisac2$ ./bin/isabelle jedit -l Isac_Test_Base ../isa2/test/Tools/isac/Test_Some.thy &

    74
wneuper/isa