SRCS = riscv_reg_type.sail riscv_regs.sail

SAIL_DIR:=$(shell opam config var sail:share)
SAIL:=sail
SAIL_LIB_DIR:=$(SAIL_DIR)/lib
export SAIL_LIB_DIR
SAIL_SRC_DIR:=$(SAIL_DIR)/src

EXPLICIT_COQ_BBV = $(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)

COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv
COQ_LIBS += -Q $(SAIL_LIB_DIR)/coq Sail
COQ_LIBS = -R generated_definitions/coq/$(ARCH) '' -R generated_definitions/coq '' -R handwritten_support ''

riscv_coq: $(addprefix build/,riscv.v riscv_types.v)
riscv_coq_build: build/riscv.vo
.PHONY: riscv_coq riscv_coq_build

# %.vo: %.v
# 	coqc $(COQ_LIBS) $<

$(addprefix build/,riscv.v riscv_types.v): $(SRCS) Makefile
	mkdir -p build
	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir build/ -o riscv $(SRCS)
# $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir build/ -o riscv -coq_lib riscv_extras -coq_lib mem_metadata $(SRCS)


# build/riscv.vo: build/riscv_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo

default:riscv_coq