Skip to content

Commit 6670631

Browse files
authored
add instructions for using Isabelle heap images.
1 parent b21681f commit 6670631

File tree

1 file changed

+15
-0
lines changed

1 file changed

+15
-0
lines changed

README.md

+15
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,21 @@ git clone https://github.com/uqcyber/veriopt-releases
2727
isabelle jedit -d veriopt-releases ROOT
2828
```
2929

30+
These theories are fairly large and require 32GB of RAM to load interactively.
31+
If you do not have that luxury, you can pre-compile the most memory-intensive theories
32+
(e.g. IRStepThms.thy).
33+
These are included in the Semantics session so we will compile that.
34+
35+
```bash
36+
cd veriopt-releases # or veriopt-dev/isabelle
37+
isabelle build -d . -v Semantics
38+
isabelle jedit -d . -l Semantics ROOT
39+
```
40+
In the Theories sidebar, you'll see Semantics instead of HOL, meaning we
41+
are using the veriopt/Semantics session.
42+
As a side-effect of this precompilation, you'll be prevented from editing
43+
theories within Semantics ("Cannot update finished theory").
44+
3045
## Building Theories
3146
Building the theories will check all the theories in the repository are correct and generate HTML and PDF outputs. You can build the theories with the following command. Isabelle2022 will need to be installed and the tool wrapper should be accessible via the `isabelle` command on your machine.
3247

0 commit comments

Comments
 (0)