summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThomas Bauereiss2018-04-20 15:47:21 +0100
committerThomas Bauereiss2018-04-20 15:50:19 +0100
commit85d6051f04a5ffa93f35f3a6f4471aebfecd5c29 (patch)
tree8311fc7c985697ac3c1f7970d1765360cf932276
parent895f868cd537277ba61dfc427fee0e288af7e226 (diff)
Make building of Isabelle heap image optional
-rw-r--r--lib/isabelle/Makefile8
-rw-r--r--lib/isabelle/manual/Manual.thy2
2 files changed, 6 insertions, 4 deletions
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 572610e1..f8786321 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -8,16 +8,18 @@ RISCV_DIR = ../../riscv
.PHONY: all heap-img clean
-all: heap-img
+all: thys
-heap-img: $(THYS) $(EXTRA_THYS) ROOT
+thys: $(THYS)
+
+heap-img: thys $(EXTRA_THYS) ROOT
@echo '*** To build a heap image with the Sail library, please'
@echo '*** add this directory to your ROOTS file'
@echo '*** (e.g. $$HOME/.isabelle/Isabelle<version>/ROOTS)'
@echo '*** and add the isabelle binary to your PATH.'
isabelle build -b Sail
-manual: heap-img manual/Manual.thy
+manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex
cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf
make -C $(RISCV_DIR) Riscv_duopod.thy
isabelle build -d manual Sail-Manual
diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy
index 5286b754..db960cf9 100644
--- a/lib/isabelle/manual/Manual.thy
+++ b/lib/isabelle/manual/Manual.thy
@@ -18,7 +18,7 @@ As an additional setup step for Isabelle generation, it is useful to build an Is
of the Sail library.
This will allow you to start Isabelle with the Sail library pre-loaded using the
@{verbatim "-l Sail"} option.
-For this purpose, run @{verbatim make} in the @{path "lib/isabelle"} subdirectory of Sail and
+For this purpose, run @{verbatim "make heap-img"} in the @{path "lib/isabelle"} subdirectory of Sail and
follow the instructions.
In order to generate theorem prover definitions, Sail specifications