Makefile 5.47 KB
Newer Older
1
default_target: .loadpath Libs ListsOp Op Car Sel Montgomery Unpack
2
3
4
5
6

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

7
8
9
10
11
12

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


13
DIRS= Libs ListsOp Op Car Sel Montgomery Unpack
14
15
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))

16

17
COQSTDPP = ../coq-stdpp/theories
18
COQPRIME = Coqprime
19

Benoit Viguier's avatar
Benoit Viguier committed
20
# for Coq-stdpp
Benoit Viguier's avatar
Benoit Viguier committed
21
ifdef COQSTDPP
22
 EXTFLAGS:=$(EXTFLAGS) -R $(COQSTDPP) stdpp
23
24
endif

25
26
27
28
29
30
31
32
33
34
35
36
37

# for Coq-stdpp
ifdef COQPRIME
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/Tactic Coqprime
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/N Coqprime
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/Z Coqprime
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/List Coqprime
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/PrimalityTest Coqprime
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/elliptic Coqprime
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/num Coqprime
 EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/examples Coqprime
endif

38
39
40
41
42
43
# for SSReflect
ifdef MATHCOMP
 EXTFLAGS:=$(EXTFLAGS) -R $(MATHCOMP) mathcomp
endif

COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
44
LIBPREFIX=Tweetnacl
45
46
47
48

ifdef LIBPREFIX
 COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(LIBPREFIX).$(d))) $(EXTFLAGS)
endif
49
DEPFLAGS:=$(COQFLAGS)
50
51
52
53

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

Benoit Viguier's avatar
update    
Benoit Viguier committed
56
COQVERSION= 8.6
57
58
59
60
61
62
COQV=$(shell $(COQC) -v)
ifeq ("$(filter $(COQVERSION),$(COQV))","")
	$(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV))
endif

define clean_files
63
	$($(1):%.v=$(2)/%.v.d) \
Benoit Viguier's avatar
Benoit Viguier committed
64
	$($(1):%.v=$(2)/%.vio) \
65
	$($(1):%.v=$(2)/%.vo) \
66
	$($(1):%.v=$(2)/.%.aux) \
67
68
69
70
71
72
73
74
75
76
77
	$($(1):%.v=$(2)/.%.vo.aux) \
	$($(1):%.v=$(2)/%.glob) \
	$($(1):%.v=$(2)/%.v.crashcoqide)
endef



LIBS_FILES = $(notdir $(wildcard Libs/*.v))
LISTSOP_FILES = $(notdir $(wildcard ListsOp/*.v))
OP_FILES = $(notdir $(wildcard Op/*.v))
CAR_FILES = $(notdir $(wildcard Car/*.v))
Benoit Viguier's avatar
Benoit Viguier committed
78
SEL_FILES = $(notdir $(wildcard Sel/*.v))
79
UNPACK_FILES = $(notdir $(wildcard Unpack/*.v))
80
MONTGOMERY_FILES = $(notdir $(wildcard Montgomery/*.v))
81

82
COUNTFILES = \
83
84
85
 $(LIBS_FILES:%=Libs/%) \
 $(LISTSOP_FILES:%=ListsOp/%) \
 $(OP_FILES:%=Op/%) \
86
 $(CAR_FILES:%=Car/%) \
Benoit Viguier's avatar
Benoit Viguier committed
87
 $(SEL_FILES:%=Sel/%) \
88
89
90
91
92
93
 $(UNPACK_FILES:%=Unpack/%) \


FILES = \
 $(COUNTFILES) \
 $(MONTGOMERY_FILES:%=Montgomery/%) \
94

95
ifneq ($(filter-out archclean clean cleanall printenv count,$(MAKECMDGOALS)),)
96
97
98
99
100
101
-include $(addsuffix .d,$(FILES))
else
ifeq ($(MAKECMDGOALS),)
-include $(addsuffix .d,$(FILES))
endif
endif
102

103
104
CLEANFILES = \
	$(call clean_files,LIBS_FILES,Libs) \
105
106
	$(call clean_files,LISTSOP_FILES,ListsOp) \
	$(call clean_files,OP_FILES,Op) \
107
	$(call clean_files,CAR_FILES,Car) \
Benoit Viguier's avatar
Benoit Viguier committed
108
	$(call clean_files,SEL_FILES,Sel) \
109
	$(call clean_files,UNPACK_FILES,Unpack) \
110
	$(call clean_files,MONTGOMERY_FILES,Montgomery)
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

%_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
127
128
129
130
131
132
133
134
135
136
%.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

137
all: .loadpath $(FILES:.v=.vo)
Benoit Viguier's avatar
Benoit Viguier committed
138
quick: .loadpath $(FILES:.v=.vio)
139
140
141

Libs: 		.loadpath $(LIBS_FILES:%.v=Libs/%.vo)
ListsOp:	.loadpath $(LISTSOP_FILES:%.v=ListsOp/%.vo)
142
Op:			.loadpath $(OP_FILES:%.v=Op/%.vo)
143
Car:		.loadpath $(CAR_FILES:%.v=Car/%.vo)
Benoit Viguier's avatar
Benoit Viguier committed
144
Sel:		.loadpath $(SEL_FILES:%.v=Sel/%.vo)
145
Unpack:		.loadpath $(UNPACK_FILES:%.v=Unpack/%.vo)
146
147
148
149
150
151
Montgomery:	.loadpath $(MONTGOMERY_FILES:%.v=Montgomery/%.vo)

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

Benoit Viguier's avatar
Benoit Viguier committed
152
.loadpath: _CoqProject
153
154
	$(SHOW)Generate .loadpath
	$(HIDE)echo $(COQFLAGS) > .loadpath
155
156


Benoit Viguier's avatar
Benoit Viguier committed
157
158
doc:
	mkdir -p doc
Benoit Viguier's avatar
Benoit Viguier committed
159
	$(COQDOC) $(FILES)
Benoit Viguier's avatar
Benoit Viguier committed
160

161
162
163
$(addsuffix .d,$(FILES)): %.v.d: %.v
	$(SHOW)'COQDEP $<'
	$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
164
165

clean:
166
167
	$(SHOW)cleaning files...
	$(HIDE)rm -f $(CLEANFILES) .loadpath _CoqProject .depend .nia.cache .lia.cache
168

Benoit Viguier's avatar
Benoit Viguier committed
169
170
171
172
173
174
175
176
177
# 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)

178
count:
179
	wc -l $(COUNTFILES)
180

Benoit Viguier's avatar
Benoit Viguier committed
181
182
183
184
185
186
187
188
189
printenv:
	@"$(COQTOP)" -config
	@echo 'CAMLC =	$(CAMLC)'
	@echo 'CAMLOPTC =	$(CAMLOPTC)'
	@echo 'PP =	$(PP)'
	@echo 'COQFLAGS =	$(COQFLAGS)'
	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'

190
191
192
193
194
# 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
195
-include .depend-concur