diff options
| author | Brian Campbell | 2018-06-29 12:07:00 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-02 18:49:29 +0100 |
| commit | b89abf9c9e1a32892c14ab3c2e92656b1410ecac (patch) | |
| tree | f8343c4b6b3e28c78d305346d4c1842d89a32b2a /mips/Makefile | |
| parent | 61e4b53642c9ff30a82a600f23985e7555a67a0b (diff) | |
Coq building rule in MIPS makefile
Diffstat (limited to 'mips/Makefile')
| -rw-r--r-- | mips/Makefile | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/mips/Makefile b/mips/Makefile index a8bce143..d3a21957 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -47,6 +47,13 @@ mips.v: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(SAIL) -coq -dcoq_undef_axioms -o mips -coq_lib mips_extras -undefined_gen -memo_z3 $^ mips_types.v: mips.v +MIPS_COQ = mips_types.v mips_extras.v mips.v +COQ_LIBS = -R ../../bbv bbv -R ../lib/coq Sail + +%.vo: %.v + coqc $(COQ_LIBS) $< +mips.vo: mips_types.vo mips_extras.vo + M%.thy: m%.lem m%_types.lem mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy @@ -63,5 +70,5 @@ include ../etc/loc.mk clean: rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild mips.c mips_c rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml - rm -f mips.v mips_types.v + rm -f mips.v mips_types.v $(MIPS_COQ:%.v=%.vo) $(MIPS_COQ:%.v=%.glob) $(MIPS_COQ:%.v=.%.aux) -Holmake cleanAll |