Makefile.in 21.9 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
DYNLINK = @DYNLINK@

ifeq ($(DYNLINK),Dynlink)
58
59
DYNLINKCMA  = dynlink.cma
DYNLINKCMXA = dynlink.cmxa
60
else
61
62
DYNLINKCMA = 
DYNLINKCMXA = 
63
64
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
68
           -I src/transform -I src/manager -I src 
BFLAGS   = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ 
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@ 
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@

78
GENERATED = src/config.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
TOOLS=bin/why-cpulimit

92
all: .depend $(BINARY) $(BINARYL) $(TOOLS) apidoc why-ide-@LABLGTK2@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93

94
95
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
96
97
98
99
100
101
102
103
104
105
106
107

.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

108
109
110
111
112
# version number
################

include Version

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

MARCHE Claude's avatar
MARCHE Claude committed
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
src/orm/sql_orm_header.ml: src/orm/sql_access.ml src/orm/convert.ml 
	ocaml src/orm/convert.ml $< $@


ORM_CMO := printer_utils.cmo sql_orm_header.cmo sql_orm.cmo
ORM_CMO := $(addprefix src/orm/,$(ORM_CMO))

src/manager/db.ml: $(ORM_CMO) src/manager/orm_schema.ml
	ocaml -I src/orm src/manager/orm_schema.ml 

src/orm/%.cmo: src/orm/%.ml
	ocamlc -c -I src/orm -I +sqlite3 $<

src/manager/orm_schema.ml: $(ORM_CMO)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
131
# why
132
#####
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
138
139
UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
            sysutil.cmo hashweak.cmo
140
141
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))

142
PARSER_CMO := ptree.cmo parser.cmo lexer.cmo denv.cmo typing.cmo 
143
144
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))

Francois Bobot's avatar
   
Francois Bobot committed
145
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
146
	split_conjunction.cmo encoding_decorate.cmo\
147
	remove_logic_definition.cmo eliminate_inductive.cmo\
148
	compile_match.cmo eliminate_algebraic.cmo\
149
	eliminate_let.cmo eliminate_definition.cmo
150
151
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))

152
153
DRIVER_CMO := driver_ast.cmo call_provers.cmo dynlink_compat.cmo \
              driver_parser.cmo\
154
155
	driver_lexer.cmo driver.cmo
DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
156

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

160
LIBCMO = src/config.cmo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
161
         $(TRANSFORM_CMO) $(PRINTER_CMO)
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
LIBCMX = $(LIBCMO:.cmo=.cmx)

$(LIBCMX): OFLAGS+=-for-pack Why

CMA  = why.cma
CMXA = why.cmxa

$(CMA): why.cmo
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

$(CMXA): why.cmx
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $(LIBCMO)
177

178
179
180
181
182
183
184
why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(INCLUDES) -pack -o $@ $(LIBCMX)


# bin/why

CMO = src/main.cmo
185
CMX = $(CMO:.cmo=.cmx)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
186

187
188
bin/why.opt: $(CMXA) $(CMX) 
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ str.cmxa unix.cmxa nums.cmxa $(DYNLINKCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189
190
	$(STRIP) $@

191
192
bin/why.byte: $(CMA) $(CMO) 
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ str.cma unix.cma nums.cma $(DYNLINKCMA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193
194


195
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196

MARCHE Claude's avatar
MARCHE Claude committed
197
198
199
200
201
MANAGER_CMO := db.cmo 
MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))

bin/manager.byte: $(MANAGER_CMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) \
MARCHE Claude's avatar
MARCHE Claude committed
202
		-thread -I +threads threads.cma sqlite3.cma -o $@ $^
MARCHE Claude's avatar
MARCHE Claude committed
203

204
205
206
# test targets
##############

Francois Bobot's avatar
Francois Bobot committed
207
test: bin/why.byte  $(TOOLS)
208
	mkdir -p output_why3
