summaryrefslogtreecommitdiff
path: root/lib/isabelle
diff options
context:
space:
mode:
Diffstat (limited to 'lib/isabelle')
-rw-r--r--lib/isabelle/Makefile17
1 files changed, 9 insertions, 8 deletions
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 57459b82..039a81f1 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -7,7 +7,9 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \
Sail2_prompt_monad_lemmas.thy \
Sail2_operators_mwords_lemmas.thy Hoare.thy
-RISCV_DIR = ../../riscv
+LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib
+
+SAIL_RISCV ?= ../../../sail-riscv
.PHONY: all heap-img clean
@@ -16,16 +18,15 @@ all: thys
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
+ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),)
+ $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable)
+endif
+ isabelle build -d $(LEM_ISA_LIB) -D .
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 -d $(RISCV_DIR) Sail-Manual
+ make -C $(SAIL_RISCV) riscv_duopod
+ isabelle build -d $(LEM_ISA_LIB) -d . -d $(SAIL_RISCV)/generated_definitions/isabelle -D manual
Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<