Makefile.in 22.1 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1
2
##########################################################################
#                                                                        #
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
3
4
5
6
7
#  Copyright (C) 2010-                                                   #
#    Francois Bobot                                                      #
#    Jean-Christophe Filliatre                                           #
#    Johannes Kanig                                                      #
#    Andrei Paskevich                                                    #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8
9
10
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
11
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
50
51
52
#  described in file LICENSE.                                            #
#                                                                        #
#  This software is distributed in the hope that it will be useful,      #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
#                                                                        #
##########################################################################

VERBOSEMAKE ?= @VERBOSEMAKE@

ifeq ($(VERBOSEMAKE),yes)
 QUIET = 
else    
 QUIET = yes
endif

# where to install the binaries
DESTDIR =
prefix=@prefix@
datarootdir=@datarootdir@
exec_prefix=@exec_prefix@
BINDIR=$(DESTDIR)@bindir@
LIBDIR=$(DESTDIR)@libdir@

EXE=@EXE@
STRIP=@STRIP@

# where to install the man page
MANDIR=$(DESTDIR)@mandir@

# other variables
OCAMLC   = @OCAMLC@ 
OCAMLOPT = @OCAMLOPT@ 
OCAMLDEP = @OCAMLDEP@
OCAMLLEX = @OCAMLLEX@
OCAMLYACC= @OCAMLYACC@
OCAMLDOC = @OCAMLDOC@
OCAMLLIB = @OCAMLLIB@
OCAMLBEST= @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
CAMLP4   = @CAMLP4O@
53
54
PSVIEWER = @PSVIEWER@
PDFVIEWER = @PDFVIEWER@
55
56
57
58
59
60
61
62
63
64
DYNLINK = @DYNLINK@

ifeq ($(DYNLINK),Dynlink)
DYNLINKBFLAGS = dynlink.cma
DYNLINKOFLAGS = dynlink.cmxa
else
DYNLINKBFLAGS = 
DYNLINKOFLAGS = 
endif

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65

66
INCLUDES = -I src/core -I src/util -I src/driver -I src/parser -I src/printer \
67
           -I src/transform -I src/programs -I src 
68
BFLAGS   = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma $(DYNLINKBFLAGS)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
70
OFLAGS   = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa $(DYNLINKOFLAGS)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
71
72
73
74
75
76
77

COQC7  = @COQC7@
COQC8  = @COQC8@
COQDEP = @COQDEP@
COQLIB = "@COQLIB@"
COQVER = @COQVER@

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
78
GENERATED = src/version.ml src/parser/parser.mli src/parser/parser.ml \
79
80
            src/parser/lexer.ml src/driver/driver_lexer.ml \
            src/driver/driver_parser.mli src/driver/driver_parser.ml \
81
	    src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \
82
	    src/programs/pgm_parser.ml src/driver/dynlink_compat.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83
84
85
86
87

# main targets
##############

BINARY=bin/why.$(OCAMLBEST)
88
BINARYL=bin/whyl.$(OCAMLBEST)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89

Francois Bobot's avatar
Francois Bobot committed
90
91
92
TOOLS=bin/why-cpulimit

all: .depend $(BINARY) $(BINARYL) $(TOOLS)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93
94
95
96

# refrain parallel make (-j nn) from starting ocaml compilation too early 
*.cm*: .depend

97
98
opt: bin/why.opt bin/whyl.opt
byte: bin/why.byte bin/whyl.byte
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99
100
101
102
103
104
105
106
107
108
109
110

.PHONY: check

PRELUDE=lib/why/prelude.why $(WHYLIBS)

# sanity check: the prelude files do typecheck
check: $(BINARY) $(PRELUDE)
	WHYLIB=lib $(BINARY) --no-pervasives -tc lib/why/prelude.why
	for f in $(WHYLIBS) ; do \
		WHYLIB=lib $(BINARY) -tc $$f; \
	done

111
112
113
114
115
116
117
118
# version number
################

include Version

