Makefile.in 20.2 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

65
66
BFLAGS   = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ 
OFLAGS   = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
67

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68
# external libraries common to all binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70
71
EXTCMA = str.cma unix.cma nums.cma $(DYNLINKCMA)
EXTCMXA = $(EXTCMA:.cma=.cmxa)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
72

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
73
74
75
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77
all: @OCAMLBEST@
Francois Bobot's avatar
Francois Bobot committed
78

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
79
.PHONY: byte opt clean depend all
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
81
82
83
#############
# Why library 
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
86
87
88
89
90
LIBGENERATED = src/config.ml \
          src/parser/parser.mli src/parser/parser.ml src/parser/parser.output \
            src/parser/lexer.ml src/driver/driver_lexer.ml \
            src/driver/driver_parser.mli src/driver/driver_parser.ml \
	    src/driver/driver_parser.output \
	    src/driver/dynlink_compat.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92
depend: $(LIBGENERATED)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94
95
96
97
98
LIBDIRS=core util parser transform driver printer
LIBCLEAN=$(addprefix src/, $(LIBDIRS))
LIBCLEAN:=$(addsuffix /*.cm[iox], $(LIBCLEAN)) \
          $(addsuffix /*.annot, $(LIBCLEAN)) \
          $(addsuffix /*.o, $(LIBCLEAN)) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100
101
102
clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED) 
	rm -f why.cm[iox] why.a why.o $(LIBCMA) $(LIBCMXA)
103
104
105

include Version

106
doc/version.tex src/config.ml: Version version.sh config.status
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
	BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) COQVER=@COQVER@ ./version.sh
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113
114
UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
            sysutil.cmo hashweak.cmo
115
116
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))

117
PARSER_CMO := ptree.cmo parser.cmo lexer.cmo denv.cmo typing.cmo 
118
119
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))

Francois Bobot's avatar
   
Francois Bobot committed
120
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
121
	split_conjunction.cmo encoding_decorate.cmo\
122
	remove_logic_definition.cmo eliminate_inductive.cmo\
123
	compile_match.cmo eliminate_algebraic.cmo\
124
	eliminate_let.cmo eliminate_definition.cmo
125
126
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))

127
128
DRIVER_CMO := driver_ast.cmo call_provers.cmo dynlink_compat.cmo \
              driver_parser.cmo\
129
130
	driver_lexer.cmo driver.cmo
DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
131

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

135
LIBCMO = src/config.cmo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
136
         $(TRANSFORM_CMO) $(PRINTER_CMO)
137
138
LIBCMX = $(LIBCMO:.cmo=.cmx)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139
140
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
$(LIBCMO) $(LIBCMX): INCLUDES=$(LIBINCLUDES)
141
142
$(LIBCMX): OFLAGS+=-for-pack Why

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
143
144
LIBCMA  = why.cma
LIBCMXA = why.cmxa
145

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
146
147
148
149
byte: $(LIBCMA)
opt: $(LIBCMA) $(LIBCMXA)

$(LIBCMA): why.cmo
150
151
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152
$(LIBCMXA): why.cmx
153
154
155
156
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

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

158
159
160
why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(INCLUDES) -pack -o $@ $(LIBCMX)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
include .depend.lib

.depend.lib: $(LIBGENERATED)
	$(OCAMLDEP) -slash $(LIBINCLUDES) $(LIBCMO:.cmo=.ml) $(LIBCMO:.cmo=.mli) > $@

depend: .depend.lib

##################
# why binary
##################

byte: bin/why.byte
opt:  bin/why.opt

bin/why.opt: $(LIBCMXA) src/main.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why.byte: $(LIBCMA) src/main.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
181

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
182
183
184
clean::
	rm -f src/main.cm[iox] src/main.annot
	rm -f bin/why.byte bin/why.opt
185

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
186
187
188
189
190
191
192
193
194
195
196
197
##########
# whyml
##########

PGM_GENERATED = src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \
	        src/programs/pgm_parser.output src/programs/pgm_parser.ml 

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

$(PGM_CMO) $(PGM_CMX): INCLUDES=-I src/programs/
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199
200
201
202
203
opt:  bin/whyml.opt
byte: bin/whyml.byte

bin/whyml.opt: $(LIBCMXA) $(PGM_CMX) 
	$(if $(QUIET), @echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
204
205
	$(STRIP) $@

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
206
207
208
209
bin/whyml.byte: $(LIBCMA) $(PGM_CMO) 
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

include .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
210

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
211
212
.depend.programs: $(PGM_GENERATED)
	$(OCAMLDEP) -slash -I src/programs/ $(PGM_CMO:.cmo=.ml) $(PGM_CMO:.cmo=.mli) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214
215
216
217
218
219
220
221
depend: .depend.programs

clean::
	rm -f $(PGM_GENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o src/programs/*.annot
	rm -f bin/whyml.byte bin/whyml.opt

###############
222
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223
224
225
226
227
228
229
230
231
232
233
234
235
236
###############

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

$(ORM_CMO): INCLUDES=-I src/orm -I +sqlite3

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

src/manager/orm_schema.ml: $(ORM_CMO)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
237

MARCHE Claude's avatar
MARCHE Claude committed
238
239
240
MANAGER_CMO := db.cmo 
MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241
242
243
$(MANAGER_CMO): INCLUDES=-I src/manager -I +sqlite3 -I +threads

bin/manager.byte: $(LIBCMA) $(MANAGER_CMO)
MARCHE Claude's avatar
MARCHE Claude committed
244
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
		-thread -I +sqlite3 -I +threads $(EXTCMA) threads.cma sqlite3.cma -o $@ $^

# graphical interface
#####################

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

$(IDE_CMO) $(IDE_CMX): INCLUDES=-I src/ide/

byte: ide-byte-@LABLGTK2@
opt:  ide-opt-@LABLGTK2@

ide-byte-yes: bin/whyide.byte
ide-byte-no:
ide-opt-yes: bin/whyide.opt
ide-opt-no:

bin/whyide.opt: $(LIBCMXA) $(IDE_CMX)
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -I +threads -o $@ $(EXTCMXA) threads.cmxa lablgtk.cmxa lablgtksourceview.cmxa gtkThread.cmx $^
	$(STRIP)    $@

bin/whyide.byte: $(GCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -I +threads -o $@ $(EXTCMA) lablgtk.cma lablgtksourceview.cma threads.cma gtkThread.cmo $^

include .depend.ide

.depend.ide:
	$(OCAMLDEP) -slash -I src/ide/ $(IDE_CMO:.cmo=.ml) $(IDE_CMO:.cmo=.mli) > $@

depend: .depend.ide

clean::
	rm -f bin/whyide.byte bin/whyide.opt
	rm -f src/ide/*.cm[iox] src/ide/*.o src/ide/*.annot
MARCHE Claude's avatar
MARCHE Claude committed
281

282
283
284
# test targets
##############

Francois Bobot's avatar
Francois Bobot committed
285
test: bin/why.byte  $(TOOLS)
286
	mkdir -p output_why3
287
288
289
290
291
292
293
294
295
296
	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
297
	@printf "*** Checking Coq file generation ***\\n"
298
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
299
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
300
301
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
302
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
303
		; do \
MARCHE Claude's avatar
MARCHE Claude committed
304
	  printf "Generating Coq file for $$i\\n" && bin/why.byte \
305
306
		-D drivers/coq.drv -I theories/ \
		-o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
307
	@printf "*** Checking Coq compilation ***\\n"
308
	@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
309

310
testl: bin/whyl.byte
311
	ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
312
313
314

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

Francois Bobot's avatar
Francois Bobot committed
316
317
318
#tools
######

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319
320
321
322
TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

Francois Bobot's avatar
Francois Bobot committed
323
324
325
bin/why-cpulimit: src/tools/@CPULIMIT@.c
	$(CC) -o $@ $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326
327
328
clean::
	rm -f bin/why-cpulimit

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
329
# bench
330
#######
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331
332
333

.PHONY: bench test

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334
bench/bench: bench/bench.in config.status
335
	./config.status --file bench/bench
336

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337
338
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ bench/bench 
	sh bench/bench "bin/why.@OCAMLBEST@ -I theories/" "bin/whyml.@OCAMLBEST@ -I theories"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
339

Francois Bobot's avatar
   
Francois Bobot committed
340
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
341
342
343
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

Francois Bobot's avatar
Francois Bobot committed
344
345
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
	$(TOOLS)
346
347
348
349
350
351
	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
352

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
353
354
355
# installation
##############

356
install: install-binary install-lib install-man 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
357

358
BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359
360

# install-binary should not depend on $(BINARYFILES); otherwise it
361
# enforces the compilation of why-ide, even when lablgtk2 is not installed
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
362
363
364
install-binary: 
	mkdir -p $(BINDIR)
	cp -f $(BINARY) $(BINDIR)/why$(EXE)
365
366
	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
367
368
	fi

369
install-lib: 
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
	mkdir -p $(LIBDIR)/why/why

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
408
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
409
410
411
	cp $(BINARY) $$HOME/bin/why
	cp $(WHYCONFIG) $$HOME/bin/why
	cp $(JESSIE) $$HOME/bin/jessie
412
413
	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
414
415
416
417
418
419
420
421
422
423
	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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
425
426
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
428
DOC=doc/manual.pdf doc/manual.html 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
430
431

doc:: $(DOC)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
432
433
doc/manual.pdf: doc/manual.tex doc/version.tex
	make -C doc manual.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
434
435
436
437

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438
439
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
440

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
441
# API DOC
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
442
443
##############

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
444
445
446
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
447
	src/manager/state.mli
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
449
450
451
452
453
454
455
.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
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474


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

475
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
495
496
497
498
499
500
501
502
503
504
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
.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
532
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
533
534
535
536
537
538
539
540
541
542
543
544
	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
545
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
546

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
547
548
dep: 
	$(MAKE) depend
549
550
	cat .depend | ocamldot | dot -Tpdf > dep.pdf
	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
551

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
552
553
554
555
556
557
558
559
560
561
# distrib
#########

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

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

562
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
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
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
       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
665
666
	headache -c misc/headache_config.txt -h misc/header.txt \
		Makefile.in configure.in \
667
		*/*.ml */*/*.ml */*/*.ml[ily4] 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
668
669
670
671

# myself
########
Makefile: Makefile.in config.status
672
	./config.status --file Makefile
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
673
674
675
676
677
678
679

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

configure: configure.in
	autoconf 

680
src/driver/dynlink_compat.ml: src/driver/dynlink_compat.ml.in config.status
681
	./config.status --file src/driver/dynlink_compat.ml
682

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
683
684
685
686
# clean and depend
##################

clean::
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
687
	rm -f *~ */*~ */*/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
688

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
689
690
distclean:: clean
	rm -f Makefile config.status config.cache config.log
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
691
692
693
694
695
696
697
698

#################################################################
# 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:
699
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700
701
702
703
704
705
706
707
# 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.