| author | wenzelm |
| Thu, 10 Jun 2021 11:54:20 +0200 | |
| changeset 60289 | a7b88fc19a92 |
| parent 60235 | 0d11e9bab8de |
| 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 |