doc/version.tex src/version.ml: Version version.sh config.status
	BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) COQVER=$(COQVER) ./version.sh

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119
# why
120
#####
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
122
CORE_CMO := ident.cmo ty.cmo term.cmo pattern.cmo decl.cmo theory.cmo\
Francois Bobot's avatar
Francois Bobot committed
123
	task.cmo pretty.cmo trans.cmo env.cmo register.cmo
124
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
125

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
126
127
UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
            sysutil.cmo hashweak.cmo
128
129
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))

130
PARSER_CMO := parser.cmo lexer.cmo denv.cmo typing.cmo 
131
132
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))

Francois Bobot's avatar
   
Francois Bobot committed
133
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
134
	split_conjunction.cmo encoding_decorate.cmo\
135
136
	remove_logic_definition.cmo eliminate_inductive.cmo\
	compile_match.cmo
137
138
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))

139
140
141
DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\
	driver_lexer.cmo driver.cmo
DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
142

MARCHE Claude's avatar
MARCHE Claude committed
143
PRINTER_CMO := print_real.cmo alt_ergo.cmo why3.cmo smt.cmo coq.cmo
144
PRINTER_CMO := $(addprefix src/printer/,$(PRINTER_CMO))
145

146
CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
147
      $(TRANSFORM_CMO) $(PRINTER_CMO) src/main.cmo
148
CMX = $(CMO:.cmo=.cmx)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
149

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150
bin/why.opt: $(CMX) 
151
	echo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ nums.cmxa $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
153
154
	$(STRIP) $@

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155
bin/why.byte: $(CMO) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ nums.cma $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
157
158

bin/why.static: $(CMX) src/why.cmx 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
159
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ nums.cmxa $^ 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160
161
162
	$(STRIP) $@

bin/top: $(CMO)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
163
	ocamlmktop $(BFLAGS) -o $@ nums.cma $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
164

165
166
167
# test targets
##############

Francois Bobot's avatar
Francois Bobot committed
168
test: bin/why.byte  $(TOOLS)
169
	mkdir -p output_why3
170
	ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \
MARCHE Claude's avatar
MARCHE Claude committed
171
		--output-dir output_why3 --all-goals src/test.why
172
	bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
MARCHE Claude's avatar
MARCHE Claude committed
173
		--output-file - --goal Test.G src/test.why --timeout 3
174
	bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
MARCHE Claude's avatar
MARCHE Claude committed
175
		--call --goal Test.G src/test.why --timeout 3
MARCHE Claude's avatar
MARCHE Claude committed
176
177
	bin/why.byte --driver drivers/coq.drv -I theories/ \
		--output-file tmp.v --goal Test.G src/test.why 
MARCHE Claude's avatar
MARCHE Claude committed
178
179
180
181
182
	bin/why.byte --call --driver drivers/alt_ergo.drv -I theories/ \
		--goal ExpLog.Log_e theories/real.why 
	bin/why.byte --driver drivers/coq.drv -I theories/ \
		--output-file tmp.v --goal ExpLog.Log_e theories/real.why 
	coqc tmp.v
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183

184
testl: bin/whyl.byte
185
	ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
186
187
188

examples/programs/%: bin/whyl.byte
	bin/whyl.byte -I theories examples/programs/$*.mlw
189

190
191
192
# programs
##########

193
PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_typing.cmo pgm_main.cmo
194
195
PGM_CMO := $(addprefix src/programs/, $(PGM_CMO))

196
WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
197
           $(TRANSFORM_CMO) $(PRINTER_CMO) $(PGM_CMO)
198
199
200
201
202
203
204
205
206
WHYL_CMX = $(WHYL_CMO:.cmo=.cmx)

