aboutsummaryrefslogtreecommitdiff
path: root/.make/coq.mk
blob: b077a5b08d7041f8182ede5087910bd0c3390bb9 (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
# © 2012–2015 the Massachusetts Institute of Technology
# @author bbaren + rsloan

COQC = coqc
COQDEP = coqdep

COMPILE.v = $(COQC) -q $(COQLIBS)

.PHONY: check_fiat check_bedrock

check_fiat:
	@perl -e \
		'if(! -d "./fiat") { print("you need to link fiat to ./fiat\n"); exit(1) }'

check_bedrock:
	@perl -e \
		'if(! -d "./bedrock") { print("you need to link bedrock to ./bedrock\n"); exit(1) }'

%.vo %.glob: %.v.d
	$(COMPILE.v) $*

%.v.d: check_fiat check_bedrock %.v
	@$(COQDEP) -I . $(COQLIBS) "$<" >"$@" \
	  || (RV=$$?; rm -f "$@"; exit $${RV})

define coq-generated
$1.vo $1.v.d $1.glob
endef