blob: 1b6435e1445c8b9222504b9f2894bb7e316ac08a (
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
|
HAVE_OPAM_BBV=$(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo yes; else echo no; fi)
ifeq ($(HAVE_OPAM_BBV),no)
BBV_DIR?=../../../bbv/src/bbv
endif
CORESRC=Prompt_monad.v Prompt.v Impl_base.v Instr_kinds.v Operators_bitlists.v Operators_mwords.v Operators.v Values.v State_monad.v State.v State_lifting.v String.v Real.v Base.v
PROOFSRC=Values_lemmas.v State_monad_lemmas.v State_lemmas.v Hoare.v
SRC=$(CORESRC) $(PROOFSRC)
ifdef BBV_DIR
COQ_LIBS = -Q . Sail -Q "$(BBV_DIR)" bbv
else
COQ_LIBS = -Q . Sail
endif
TARGETS=$(SRC:.v=.vo)
.PHONY: all clean install
all: $(TARGETS)
clean:
rm -f -- $(TARGETS) $(TARGETS:.vo=.glob) $(TARGETS:%.vo=.%.aux) deps
$(TARGETS): %.vo: %.v
coqc $(COQ_LIBS) $<
deps: $(SRC)
coqdep $(COQ_LIBS) $(SRC) > deps
-include deps
COQLIB = $(shell coqc -where)
DESTDIR ?=
INSTALLDIR = $(DESTDIR)/$(COQLIB)/user-contrib/Sail
install: $(TARGETS)
test -d "$(DESTDIR)/$(COQLIB)/user-contrib" || echo Coq library directory "$(DESTDIR)/$(COQLIB)/user-contrib" not present
install -d -- "$(INSTALLDIR)"
install -m 644 -- $(SRC) $(TARGETS) $(TARGETS:.vo=.glob) "$(INSTALLDIR)"
|