bin/whyl.opt: $(WHYL_CMX) 
	$(if $(QUIET), @echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ nums.cmxa $^
	$(STRIP) $@

bin/whyl.byte: $(WHYL_CMO) 
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ nums.cma $^

Francois Bobot's avatar
Francois Bobot committed
207
208
209
210
211
212
#tools
######

bin/why-cpulimit: src/tools/@CPULIMIT@.c
	$(CC) -o $@ $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213
# graphical interface
214
#####################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237

GCMO = $(CMO) intf/colors.cmo intf/tags.cmo intf/tools.cmo intf/tagsplit.cmo\
	      intf/astprinter.cmo intf/astnprinter.cmo intf/astpprinter.cmo\
	      intf/model.cmo intf/cache.cmo intf/gConfig.cmo intf/hilight.cmo\
	      intf/whyhilight.cmo intf/pprinter.cmo intf/preferences.cmo intf/stat.cmo
GCMX = $(GCMO:.cmo=.cmx)

gwhy-yes: bin/gwhy.$(OCAMLBEST)
gwhy-no:
gwhy: bin/gwhy.$(OCAMLBEST)

bin/gwhy.opt: $(GCMX)
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^
	$(STRIP)    $@

bin/gwhy.static: $(GCMX)
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^
	$(STRIP)    $@

bin/gwhy.byte: $(GCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ unix.cma str.cma nums.cma graph.cma lablgtk.cma threads.cma gtkThread.cmo $^

# bench
238
#######
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239
240
241
242
243

.PHONY: bench test

WHYVO=lib/coq/Why.vo

244
245
bench/bench : bench/bench.in config.status
	./config.status --file bench/bench
246

Francois Bobot's avatar
Francois Bobot committed
247
bench:: $(BINARY) bench/bench $(TOOLS)
248
	sh bench/bench "$(BINARY) -I theories/"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249

Francois Bobot's avatar
   
Francois Bobot committed
250
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
251
252
253
254
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)


Francois Bobot's avatar
Francois Bobot committed
255

Francois Bobot's avatar
Francois Bobot committed
256
257
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
	$(TOOLS)
258
	bin/why.byte --driver bench/plugins/helloworld.drv -I theories/ \
259
        --output-file - --goal Test.G src/test.why
260
	bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I theories/ \
261
        --output-file - --goal Test.G src/test.why
262
	bin/why.$(OCAMLBEST) --driver bench/plugins/simplify_array.drv -I theories/ \
Francois Bobot's avatar
Francois Bobot committed
263
        --output-file - --goal  Test_simplify_array.G src/test.why
264

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
266
267
# installation
##############

268
install: install-binary install-lib install-man 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
269

270
BINARYFILES = $(BINARY) bin/gwhy.$(OCAMLBEST) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
271
272
273
274
275
276
277
278
279
280

# install-binary should not depend on $(BINARYFILES); otherwise it
# enforces the compilation of gwhy, even when lablgtk2 is not installed
install-binary: 
	mkdir -p $(BINDIR)
	cp -f $(BINARY) $(BINDIR)/why$(EXE)
	if test -f bin/gwhy.$(OCAMLBEST); then \
		cp -f bin/gwhy.$(OCAMLBEST) $(BINDIR)/gwhy-bin$(EXE); \
	fi

281
install-lib: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282
	mkdir -p $(LIBDIR)/why/why
283
#	cp -f $(PRELUDE) $(LIBDIR)/why/why
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427

install-man:
	mkdir -p $(MANDIR)/man1
	cp -f doc/*.1 $(MANDIR)/man1

install-coq-no:
install-coq-yes: install-coq-@COQVER@
install-coq-v7:
	mkdir -p $(LIBDIR)/why/coq7
	cp -f $(V7FILES) $(LIBDIR)/why/coq7
	cp -f $(VO7) $(LIBDIR)/why/coq7
install-coq-v8 install-coq-v8.1:
	if test -w $(COQLIB) ; then \
	 mkdir -p $(COQLIB)/user-contrib ; \
	 cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
	 cp -f $(VO8) $(COQLIB)/user-contrib ; \
	else \
	echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
	mkdir -p $(LIBDIR)/why/coq ;\
	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
	fi

install-pvs-no:
install-pvs-yes: $(PVSFILES)
	mkdir -p $(PVSLIB)/why
	cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(PVSLIB)/why
	cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(PVSLIB)/why
	@echo "======  Compiling PVS theories, this may take some time ======"
	(cd $(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out)
	@echo "======  Done compiling PVS theories ======"

install-mizar-no:
install-mizar-yes:
	mkdir -p @MIZARLIB@/mml/dict
	cp lib/mizar/why.miz @MIZARLIB@/mml
	cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict

local-install: $(BINARY) $(WHYCONFIG) $(CADUCEUS) $(JESSIE) bin/gwhy.$(OCAMLBEST) byte bin/gwhy.byte 
	cp $(BINARY) $$HOME/bin/why
	cp $(WHYCONFIG) $$HOME/bin/why
	cp $(CADUCEUS) $$HOME/bin/caduceus
	cp $(JESSIE) $$HOME/bin/jessie
	if test -f bin/gwhy.$(OCAMLBEST); then \
	  cp -f bin/gwhy.$(OCAMLBEST) $$HOME/bin/gwhy; \
	fi

local: install
# local: bin/why.opt $(CADUCEUS) $(WHY2HTML) $(DP) $(RVMERGE) coq-@COQ@
# 	cp -f bin/why.opt $$HOME/bin/$$OSTYPE/why
# 	cp -f $(CADUCEUS) $$HOME/bin/$$OSTYPE/caduceus
# 	cp -f $(WHY2HTML) $$HOME/bin/$$OSTYPE/why2html
# 	cp -f $(DP) $$HOME/bin/$$OSTYPE/dp
# 	cp -f $(RVMERGE) $$HOME/bin/$$OSTYPE/rv_merge
# #	mkdir -p $(COQLIB)/contrib7/why
# #	cp -f $(VO7) $(VFILES) $(COQLIB)/contrib7/why
# #	mkdir -p $(COQLIB)/contrib/why
# #	cp -f $(VO8) $(VFILES) $(COQLIB)/contrib/why
# 	mkdir -p $(PVSLIB)/why
# 	cp $(PVSFILES) $(PVSLIB)/why
# 	mkdir -p $(MIZFILES)/mml/dict
# 	cp lib/mizar/why.miz $(MIZFILES)/mml
# 	cp lib/mizar/dict/why.voc $(MIZFILES)/mml/dict
# 	mkdir -p $$HOME/man/man1
# 	cp -f doc/*.1 $$HOME/man/man1

demons: $(STATICBINARY) doc/manual.ps
	cp -f $(STATICBINARY) /users/demons/demons/bin/$$OSTYPE/why
	cp doc/manual.ps /users/demons/demons/docs/why.ps

win: why.nsi
	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi

zip:
	zip -A -r why-$(VERSION).zip c:/why/bin c:/why/lib c:/coq/lib/contrib/why c:/coq/lib/contrib7/why

# doc

DOC=doc/manual.ps doc/manual.html doc/caduceus.ps doc/caduceus.html \
	doc/krakatoa.pdf doc/krakatoa.html \
	doc/main.pdf doc/main.html

doc:: $(DOC)


doc/manual.ps: doc/manual.tex doc/version.tex
	make -C doc manual.ps

# doc/version.tex: Version Makefile.in
#	echo '\newcommand{\whyversion}'"{$(VERSION)}" > $@
#	echo '\newcommand{\caduceusversion}'"{$(CVERSION)}" >> $@
#	echo '\newcommand{\jessieversion}'"{$(JCVERSION)}" >> $@
#	echo '\newcommand{\krakatoaversion}'"{$(KVERSION)}" >> $@

doc/manual.html: doc/manual.tex doc/version.tex
	make -C doc manual.html

doc/caduceus.ps: doc/caduceus.tex doc/version.tex
	make -C doc caduceus.ps

doc/caduceus.html: doc/caduceus.tex doc/version.tex
	make -C doc caduceus.html

doc/krakatoa.pdf: doc/krakatoa.tex doc/version.tex
	make -C doc krakatoa.pdf

doc/krakatoa.html: doc/krakatoa.tex doc/version.tex
	make -C doc krakatoa.html

doc/main.pdf: doc/main.tex doc/version.tex
	make -C doc main.pdf

doc/main.html: doc/main.tex doc/version.tex
	make -C doc main.html


# API HTML DOC
##############

OCAMLDOCSRC = intf/model.mli $(WHYCONFIGCMO:.cmo=.ml) $(WHYCONFIGCMI:.cmi=.mli)
	# $(JCCMO:.cmo=.ml) $(JCCMI:.cmi=.mli) 

apidoc: $(OCAMLDOCSRC)
	mkdir -p ocamldoc
	rm -f ocamldoc/* 
	$(OCAMLDOC) -d ocamldoc -html $(INCLUDES) @INCLUDEGTK2@ $(OCAMLDOCSRC)


# special rules
###############

# CAMLP4=@CAMLP4O@ pa_extend.cmo pa_macro.cmo

# src/%.cmo: src/%.ml4
# 	$(OCAMLC) -c $(BFLAGS) -pp "$(CAMLP4) -DOCAML@OCAMLV@ -impl" -impl $<

# src/%.cmx: src/%.ml4
# 	$(OCAMLOPT) -c $(OFLAGS) -pp "$(CAMLP4) -DOCAML@OCAMLV@ -impl" -impl $<

# src/%.ml: src/%.ml4
# 	$(CAMLP4) pr_o.cmo -DOCAML@OCAMLV@ -impl $< > $@

# generic rules
###############

428
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444

.mli.cmi:
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $<

.ml.cmi:
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $<

.ml.cmo:
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $<

.ml.o:
	$(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $<

.ml.cmx:
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $<

Francois Bobot's avatar
   
Francois Bobot committed
445
%.cmxs: %.ml %.cmx
Francois Bobot's avatar
Francois Bobot committed
446
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(INCLUDES) -o $@ $<
447

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
.mll.ml:
	$(OCAMLLEX) $<

.mly.ml:
	$(OCAMLYACC) -v $<

.mly.mli:
	$(OCAMLYACC) -v $<

.ml4.ml:
	$(CAMLP4) pr_o.cmo -impl $< > $@

lib/coq/%.vo: lib/coq/%.v
	$(COQC8) -I lib/coq $<

lib/coq-v7/%.vo: lib/coq-v7/%.v
	$(COQC7) -I lib/coq-v7 $<

jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile
	if test "@enable_apron@" = "yes" ; then \
	  echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \
	  cat jc/jc_annot_inference.ml >> jc/jc_ai.ml; \
	else \
	  echo "# 1 \"jc/jc_annot_fail.ml\"" > jc/jc_ai.ml; \
	  cat jc/jc_annot_fail.ml >> jc/jc_ai.ml; \
	fi

# %_why.v: %.mlw $(BINARY)
# 	$(BINARY) -coq $*.mlw

# %_why.pvs: %.mlw $(BINARY)
# 	$(BINARY) -pvs $*.mlw

# Emacs tags
############

tags:
Francois Bobot's avatar
   
Francois Bobot committed
485
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
486
487
488
489
490
491
492
493
494
495
496
497
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
	otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml

wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
499

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
500
501
dep: 
	$(MAKE) depend
502
503
	cat .depend | ocamldot | dot -Tpdf > dep.pdf
	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
504

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
# distrib
#########

NAME=why-$(VERSION)
EXPORT=export/$(NAME)

WWW = /users/www-perso/projets/why
FTP = $(WWW)/download
WWWKRAKATOA = /users/www-perso/projets/krakatoa

FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/gwhy.sh \
       mix/*.ml* \
       version.sh Version Makefile.in configure.in configure .depend .depend.coq \
       config/check_ocamlgraph.ml \
       README INSTALL COPYING LICENSE CHANGES \
       doc/Makefile doc/manual.ps doc/why.1 \
	examples-c/*/*.h examples-c/*/*.c \
	examples-c/Makefile examples-c/*/Makefile \
	examples-c/*/coq/*.v \
	examples/Makefile* \
	examples/*/*.mlw examples/*/*.why examples/*/*.v examples/*/*.sx \
	examples/*/.depend examples/*/Makefile \
	bench/bench.in bench/good*/*.mlw bench/good*/*.v \
        bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
	bench/jc/bench bench/jc/good/*.jc \
	bench/java/bench bench/java/*/*.java bench/provers/*.mlw \
	tests/regtest.sh tests/java/*.java \
	tests/java/coq/*.v \
	tests/java/result/README tests/java/oracle/*.oracle \
	lib/coq*/*.v \
	lib/pvs/pvscontext.el lib/pvs/*.pvs lib/pvs/*.prf \
	lib/mizar/why.miz lib/mizar/dict/why.voc \
	lib/why/*.why lib/isabelle/*.thy lib/hol4/*.ml lib/harvey/*.rv \
	lib/java_api/java/*/*.java \
	lib/javacard_api/java/lang/*.java \
	lib/javacard_api/javacard/*/*.java \
	lib/javacard_api/javacardx/crypto/*.java \
	lib/javacard_api/com/sun/javacard/impl/*.java \
	lib/images/*.png \
	atp/*.ml atp/LICENSE.txt atp/Makefile atp/Mk_ml_file \
	ocamlgraph/configure.in ocamlgraph/configure ocamlgraph/.depend \
	ocamlgraph/Makefile.in ocamlgraph/META.in ocamlgraph/*/*.ml* \
        frama-c-plugin/Makefile frama-c-plugin/configure \
	frama-c-plugin/*.ml* frama-c-plugin/share/jessie/*.h 

# ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c

distrib export: source export-doc export-www export-examples export-examples-c linux

export-www:
	echo "<#def version>$(VERSION)</#def>" > /users/demons/filliatr/www/why/version.prehtml
	echo "<#def cversion>$(CVERSION)</#def>" >> /users/demons/filliatr/www/why/version.prehtml
	make -C /users/demons/filliatr/www/why install

source: export/$(NAME).tar.gz
	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)

export/$(NAME).tar.gz: $(FILES)
	rm -rf $(EXPORT)
	mkdir -p $(EXPORT)/bin
	cp --parents $(FILES) $(EXPORT)
	cd $(EXPORT); rm -f $(GENERATED)
	cd export; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar

tarball-for-framac: 
	make tarball
	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz

tarball: 
	mkdir -p export
	cd export; rm -rf $(NAME) $(NAME).tar.gz
	make export/$(NAME).tar.gz

EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw

export-examples:
	cp --parents $(EXFILES) $(WWW)
	make -C $(WWW)/examples clean depend
	echo "*** faire make all dans $(WWW)/examples ***"

export-examples-c:
	mkdir -p $(WWW)/caduceus/examples
	cd examples-c; cp --parents */*.c */*.h $(WWW)/caduceus/examples
	mkdir -p $(WWW)/caduceus/examples/bench
	cp bench/c/good/*.c $(WWW)/caduceus/examples/bench
	rm -f $(WWW)/caduceus/examples/bench/test.c

export-doc: $(DOC)
	cp doc/manual.ps doc/manual.html $(WWW)/manual
	cp doc/logic_syntax.bnf $(WWW)/manual
	(cd $(WWW)/manual; hacha manual.html)
	cp doc/caduceus.ps doc/caduceus.html $(WWW)/caduceus/manual
	(cd $(WWW)/caduceus/manual; hacha caduceus.html)
	cp doc/krakatoa.pdf doc/krakatoa.html $(WWWKRAKATOA)/manual
	(cd $(WWWKRAKATOA)/manual; hacha krakatoa.html)

OSTYPE  ?= linux

BINARYNAME = $(NAME)-$(OSTYPE)

linux: binary

ALLBINARYFILES = $(FILES) $(BINARYFILES) 

binary: $(ALLBINARYFILES)
	mkdir -p export/$(BINARYNAME)
	cp --parents $(ALLBINARYFILES) export/$(BINARYNAME)
	(cd export; tar czf $(BINARYNAME).tar.gz $(BINARYNAME))
	cp export/$(BINARYNAME).tar.gz $(FTP)

# file headers
##############
headers:
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
618
619
	headache -c misc/headache_config.txt -h misc/header.txt \
		Makefile.in configure.in \
620
		*/*.ml */*/*.ml */*/*.ml[ily4] 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
621
622
623
624

# myself
########
Makefile: Makefile.in config.status
625
	./config.status --file Makefile
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
626
627
628
629
630
631
632

config.status: configure
	./config.status --recheck

configure: configure.in
	autoconf 

633
src/driver/dynlink_compat.ml: src/driver/dynlink_compat.ml.in config.status
634
	./config.status --file src/driver/dynlink_compat.ml
635

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
636
637
638
639
640
# clean and depend
##################

clean::
	rm -f src/*.cm[iox] src/*.o src/*~ src/*.annot src/*.output
641
	rm -f src/*/*.cm[iox] src/*/*.o src/*/*~ src/*/*.annot src/*/*.output
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
	rm -f c/*.cm[iox] c/*.o c/*~ c/*.annot c/*.output
	rm -f intf/*.cm[iox] intf/*.o intf/*~ intf/*.annot
	rm -f tools/*.cm[iox] tools/*.o tools/*~ tools/*.annot
	rm -f jc/*.cm[iox] jc/*.o jc/*~ jc/*.annot jc/*.output
	rm -f java/*.cm[iox] java/*.o java/*~ java/*.annot java/*.output
	rm -f ml/*.cm[iox] ml/*.o ml/*~ ml/*.annot
	rm -f ml/parsing/*.cm[iox] ml/parsing/*.o ml/parsing/*~ \
		ml/parsing/*.annot ml/parsing/*.output
	rm -f ml/utils/*.cm[iox] ml/utils/*.o ml/utils/*~ ml/utils/*.annot
	rm -f ml/typing/*.cm[iox] ml/typing/*.o ml/typing/*~ ml/typing/*.annot
	rm -f bin/why.opt bin/why.byte bin/why.static bin/top
	rm -f bin/caduceus.opt bin/caduceus.byte
	rm -f bin/jessie.opt bin/jessie.byte
	rm -f bin/jessica.opt bin/jessica.byte
	rm -f bin/why-obfuscator.opt bin/why-obfuscator.byte
	rm -f bin/rv_merge.opt bin/rv_merge.byte
	rm -f bin/why-stat.opt bin/why-stat.byte
	rm -f bin/tool-stat.opt bin/tool-stat.byte
	rm -f bin/why2html.opt bin/why2html.byte
	rm -f bin/why-dp.opt bin/why-dp.byte
	rm -f bin/why-cpulimit
	rm -f lib/coq*/*.vo lib/coq*/*~
	rm -f $(GENERATED)
665
666
	rm -rf output_why3
	rm -f ergo.why
667
	rm -rf bench/plugins/*.cm[iox]* bench/plugins/*.annot
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
#	make -C atp clean
#	make -C doc clean
#	if test -d examples-v7; then \
#		make -C examples-v7 clean ; \
#	fi
#	make -C examples clean

dist-clean:: clean
	rm -f Makefile config.status config.cache config.log

coq-clean::
	rm -f lib/coq*/*.vo examples/*/*.vo
	rm .depend.coq

.PHONY: depend
.depend depend: $(GENERATED)
	rm -f .depend
685
	$(OCAMLDEP) -slash $(INCLUDES) src/*/*.ml src/*/*.mli src/*.ml src/*.mli bench/plugins/*.ml > .depend
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
ifeq ($(FRAMAC),yes)
#	$(MAKE) -C $(JESSIE_PLUGIN_PATH) depend
endif

.depend.coq: #lib/coq*/*.v
	if test @COQ@ = yes; then \
	  rm -f .depend.coq; \
	  $(COQDEP) -I lib/coq lib/coq/*.v > .depend.coq; \
	  $(COQDEP) -I lib/coq-v7 lib/coq-v7/*.v >> .depend.coq; \
	else touch .depend.coq; \
	fi

alldepend:
	make -C examples-v7 depend
	make -C examples depend

include .depend
include .depend.coq

#################################################################
# Building the Why platform with ocamlbuild (OCaml 3.10 needed) #
#################################################################

# There used to be targets here but they are no longer useful.

# To build using Ocamlbuild:
# 1) Run "make Makefile" to ensure that the generated files (version.ml, ...)
# are generated.
# 2) Run Ocamlbuild with any target to generate the sanitization script.
# 3) Run ./sanitize to delete the generated files that shouldn't be generated
# (i.e. all lexers and parsers).
# 4) Run Ocamlbuild with the target you need, for example:
# ocamlbuild jc/jc_main.native

# You can also use the Makefile ./build.makefile which has some handy targets.