diff options
Diffstat (limited to 'lib/isabelle/Makefile')
| -rw-r--r-- | lib/isabelle/Makefile | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 566af455..572610e1 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -4,44 +4,50 @@ THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \ Sail_operators_mwords_lemmas.thy Hoare.thy +RISCV_DIR = ../../riscv + .PHONY: all heap-img clean all: heap-img heap-img: $(THYS) $(EXTRA_THYS) ROOT @echo '*** To build a heap image with the Sail library, please' - @echo '*** add the ROOT file in this directory to your ROOTS file' + @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 + 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 + Sail_instr_kinds.thy: ../../src/lem_interp/sail_instr_kinds.lem - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy Prompt.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy Prompt.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_lemmas.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy - lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< clean: -rm $(THYS) - -rm *Auxiliary.thy |