Makefile 4.14 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
default_target: .loadpath Libs ListsOp Mid Low Car Sel Unpack

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),,@)


Benoit Viguier's avatar
Benoit Viguier committed
15
DIRS= Libs ListsOp Mid Car Sel High Unpack
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

Benoit Viguier's avatar
Benoit Viguier committed
31
COQVERSION= 8.7.0
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
40
41
42
43
LIBS_FILES = $(wildcard Libs/*.v)
LISTSOP_FILES = $(wildcard ListsOp/*.v)
MID_FILES = $(wildcard Mid/*.v)
CAR_FILES = $(wildcard Car/*.v)
SEL_FILES = $(wildcard Sel/*.v)
UNPACK_FILES = $(wildcard Unpack/*.v)
HIGH_FILES = $(wildcard High/*.v)
44

Benoit Viguier's avatar
Benoit Viguier committed
45
46
COUNTFILES = $(LIBS_FILES) $(LISTSOP_FILES) $(MID_FILES) $(CAR_FILES) \
 $(SEL_FILES) $(UNPACK_FILES)
47
48


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

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

%_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
74
75
76
77
78
79
80
81
82
83
%.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

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

Benoit Viguier's avatar
Benoit Viguier committed
87
88
89
90
91
92
93
Libs: 		.loadpath $(LIBS_FILES:%.v=%.vo)
ListsOp:	.loadpath $(LISTSOP_FILES:%.v=%.vo)
Mid:		.loadpath $(MID_FILES:%.v=%.vo)
Car:		.loadpath $(CAR_FILES:%.v=%.vo)
Sel:		.loadpath $(SEL_FILES:%.v=%.vo)
Unpack:		.loadpath $(UNPACK_FILES:%.v=%.vo)
High:		.loadpath $(HIGH_FILES:%.v=%.vo)
94
95
96
97
98

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

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


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

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

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

Benoit Viguier's avatar
Benoit Viguier committed
116
117
118
119
120
121
122
123
124
# 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)

125
count:
126
	wc -l $(COUNTFILES)
127

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

137
138
139
140
141
# 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
142
-include .depend-concur