blob: 42071a8c7f25b72a888f3fa432cb74a9dbcea148 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
THYS = Sail2_instr_kinds.thy Sail2_values.thy Sail2_operators.thy \
Sail2_operators_mwords.thy Sail2_operators_bitlists.thy \
Sail2_state_monad.thy Sail2_state.thy Sail2_state_lifting.thy \
Sail2_prompt_monad.thy Sail2_prompt.thy \
Sail2_string.thy
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
SAIL_RISCV ?= ../../../sail-riscv
.PHONY: all heap-img clean
all: thys
thys: $(THYS)
heap-img: thys $(EXTRA_THYS) ROOT
if [ -z "$(wildcard $(LEM_ISA_LIB)/ROOT)" ]; \
then echo isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable; false; \
else isabelle build -b -d $(LEM_ISA_LIB) -D . ; \
fi
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 $(SAIL_RISCV) riscv_duopod
isabelle build -d $(LEM_ISA_LIB) -d . -d $(SAIL_RISCV)/generated_definitions/isabelle -D manual
Sail2_instr_kinds.thy: ../../src/gen_lib/sail2_instr_kinds.lem
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_values.thy: ../../src/gen_lib/sail2_values.lem Sail2_instr_kinds.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_operators.thy: ../../src/gen_lib/sail2_operators.lem Sail2_values.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_operators_mwords.thy: ../../src/gen_lib/sail2_operators_mwords.lem Sail2_operators.thy Sail2_prompt.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_operators_bitlists.thy: ../../src/gen_lib/sail2_operators_bitlists.lem Sail2_operators.thy Sail2_prompt.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_prompt_monad.thy: ../../src/gen_lib/sail2_prompt_monad.lem Sail2_values.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_prompt.thy: ../../src/gen_lib/sail2_prompt.lem Sail2_prompt_monad.thy Sail2_prompt_monad_lemmas.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_state_monad.thy: ../../src/gen_lib/sail2_state_monad.lem Sail2_values.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_state.thy: ../../src/gen_lib/sail2_state.lem Sail2_prompt.thy Sail2_state_monad.thy Sail2_state_monad_lemmas.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_state_lifting.thy: ../../src/gen_lib/sail2_state_lifting.lem Sail2_prompt.thy Sail2_state.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
Sail2_string.thy: ../../src/gen_lib/sail2_string.lem Sail2_operators_mwords.thy
lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
clean:
-rm $(THYS)
|
