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>
Tue, 24 May 2022 12:57:47 +0200
changeset 60421 3e87dea4c1ae
parent 60420 e58e1aa72455
child 60436 1c8263e775d4
permissions -rw-r--r--
unify parse 5: for appendFormula and CAS-cmd 
     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 

    56 * Test:

    57 

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

    59 

    60     isabisac/bin/isabelle jedit -R Isac_Test &

    61 

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

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

    64 

    65 * Parallel Build

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

    67 * Parallel Test

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