209
210
211
212
213
214
215
216
217
218
	ocamlrun -bt bin/why.byte -I theories/ -D drivers/why3.drv \
		-o output_why3 src/test.why
	bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		src/test.why -t Test -g G
	bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		--timeout 3 --prove src/test.why -t Test -g G
	bin/why.byte -D drivers/coq.drv -I theories/ \
		src/test.why -t Test -g G 
	echo bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		--timeout 1 --prove theories/real.why 
MARCHE Claude's avatar
MARCHE Claude committed
219
	@printf "*** Checking Coq file generation ***\\n"
220
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
221
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
222
223
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
224
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
225
		; do \
MARCHE Claude's avatar
MARCHE Claude committed
226
	  printf "Generating Coq file for $$i\\n" && bin/why.byte \
227
228
		-D drivers/coq.drv -I theories/ \
		-o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
229
	@printf "*** Checking Coq compilation ***\\n"
230
	@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
231

232
testl: bin/whyl.byte
233
	ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
234
235
236

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

238
239
240
# programs
##########

241
PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_typing.cmo pgm_main.cmo
242
PGM_CMO := $(addprefix src/programs/, $(PGM_CMO))
243
PGM_CMX = $(PGM_CMO:.cmo=.cmx)
244

245
$(PGM_CMO) $(PGM_CMX): INCLUDES=-I src/programs/
246

247
248
bin/whyl.opt: $(CMXA) $(PGM_CMX) 
	$(if $(QUIET), @echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ str.cmxa unix.cmxa nums.cmxa $^
249
250
	$(STRIP) $@

251
bin/whyl.byte: $(CMA) $(PGM_CMO) 
252
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ str.cma unix.cma nums.cma $^
253

Francois Bobot's avatar
Francois Bobot committed
254
255
256
257
258
259
#tools
######

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
260
# graphical interface
261
#####################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
262

263
264
IDE_CMO := ide_main.cmo
IDE_CMO := $(addprefix src/ide/,$(IDE_CMO))
265
IDE_CMX = $(IDE_CMO:.cmo=.cmx)
266

267
$(IDE_CMO) $(IDE_CMX): INCLUDES=-I src/ide/
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
268

269
270
271
why-ide-yes: bin/why-ide.$(OCAMLBEST)
why-ide-no:
why-ide: bin/why-ide.$(OCAMLBEST)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
272

273
274
bin/why-ide.opt: $(CMXA) $(IDE_CMX)
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -I +threads -o $@ str.cmxa nums.cmxa unix.cmxa threads.cmxa lablgtk.cmxa lablgtksourceview.cmxa gtkThread.cmx $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
275
276
	$(STRIP)    $@

277
bin/why-ide.byte: $(GCMO)
278
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -I +threads -o $@ str.cma nums.cma unix.cma lablgtk.cma lablgtksourceview.cma threads.cma gtkThread.cmo $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279
280

# bench
281
#######
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282
283
284
285
286

.PHONY: bench test

WHYVO=lib/coq/Why.vo

287
288
bench/bench : bench/bench.in config.status
	./config.status --file bench/bench
289

290
291
bench:: $(BINARY) $(BINARYL) bench/bench $(TOOLS)
	sh bench/bench "$(BINARY) -I theories/" "$(BINARYL) -I theories"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
292

Francois Bobot's avatar
   
Francois Bobot committed
293
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
294
295
296
297
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)


Francois Bobot's avatar
Francois Bobot committed
298

Francois Bobot's avatar
Francois Bobot committed
299
300
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
	$(TOOLS)
301
302
303
304
305
306
	bin/why.byte -D bench/plugins/helloworld.drv -I theories/ \
        src/test.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv -I theories/ \
        src/test.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/simplify_array.drv -I theories/ \
        src/test.why -t Test_simplify_array -g G
307

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
308
309
310
# installation
##############

311
install: install-binary install-lib install-man 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312

