Makefile.in 20.5 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
###############

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

MARCHE Claude's avatar
db    
MARCHE Claude committed
233
234
# src/manager/db.ml: $(ORM_CMO) src/manager/orm_schema.ml
# 	ocaml -I src/orm src/manager/orm_schema.ml 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
235
236

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) \
MARCHE Claude's avatar
MARCHE Claude committed
245
246
247
248
249
250
251
252
253
254
255
256
		-I +sqlite3 $(EXTCMA) sqlite3.cma -o $@ $^

include .depend.manager

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

depend: .depend.programs

clean::
	rm -f src/manager/*.cm[iox] src/manager/*.o src/manager/*.annot
	rm -f bin/manager.byte bin/manager.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275

# 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)
276
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -I +threads -o $@ $(EXTCMXA) threads.cmxa lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277
278
279
	$(STRIP)    $@

bin/whyide.byte: $(GCMO)
280
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -I +threads -o $@ $(EXTCMA) lablgtk.cma lablgtksourceview2.cma threads.cma gtkThread.cmo $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
281
282
283
284
285
286
287
288
289
290
291

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
292

293
294
295
# test targets
##############

Francois Bobot's avatar
Francois Bobot committed
296
test: bin/why.byte  $(TOOLS)
297
	mkdir -p output_why3
298
299
300
301
302
303
304
305
306
307
	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
308
	@printf "*** Checking Coq file generation ***\\n"
309
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
310
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
311
312
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
313
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
314
		; do \
MARCHE Claude's avatar
MARCHE Claude committed
315
	  printf "Generating Coq file for $$i\\n" && bin/why.byte \
316
317
		-D drivers/coq.drv -I theories/ \
		-o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
318
	@printf "*** Checking Coq compilation ***\\n"
319
	@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
320

321
testl: bin/whyl.byte
322
	ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
323
324
325

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

Francois Bobot's avatar
Francois Bobot committed
327
328
329
#tools
######

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330
331
332
333
TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337
338
339
clean::
	rm -f bin/why-cpulimit

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340
# bench
341
#######
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342
343
344

.PHONY: bench test

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345
bench/bench: bench/bench.in config.status
346
	./config.status --file bench/bench
347

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348
349
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
350

Francois Bobot's avatar
   
Francois Bobot committed
351
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
352
353
354
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

Francois Bobot's avatar
Francois Bobot committed
355
356
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
	$(TOOLS)
357
358
359
360
361
362
	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
363

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
364
365
366
# installation
##############

367
install: install-binary install-lib install-man 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
368

369
BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
370
371

# install-binary should not depend on $(BINARYFILES); otherwise it
372
# enforces the compilation of why-ide, even when lablgtk2 is not installed
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
373
374
375
install-binary: 
	mkdir -p $(BINDIR)
	cp -f $(BINARY) $(BINDIR)/why$(EXE)
376
377
	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
378
379
	fi

380
install-lib: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
	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
419
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
420
421
422
	cp $(BINARY) $$HOME/bin/why
	cp $(WHYCONFIG) $$HOME/bin/why
	cp $(JESSIE) $$HOME/bin/jessie
423
424
	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
425
426
427
428
429
430
431
432
433
434
	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
435
436
437
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
439
DOC=doc/manual.pdf doc/manual.html 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
440
441
442

doc:: $(DOC)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
443
444
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
445
446
447
448

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
449
450
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
451

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
452
# API DOC
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
453
454
##############

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
455
456
457
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
458
	src/manager/state.mli
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
460
461
462
463
464
465
466
.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
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485


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

486
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
.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
543
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
544
545
546
547
548
549
550
551
552
553
554
555
	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
556
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
558
559
dep: 
	$(MAKE) depend
560
561
	cat .depend | ocamldot | dot -Tpdf > dep.pdf
	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
562

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
563
564
565
566
567
568
569
570
571
572
# distrib
#########

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

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

573
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
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
665
666
667
668
669
670
671
672
673
674
675
       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
676
677
	headache -c misc/headache_config.txt -h misc/header.txt \
		Makefile.in configure.in \
678
		*/*.ml */*/*.ml */*/*.ml[ily4] 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
679
680
681
682

# myself
########
Makefile: Makefile.in config.status
683
	./config.status --file Makefile
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
684
685
686
687
688
689
690

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

configure: configure.in
	autoconf 

691
src/driver/dynlink_compat.ml: src/driver/dynlink_compat.ml.in config.status
692
	./config.status --file src/driver/dynlink_compat.ml
693

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
694
695
696
697
# clean and depend
##################

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700
701
distclean:: clean
	rm -f Makefile config.status config.cache config.log
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
702
703
704
705
706
707
708
709

#################################################################
# 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:
710
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
711
712
713
714
715
716
717
718
# 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.