From 07cf22289b1b4bb2300d4670573a7faee7211a04 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 18:53:20 +0000 Subject: Fix build of Isabelle documentation --- lib/isabelle/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/isabelle/Makefile') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 57459b82..f9c061b3 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -7,7 +7,7 @@ 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 +RISCV ?= ../../../sail-riscv .PHONY: all heap-img clean @@ -24,8 +24,8 @@ heap-img: thys $(EXTRA_THYS) ROOT 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 $(RISCV) riscv_duopod + isabelle build -d manual -d $(RISCV)/generated_definitions/isabelle Sail-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 $< -- cgit v1.2.3 From aeb0f82f67ff829cd7a4b57c638b44a07d39ba3b Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 19:53:59 +0000 Subject: Don't require manual set up of Isabelle session directories Since Isabelle 2018, specifying the same directory both on the command line and persistently in the user's ROOTS file is allowed, so we don't have to choose between one or the other any more. --- lib/isabelle/Makefile | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'lib/isabelle/Makefile') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index f9c061b3..3ce9b9d8 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -16,16 +16,12 @@ 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/ROOTS)' - @echo '*** and add the isabelle binary to your PATH.' - isabelle build -b Sail + isabelle build -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) riscv_duopod - isabelle build -d manual -d $(RISCV)/generated_definitions/isabelle Sail-Manual + isabelle build -d . -d $(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 $< -- cgit v1.2.3 From 365cf2015c77551e37d31336220497f6ca84794c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 23:16:47 +0000 Subject: Pass Lem library path to Isabelle --- lib/isabelle/Makefile | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'lib/isabelle/Makefile') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 3ce9b9d8..a1500292 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -7,6 +7,11 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ Sail2_prompt_monad_lemmas.thy \ Sail2_operators_mwords_lemmas.thy Hoare.thy +LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib +ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) +$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) +endif + RISCV ?= ../../../sail-riscv .PHONY: all heap-img clean @@ -16,12 +21,12 @@ all: thys thys: $(THYS) heap-img: thys $(EXTRA_THYS) ROOT - isabelle build -D . + 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) riscv_duopod - isabelle build -d . -d $(RISCV)/generated_definitions/isabelle -D manual + isabelle build -d $(LEM_ISA_LIB) -d . -d $(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 $< -- cgit v1.2.3 From 8a3c75dfd07d7264a82450aaebce86b5e82c974b Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Mon, 21 Jan 2019 18:42:12 -0800 Subject: The RISCV environment variable collides with common usage by the RISC-V toolchain; use SAIL_RISCV instead to refer to sail-riscv. --- lib/isabelle/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/isabelle/Makefile') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index a1500292..975810a1 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -12,7 +12,7 @@ ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) endif -RISCV ?= ../../../sail-riscv +SAIL_RISCV ?= ../../../sail-riscv .PHONY: all heap-img clean @@ -25,8 +25,8 @@ heap-img: thys $(EXTRA_THYS) ROOT 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) riscv_duopod - isabelle build -d $(LEM_ISA_LIB) -d . -d $(RISCV)/generated_definitions/isabelle -D 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 $< -- cgit v1.2.3 From 1951607813f73688297840fc4ae4b3059b7528c5 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 23 Jan 2019 16:29:49 +0000 Subject: Don't let "make" fail unnecessarily in lib/isabelle Only check for availability of Lem library if actually trying to build an Isabelle heap image. --- lib/isabelle/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/isabelle/Makefile') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 975810a1..039a81f1 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -8,9 +8,6 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ Sail2_operators_mwords_lemmas.thy Hoare.thy LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib -ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) -$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) -endif SAIL_RISCV ?= ../../../sail-riscv @@ -21,6 +18,9 @@ all: thys thys: $(THYS) heap-img: thys $(EXTRA_THYS) ROOT +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 -- cgit v1.2.3