313
BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
314
315

# install-binary should not depend on $(BINARYFILES); otherwise it
316
# enforces the compilation of why-ide, even when lablgtk2 is not installed
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
317
318
319
install-binary: 
	mkdir -p $(BINDIR)
	cp -f $(BINARY) $(BINDIR)/why$(EXE)
320
321
	if test -f bin/why-ide.$(OCAMLBEST); then \
		cp -f bin/why-ide.$(OCAMLBEST) $(BINDIR)/why-ide-bin$(EXE); \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
322
323
	fi

324
install-lib: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
325
	mkdir -p $(LIBDIR)/why/why
326
#	cp -f $(PRELUDE) $(LIBDIR)/why/why
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
364
local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
365
366
367
	cp $(BINARY) $$HOME/bin/why
	cp $(WHYCONFIG) $$HOME/bin/why
	cp $(JESSIE) $$HOME/bin/jessie
368
369
	if test -f bin/why-ide.$(OCAMLBEST); then \
	  cp -f bin/why-ide.$(OCAMLBEST) $$HOME/bin/why-ide; \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
	fi

local: install

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


MARCHE Claude's avatar
API doc    
MARCHE Claude committed
420
# API DOC
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
421
422
##############

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
423
424
425
APIDOCSRC = $(UTIL_CMO:.cmo=.mli) $(CORE_CMO:.cmo=.mli) \
	src/driver/call_provers.mli \
	src/driver/driver.mli \
MARCHE Claude's avatar
MARCHE Claude committed
426
	src/manager/state.mli
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
428
429
430
431
432
433
434
.PHONY: apidoc

apidoc: $(APIDOCSRC)
	rm -f apidoc/* 
	mkdir -p apidoc
	$(OCAMLDOC) -d apidoc -html -I src/util -I src/core -I src/driver \
		$(APIDOCSRC)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453


# 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
###############

454
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470

.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
471
%.cmxs: %.ml %.cmx
Francois Bobot's avatar
Francois Bobot committed
472
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(INCLUDES) -o $@ $<
473

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
.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
511
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
512
513
514
515
516
517
518
519
520
521
522
523
	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
524
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
526
527
dep: 
	$(MAKE) depend
528
529
	cat .depend | ocamldot | dot -Tpdf > dep.pdf
	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
531
532
533
534
535
536
537
538
539
540
# distrib
#########

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

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

541
FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
       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
644
645
	headache -c misc/headache_config.txt -h misc/header.txt \
		Makefile.in configure.in \
646
		*/*.ml */*/*.ml */*/*.ml[ily4] 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
647
648
649
650

# myself
########
Makefile: Makefile.in config.status
651
	./config.status --file Makefile
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
652
653
654
655
656
657
658

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

configure: configure.in
	autoconf 

659
src/driver/dynlink_compat.ml: src/driver/dynlink_compat.ml.in config.status
660
	./config.status --file src/driver/dynlink_compat.ml
661

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
662
663
664
665
# clean and depend
##################

clean::
666
	rm -f *.cm*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
667
	rm -f src/*.cm[iox] src/*.o src/*~ src/*.annot src/*.output
668
	rm -f src/*/*.cm[iox] src/*/*.o src/*/*~ src/*/*.annot src/*/*.output
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
669
670
671
672
673
674
675
676
	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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
677
	rm -f bin/why.opt bin/why.byte
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
678
679
680
681
682
683
684
685
686
687
688
	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)
689
690
	rm -rf output_why3
	rm -f ergo.why
691
	rm -rf bench/plugins/*.cm[iox]* bench/plugins/*.annot
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
#	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
709
	$(OCAMLDEP) -slash $(INCLUDES) -I src/programs/ -I src/ide/ src/*/*.ml src/*/*.mli src/*.ml src/*.mli bench/plugins/*.ml > .depend
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
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:
736
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
737
738
739
740
741
742
743
744
# 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.