## Platform prerequisites ##

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

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

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

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

## Repository management ##

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

put side-by-side.

* initial clone:

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

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

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

    isabisac/bin/isabelle components -u ./isa

* later updates:

    hg -R ./isa pull -vu

    isabisac/Admin/init -V ./isa

* parallel clone:

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

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

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

    isabisac2/bin/isabelle components -u ./isa2

* parallel updates:

    hg -R ./isa2 pull -vu

    isabisac2/Admin/init -V ./isa2

* when repeating installation you may delete in

    ~/.isabelle/isabisac/etc/components

    the line with "isa2"

## Development ##

* Build:

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

    isabisac/bin/isabelle jedit -R Specify &

    isabisac/bin/isabelle jedit -R Interpret &

    isabisac/bin/isabelle jedit -R Isac &

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

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

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

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

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

* Test:

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

    isabisac/bin/isabelle jedit -R Isac_Test &

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

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

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

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

* Parallel Build

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

* Parallel Test

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

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