Reentry/Makefile at master · BruceZoom/Reentry · GitHub

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
41
42
43
44
45
46
47
48
49
CURRENT_DIR=.
COQBIN=

-include CONFIGURE

COQC=$(COQBIN)coqc
COQDEP=$(COQBIN)coqdep

DIRS = WithCall WithoutCall

INCLUDE_DEMO = $(foreach d, $(DIRS), -R $(CURRENT_DIR)/$(d) Reentry.$(d))
COQ_FLAG = $(INCLUDE_DEMO)
DEP_DEMO = -R $(CURRENT_DIR) Reentry
DEP_FLAG = $(DEP_DEMO)

Derivation_FILES = DenotationalSemantics.v FineGrainedSemantics.v DerivationTheorem.v

WithoutCall_FILES = $(Derivation_FILES)

WithCall_FILES = $(Derivation_FILES) CoarseGrainedLogic.v

FILES = \
	$(WithoutCall_FILES:%.v=WithoutCall/%.v) \
	$(WithCall_FILES:%.v=WithCall/%.v)

$(FILES:%.v=%.vo): %.vo: %.v
	@echo COQC $*.v
	@$(COQC) $(COQ_FLAG) $(CURRENT_DIR)/$*.v

WithoutCall: \
	.depend clean $(WithoutCall_FILES:%.v=WithoutCall/%.vo)

WithCall: \
	.depend clean $(WithCall_FILES:%.v=WithCall/%.vo)

# all: $(FILES:%.v=%.vo)

depend:
	$(COQDEP) $(DEP_FLAG) $(FILES) > .depend

.depend:
	@$(COQDEP) $(DEP_FLAG) $(FILES) > .depend

clean:
	@rm -f */.*.aux */*.vo */*.glob

.DEFAULT_GOAL := WithCall

include .depend