diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2020-06-18 20:00:13 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2020-06-18 20:00:13 +0100 |
| commit | 0b8bf69d1509ae19a580ef893c1d93e9f068673b (patch) | |
| tree | 706833bf4b592b186131753c6b772bbe97a192cd | |
| parent | 2ae02a095ac9fc7947e7e2019ecb78af257d81d6 (diff) | |
| download | sail-riscv-0b8bf69d1509ae19a580ef893c1d93e9f068673b.zip sail-riscv-0b8bf69d1509ae19a580ef893c1d93e9f068673b.tar.gz sail-riscv-0b8bf69d1509ae19a580ef893c1d93e9f068673b.tar.bz2 | |
Make duopod build in coq again, and fix location
| -rw-r--r-- | Makefile | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -336,7 +336,7 @@ ifndef EXPLICIT_COQ_SAIL EXPLICIT_COQ_SAIL = $(shell if opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi) endif -COQ_LIBS = -R generated_definitions/coq/$(ARCH) '' -R handwritten_support '' +COQ_LIBS = -R generated_definitions/coq/$(ARCH) '' -R generated_definitions/coq '' -R handwritten_support '' ifeq ($(EXPLICIT_COQ_BBV),yes) COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv endif @@ -351,9 +351,9 @@ 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 -coq_lib mem_metadata $(SAIL_COQ_SRCS) -$(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 -coq_lib mem_metadata $^ +$(addprefix generated_definitions/coq/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail model/riscv_termination_duo.sail + mkdir -p generated_definitions/coq/ + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq -o riscv_duopod -coq_lib riscv_extras -coq_lib mem_metadata model/riscv_duopod.sail model/riscv_termination_duo.sail %.vo: %.v ifeq ($(EXPLICIT_COQ_BBV),yes) @@ -369,7 +369,7 @@ endif coqc $(COQ_LIBS) $< generated_definitions/coq/$(ARCH)/riscv.vo: generated_definitions/coq/$(ARCH)/riscv_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo -generated_definitions/coq/$(ARCH)/riscv_duopod.vo: generated_definitions/coq/$(ARCH)/riscv_duopod_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo +generated_definitions/coq/riscv_duopod.vo: generated_definitions/coq/riscv_duopod_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo echo_rmem_srcs: echo $(SAIL_RMEM_SRCS) |