author | wneuper <Walther.Neuper@jku.at> |
Fri, 01 Dec 2023 05:51:18 +0100 | |
changeset 60770 | 365758b39d90 |
parent 60756 | b1ae5a019fa1 |
child 60771 | 1b072aab8f4e |
permissions | -rw-r--r-- |
wenzelm@60215 | 1 |
## Platform prerequisites ## |
wenzelm@60215 | 2 |
|
wenzelm@60215 | 3 |
Ensure that "curl" and "hg" (Mercurial) are installed: |
wenzelm@60215 | 4 |
|
wenzelm@60591 | 5 |
(a) Linux: e.g. "sudo apt install curl mercurial" |
wenzelm@60215 | 6 |
|
wenzelm@60215 | 7 |
(b) macOS: e.g. "brew install mercurial" or download from https://www.mercurial-scm.org |
wenzelm@60215 | 8 |
|
wenzelm@60215 | 9 |
(c) Windows: use Cygwin64 with packages "curl" and "mercurial" (via Cygwin setup-x86_64.exe) |
wenzelm@60215 | 10 |
|
wenzelm@60215 | 11 |
|
wenzelm@60215 | 12 |
## Repository management ## |
wenzelm@60215 | 13 |
|
wenzelm@60218 | 14 |
Commands below assume the same current directory: "isabisac" and "isa" are |
wenzelm@60215 | 15 |
put side-by-side. |
wenzelm@60215 | 16 |
|
wenzelm@60215 | 17 |
* initial clone: |
wenzelm@60215 | 18 |
|
wenzelm@60218 | 19 |
hg clone https://isabelle.in.tum.de/repos/isabelle isabisac |
wenzelm@60215 | 20 |
hg clone https://hg.risc.uni-linz.ac.at/wneuper/isa |
wenzelm@60215 | 21 |
|
wenzelm@60232 | 22 |
isabisac/Admin/init -I isabisac -V ./isa |
wenzelm@60232 | 23 |
isabisac/bin/isabelle components -u ./isa |
wenzelm@60215 | 24 |
|
wenzelm@60215 | 25 |
* later updates: |
wenzelm@60215 | 26 |
|
wenzelm@60621 | 27 |
hg -R ./isa pull -vu |
wenzelm@60233 | 28 |
isabisac/Admin/init -V ./isa |
wenzelm@60215 | 29 |
|
Walther@60420 | 30 |
* parallel clone: |
Walther@60420 | 31 |
hg clone https://isabelle.in.tum.de/repos/isabelle isabisac2 |
Walther@60421 | 32 |
hg clone https://hg.risc.uni-linz.ac.at/wneuper/isa isa2 |
Walther@60420 | 33 |
isabisac2/Admin/init -I isabisac2 -V ./isa2 |
Walther@60420 | 34 |
isabisac2/bin/isabelle components -u ./isa2 |
Walther@60420 | 35 |
* parallel updates: |
Walther@60420 | 36 |
hg -R ./isa2 pull -vu |
Walther@60420 | 37 |
isabisac2/Admin/init -V ./isa2 |
Walther@60420 | 38 |
* when repeating installation you may delete in |
Walther@60420 | 39 |
~/.isabelle/isabisac/etc/components |
Walther@60420 | 40 |
the line with "isa2" |
Walther@60420 | 41 |
|
wenzelm@60215 | 42 |
|
wenzelm@60215 | 43 |
## Development ## |
wenzelm@60215 | 44 |
|
wenzelm@60215 | 45 |
* Build: |
wenzelm@60215 | 46 |
|
wenzelm@60218 | 47 |
isabisac/bin/isabelle build -D '$ISABELLE_ISAC' |
wenzelm@60215 | 48 |
|
Walther@60419 | 49 |
isabisac/bin/isabelle jedit -R Specify & |
Walther@60419 | 50 |
isabisac/bin/isabelle jedit -R Interpret & |
Walther@60419 | 51 |
isabisac/bin/isabelle jedit -R Isac & |
wenzelm@60217 | 52 |
|
Walther@60419 | 53 |
isabisac/bin/isabelle jedit -l HOL isa/src/Tools/isac/Build_Isac.thy & |
Walther@60421 | 54 |
====isabisac$ ./bin/isabelle jedit -l HOL ../isa/src/Tools/isac/Build_Isac.thy & |
Walther@60436 | 55 |
isabisac$ ./bin/isabelle build -o browser_info -v -c Specify & |
Walther@60436 | 56 |
isabisac$ ./bin/isabelle build -o browser_info -v -c Interpret & |
Walther@60436 | 57 |
isabisac$ ./bin/isabelle build -o browser_info -v -c Isac & |
wenzelm@60235 | 58 |
|
wenzelm@60215 | 59 |
* Test: |
wenzelm@60215 | 60 |
|
wenzelm@60218 | 61 |
isabisac/bin/isabelle build -D '$ISABELLE_ISAC_TEST' |
wenzelm@60217 | 62 |
|
Walther@60419 | 63 |
isabisac/bin/isabelle jedit -R Isac_Test & |
wenzelm@60235 | 64 |
|
Walther@60419 | 65 |
isabisac/bin/isabelle jedit -l Isac_Test_Base isa/test/Tools/isac/Test_Isac_Short.thy & |
Walther@60421 | 66 |
====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Isac_Short.thy & |
Walther@60756 | 67 |
====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Isac.thy & |
Walther@60467 | 68 |
====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Some.thy & |
Walther@60420 | 69 |
|
Walther@60420 | 70 |
* Parallel Build |
Walther@60421 | 71 |
====isabisac2$ ./bin/isabelle jedit -l HOL ../isa2/src/Tools/isac/Build_Isac.thy & |
Walther@60420 | 72 |
* Parallel Test |
Walther@60421 | 73 |
====isabisac2$ ./bin/isabelle jedit -l Isac_Test_Base ../isa2/test/Tools/isac/Test_Isac_Short.thy & |
Walther@60493 | 74 |
====isabisac2$ ./bin/isabelle jedit -l Isac_Test_Base ../isa2/test/Tools/isac/Test_Some.thy & |
Walther@60483 | 75 |