author | wenzelm |
Mon, 19 Apr 2021 18:05:01 +0200 | |
changeset 60235 | 0d11e9bab8de |
parent 60233 | 49db3ac4e14d |
child 60419 | 1268b43faf69 |
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@60215 | 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@60233 | 27 |
hg -R ./isa pull -vu |
wenzelm@60233 | 28 |
isabisac/Admin/init -V ./isa |
wenzelm@60215 | 29 |
|
wenzelm@60215 | 30 |
|
wenzelm@60215 | 31 |
## Development ## |
wenzelm@60215 | 32 |
|
wenzelm@60215 | 33 |
* Build: |
wenzelm@60215 | 34 |
|
wenzelm@60218 | 35 |
isabisac/bin/isabelle build -D '$ISABELLE_ISAC' |
wenzelm@60215 | 36 |
|
wenzelm@60218 | 37 |
isabisac/bin/isabelle jedit -R Specify |
wenzelm@60218 | 38 |
isabisac/bin/isabelle jedit -R Interpret |
wenzelm@60218 | 39 |
isabisac/bin/isabelle jedit -R Isac |
wenzelm@60217 | 40 |
|
wenzelm@60235 | 41 |
isabisac/bin/isabelle jedit -l HOL isa/src/Tools/isac/Build_Isac.thy |
wenzelm@60235 | 42 |
|
wenzelm@60215 | 43 |
* Test: |
wenzelm@60215 | 44 |
|
wenzelm@60218 | 45 |
isabisac/bin/isabelle build -D '$ISABELLE_ISAC_TEST' |
wenzelm@60217 | 46 |
|
wenzelm@60218 | 47 |
isabisac/bin/isabelle jedit -R Isac_Test |
wenzelm@60235 | 48 |
|
wenzelm@60235 | 49 |
isabisac/bin/isabelle jedit -l Isac_Test_Base isa/test/Tools/isac/Test_Isac_Short.thy |