aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorBrian Campbell <Brian.Campbell@ed.ac.uk>2019-08-13 15:41:48 +0100
committerBrian Campbell <Brian.Campbell@ed.ac.uk>2019-08-13 15:41:48 +0100
commit503cb6eca4831609e46abf22a54d4ba4b663d2b5 (patch)
treecbdf09e763c4627295ae54aadfa92413518cf075 /Makefile
parenteafbb796e16ac61ef39d36b32524b40ada195375 (diff)
downloadsail-riscv-503cb6eca4831609e46abf22a54d4ba4b663d2b5.zip
sail-riscv-503cb6eca4831609e46abf22a54d4ba4b663d2b5.tar.gz
sail-riscv-503cb6eca4831609e46abf22a54d4ba4b663d2b5.tar.bz2
Fix Coq duopod build by giving missing termination measure
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index e69208c..82c6315 100644
--- a/Makefile
+++ b/Makefile
@@ -289,7 +289,7 @@ riscv_coq_build: generated_definitions/coq/$(ARCH)/riscv.vo
$(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile
mkdir -p generated_definitions/coq/$(ARCH)
$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS)
-$(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail
+$(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail model/riscv_termination_duo.sail
mkdir -p generated_definitions/coq/$(ARCH)
$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv_duopod -coq_lib riscv_extras $^