Makefile 4.04 KB
Newer Older
1
default_target: .loadpath Libs ListsOp Mid Low 
Benoit Viguier's avatar
Benoit Viguier committed
2

3
all: default_target High
4
5
6
7
8

#Note3: for SSReflect, one solution is to install MathComp 1.6
# somewhere add this line to a CONFIGURE file
# MATHCOMP=/my/path/to/mathcomp

9
10
11
12
13
14

VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)


15
DIRS= Libs ListsOp Mid Low High
16
17
18
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))

COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
19
LIBPREFIX=Tweetnacl
20
21
22
23

ifdef LIBPREFIX
 COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(LIBPREFIX).$(d))) $(EXTFLAGS)
endif
24
DEPFLAGS:=$(COQFLAGS)
25
26
27
28

COQC=$(COQBIN)coqc
COQTOP=$(COQBIN)coqtop
COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
Benoit Viguier's avatar
Benoit Viguier committed
29
COQDOC=$(COQBIN)coqdoc -d doc -g -utf8 $(DEPFLAGS)
30

ildyria's avatar
ildyria committed
31
COQVERSION= 8.7.0 or-else 8.7.1
32
33
34
35
36
COQV=$(shell $(COQC) -v)
ifeq ("$(filter $(COQVERSION),$(COQV))","")
	$(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV))
endif

Benoit Viguier's avatar
Benoit Viguier committed
37
38
39
LIBS_FILES = $(wildcard Libs/*.v)
LISTSOP_FILES = $(wildcard ListsOp/*.v)
MID_FILES = $(wildcard Mid/*.v)
Benoit Viguier's avatar
Benoit Viguier committed
40
LOW_FILES = $(wildcard Low/*.v)
Benoit Viguier's avatar
Benoit Viguier committed
41
HIGH_FILES = $(wildcard High/*.v)
42
FIELD_FILES = $(wildcard Field/*.v)
43

Benoit Viguier's avatar
Benoit Viguier committed
44
45
COUNTFILES = $(LIBS_FILES) $(LISTSOP_FILES) $(MID_FILES) $(LOW_FILES) \
$(UNPACK_FILES)
46
47


Benoit Viguier's avatar
Benoit Viguier committed
48
FILES = $(COUNTFILES) $(HIGH_FILES)
49

50
ifneq ($(filter-out archclean clean cleanall printenv count,$(MAKECMDGOALS)),)
51
52
53
54
55
56
-include $(addsuffix .d,$(FILES))
else
ifeq ($(MAKECMDGOALS),)
-include $(addsuffix .d,$(FILES))
endif
endif
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72

%_stripped.v: %.v
# e.g., 'make progs/verif_reverse_stripped.v will remove the tutorial comments
# from progs/verif_reverse.v
	grep -v '^.[*][*][ )]' $*.v >$@

%.vo: %.v
	@echo COQC $*.v
ifeq ($(TIMINGS), true)
#	bash -c "wc $*.v >>timings; date +'%s.%N before' >> timings; $(COQC) $(COQFLAGS) $*.v; date +'%s.%N after' >>timings" 2>>timings
	@bash -c "/bin/time --output=TIMINGS -a -f '%e real, %U user, %S sys, '\"$(shell wc $*.v)\" $(COQC) $(COQFLAGS) $*.v"
#	echo -n $*.v " " >>TIMINGS; bash -c "/usr/bin/time -o TIMINGS -a $(COQC) $(COQFLAGS) $*.v"
else
	@$(COQC) $(COQFLAGS) $*.v
endif

Benoit Viguier's avatar
Benoit Viguier committed
73
74
75
76
77
78
79
80
81
82
%.vio: %.v
	@echo COQC $*.v
ifeq ($(TIMINGS), true)
#	bash -c "wc $*.v >>timings; date +'%s.%N before' >> timings; $(COQC) $(COQFLAGS) $*.v; date +'%s.%N after' >>timings" 2>>timings
	@bash -c "/bin/time --output=TIMINGS -a -f '%e real, %U user, %S sys, '\"$(shell wc $*.v)\" $(COQC) $(COQFLAGS) $*.v"
#	echo -n $*.v " " >>TIMINGS; bash -c "/usr/bin/time -o TIMINGS -a $(COQC) $(COQFLAGS) $*.v"
else
	@$(COQC) -quick $(COQFLAGS) $*.v
endif

83
all: .loadpath $(FILES:.v=.vo)
Benoit Viguier's avatar
Benoit Viguier committed
84
quick: .loadpath $(FILES:.v=.vio)
85

Benoit Viguier's avatar
Benoit Viguier committed
86
87
88
Libs: 		.loadpath $(LIBS_FILES:%.v=%.vo)
ListsOp:	.loadpath $(LISTSOP_FILES:%.v=%.vo)
Mid:		.loadpath $(MID_FILES:%.v=%.vo)
Benoit Viguier's avatar
Benoit Viguier committed
89
Low:		.loadpath $(LOW_FILES:%.v=%.vo)
Benoit Viguier's avatar
Benoit Viguier committed
90
High:		.loadpath $(HIGH_FILES:%.v=%.vo)
91
Field:		.loadpath $(FIELD_FILES:%.v=%.vo)
92
93
94
95
96

_CoqProject: Makefile
	$(SHOW)Generate _CoqProject
	$(HIDE)echo $(COQFLAGS) >_CoqProject

Benoit Viguier's avatar
Benoit Viguier committed
97
.loadpath: _CoqProject
98
99
	$(SHOW)Generate .loadpath
	$(HIDE)echo $(COQFLAGS) > .loadpath
100
101


Benoit Viguier's avatar
Benoit Viguier committed
102
103
doc:
	mkdir -p doc
Benoit Viguier's avatar
Benoit Viguier committed
104
	$(COQDOC) $(FILES)
Benoit Viguier's avatar
Benoit Viguier committed
105

106
107
108
$(addsuffix .d,$(FILES)): %.v.d: %.v
	$(SHOW)'COQDEP $<'
	$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
109
110

clean:
111
	$(SHOW)cleaning files...
Benoit Viguier's avatar
Benoit Viguier committed
112
	$(HIDE)rm -f $(wildcard */*.d) $(wildcard */*.vo) $(wildcard */*.glob) $(wildcard */.*.aux) .loadpath _CoqProject .depend .nia.cache .lia.cache
113

Benoit Viguier's avatar
Benoit Viguier committed
114
115
116
117
118
119
120
121
122
# check: quick
# 	coqtop -schedule-vio2vo

vio2vo: quick
	$(COQC) $(COQFLAGS) -schedule-vio2vo $(J) $(FILES:%.v=%.vio)

checkproofs:
	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(FILES:%.v=%.vio)

123
count:
124
	wc -l $(COUNTFILES)
125

Benoit Viguier's avatar
Benoit Viguier committed
126
127
128
129
130
131
132
133
134
printenv:
	@"$(COQTOP)" -config
	@echo 'CAMLC =	$(CAMLC)'
	@echo 'CAMLOPTC =	$(CAMLOPTC)'
	@echo 'PP =	$(PP)'
	@echo 'COQFLAGS =	$(COQFLAGS)'
	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'

135
136
137
138
139
# The .depend file is divided into two parts, .depend and .depend-concur,
# in order to work around a limitation in Cygwin about how long one
# command line can be.  (Or at least, it seems to be a solution to some
# such problem, not sure exactly.  -- Andrew)
-include .depend
Benoit Viguier's avatar
update    
Benoit Viguier committed
140
-include .depend-concur