Makefile.in 21.1 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1
2
##########################################################################
#                                                                        #
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
3
4
5
6
7
#  Copyright (C) 2010-                                                   #
#    Francois Bobot                                                      #
#    Jean-Christophe Filliatre                                           #
#    Johannes Kanig                                                      #
#    Andrei Paskevich                                                    #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8
9
10
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
11
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12
13
14
15
16
17
18
19
#  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.                  #
#                                                                        #
##########################################################################

Andrei Paskevich's avatar
Andrei Paskevich committed
20
include Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

22
23
24
25
26
27
VERBOSEMAKE ?= @enable_verbose_make@

ifeq ($(VERBOSEMAKE),yes)
  QUIET =
else
  QUIET = yes
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28
29
endif

30
# install the binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31
DESTDIR =
32
33
34
35
36
37
38
39
40

prefix 	    = @prefix@
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
DATADIR = $(DESTDIR)@datadir@
MANDIR  = $(DESTDIR)@mandir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
41

Andrei Paskevich's avatar
Andrei Paskevich committed
42
# OS specific stuff
43
44
EXE   = @EXE@
STRIP = @STRIP@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
46

# other variables
47
48
49
50
51
52
53
54
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
Andrei Paskevich's avatar
Andrei Paskevich committed
55
#CAMLP4   = @CAMLP4O@
56
57
58
59

OCAMLVERSION = @OCAMLVERSION@

#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
60
#PDFVIEWER = @PDFVIEWER@
61

62
63
BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -dtypes    -I src $(INCLUDES)
64
65
66

# external libraries common to all binaries

Andrei Paskevich's avatar
Andrei Paskevich committed
67
ifeq (@enable_plugins@,yes)
68
  DYNLINK = dynlink
69
else
70
  DYNLINK =
71
72
endif

73
74
75
EXTLIBS = str unix nums $(DYNLINK)
EXTCMA	= $(addsuffix .cma,$(EXTLIBS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77
78
79
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83
.PHONY: byte opt clean depend all
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
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88

89
LIBGENERATED = src/util/rc.ml \
90
91
92
93
	       src/parser/parser.mli src/parser/parser.ml \
	       src/parser/parser.output src/parser/lexer.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
	       src/driver/driver_parser.output src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94

95
LIB_UTIL = pp loc prtree util hashcons sysutil hashweak rc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96

97
LIB_CORE = ident ty term pattern decl theory task pretty trans env register
98

99
LIB_PARSER = ptree parser lexer denv typing
100

101
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver whyconf
102

103
104
105
106
107
LIB_TRANSFORM = simplify_recursive_definition inlining \
		split_conjunction encoding_decorate \
		remove_logic_definition eliminate_inductive \
		compile_match eliminate_algebraic \
		eliminate_let eliminate_definition
108

109
LIB_PRINTER = print_real alt_ergo why3 smt coq
110

111
112
113
114
115
116
LIBMODULES = src/config \
	      $(addprefix src/util/, $(LIB_UTIL)) \
	      $(addprefix src/core/, $(LIB_CORE)) \
	      $(addprefix src/parser/, $(LIB_PARSER)) \
	      $(addprefix src/driver/, $(LIB_DRIVER)) \
	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
117
	      $(addprefix src/printer/, $(LIB_PRINTER))
118

119
LIBDIRS = util core parser driver transform printer
120
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
121

122
123
124
125
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
126

127
128
$(LIBCMO) $(LIBCMX): INCLUDES = $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why
129

130
# build targets
131

132
133
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134

135
src/why.cma: src/why.cmo
136
137
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

138
src/why.cmxa: src/why.cmx
139
140
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

141
142
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
143

144
145
146
147
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

src/why.cmi: src/why.cmo src/why.cmx
148
	@echo -n
Francois Bobot's avatar
Francois Bobot committed
149

150
# depend target
151

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152
153
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
154
.depend.lib: src/config.ml $(LIBGENERATED)
155
	$(OCAMLDEP) -slash $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156
157
158

depend: .depend.lib

159
160
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
161
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
162
163
164
165
166
167
168
169
170
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
	rm -f src/why.cm[iox] src/why.[ao] src/why.cma src/why.cmxa

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171
##################
172
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173
174
175
176
177
##################

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

178
bin/why.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
179
180
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181
182
	$(STRIP) $@

183
bin/why.byte: src/why.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
184
185
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
186

187
188
src/main.cmo src/main.cmx: src/why.cmi

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
190
	rm -f src/main.cm[iox] src/main.annot src/main.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191
	rm -f bin/why.byte bin/why.opt
192

193
194
195
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196

197
198
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
	       src/programs/pgm_parser.output src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
199

200
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
201

202
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203

204
205
206
207
208
209
210
211
212
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

$(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs
$(PGMCMO) $(PGMCMX): src/why.cmi

# build targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214
byte: bin/whyml.byte
215
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
216

217
218
219
bin/whyml.opt: src/why.cmxa $(PGMCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220
221
	$(STRIP) $@

222
223
224
225
226
bin/whyml.byte: src/why.cma $(PGMCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227
228

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

230
231
.depend.programs: $(PGMGENERATED)
	$(OCAMLDEP) -slash -I src/programs $(PGMML) $(PGMMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233
234
235
depend: .depend.programs

clean::
236
237
238
	rm -f $(PGMGENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239
240
241
	rm -f bin/whyml.byte bin/whyml.opt

###############
242
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243
244
###############

245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
MNG_FILES = db test

MNGMODULES = $(addprefix src/manager/, $(MNG_FILES))

MNGML  = $(addsuffix .ml,  $(MNGMODULES))
MNGMLI = $(addsuffix .mli, $(MNGMODULES))
MNGCMO = $(addsuffix .cmo, $(MNGMODULES))
MNGCMX = $(addsuffix .cmx, $(MNGMODULES))

$(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3
$(MNGCMO) $(MNGCMX): src/why.cmi

#byte: bin/manager.byte
#opt:  bin/manager.opt

MARCHE Claude's avatar
MARCHE Claude committed
260
261
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3

262
263
bin/manager.opt: src/why.cmxa $(MNGCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
MARCHE Claude's avatar
MARCHE Claude committed
264
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^
265
	$(STRIP) $@
MARCHE Claude's avatar
MARCHE Claude committed
266

267
268
269
bin/manager.byte: src/why.cma $(MNGCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
270

271
# depend and clean targets
MARCHE Claude's avatar
MARCHE Claude committed
272
273
274

include .depend.manager

275
276
.depend.manager:
	$(OCAMLDEP) -slash -I src/manager/ $(MNGML) $(MNGMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
277

278
depend: .depend.manager
MARCHE Claude's avatar
MARCHE Claude committed
279
280

clean::
281
282
	rm -f src/manager/*.cm[iox] src/manager/*.o
	rm -f src/manager/*.annot src/manager/*~
MARCHE Claude's avatar
MARCHE Claude committed
283
	rm -f bin/manager.byte bin/manager.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284

285
#####################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286
287
288
# graphical interface
#####################

289
IDE_FILES = ide_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
290

291
292
293
294
295
296
297
298
299
300
301
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))

IDEML  = $(addsuffix .ml,  $(IDEMODULES))
IDEMLI = $(addsuffix .mli, $(IDEMODULES))
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

$(IDECMO) $(IDECMX): INCLUDES = -I src/ide -I +lablgtk2 -I +threads
$(IDECMO) $(IDECMX): src/why.cmi

# build targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
302

Andrei Paskevich's avatar
Andrei Paskevich committed
303
304
305
306
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt:  bin/whyide.opt
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
307

MARCHE Claude's avatar
MARCHE Claude committed
308
309
bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads

310
bin/whyide.opt: src/why.cmxa $(IDE_CMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
311
312
313
314
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
	    lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
	$(STRIP) $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
315

MARCHE Claude's avatar
MARCHE Claude committed
316

317
bin/whyide.byte: src/why.cma $(IDE_CMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
318
319
320
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
	    lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321

322
323
# depend and clean targets

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324
325
326
include .depend.ide

.depend.ide:
327
	$(OCAMLDEP) -slash -I src/ide $(IDEML) $(IDEMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328
329
330
331

depend: .depend.ide

clean::
332
333
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334
	rm -f bin/whyide.byte bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
335

336
337
338
339
##############
# Coq plugin
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
340
ifeq (@enable_coq_support@,yes)
341
#byte: src/coq-plugin/whytac.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
342
343
opt:  src/coq-plugin/whytac.cmxs
endif
344

345
COQTREES = kernel lib interp parsing proofs pretyping tactics library
Andrei Paskevich's avatar
Andrei Paskevich committed
346

347
348
349
350
#src/coq-plugin/whytac.cmo:  INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))

#src/coq-plugin/whytac.cmo:  BFLAGS+=-rectypes
351
352
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes

353
src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml
354
355
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
#######
# tools
#######

TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

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

clean::
	rm -f bin/why-cpulimit src/tools/*~

########
# bench
########

.PHONY: bench test

bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
	sh bench/bench \
	    "bin/why.@OCAMLBEST@ -I theories" \
	    "bin/whyml.@OCAMLBEST@ -I theories"

BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
	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

###############
394
# test targets
395
###############
396

397
test: bin/why.byte $(TOOLS)
398
	mkdir -p output_why3
399
400
401
402
403
404
405
	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/ \
406
		src/test.why -t Test -g G
407
	echo bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
408
		--timeout 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
409
	@printf "*** Checking Coq file generation ***\\n"
410
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
411
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
412
413
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
414
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
415
		; do \
MARCHE Claude's avatar
MARCHE Claude committed
416
	  printf "Generating Coq file for $$i\\n" && bin/why.byte \
417
418
		-D drivers/coq.drv -I theories/ \
		-o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
419
	@printf "*** Checking Coq compilation ***\\n"
420
	@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
421

422
423
testl: bin/whyml.byte
	ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw
424

425
426
examples/programs/%: bin/whyml.byte
	bin/whyml.byte -I theories examples/programs/$*.mlw
427

428
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
# installation
430
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
431

432
433
434
435
## install: install-binary install-lib install-man
##
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST)
##
Andrei Paskevich's avatar
Andrei Paskevich committed
436
437
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
438
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
439
440
441
442
443
## 	mkdir -p $(BINDIR)
## 	cp -f $(BINARY) $(BINDIR)/why$(EXE)
## 	if test -f bin/why-ide.$(OCAMLBEST); then \
## 		cp -f bin/why-ide.$(OCAMLBEST) $(BINDIR)/why-ide-bin$(EXE); \
## 	fi
444
445
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
446
## 	mkdir -p $(LIBDIR)/why/why
447
##
Andrei Paskevich's avatar
Andrei Paskevich committed
448
449
450
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
451
##
Andrei Paskevich's avatar
Andrei Paskevich committed
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
## 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
468
##
Andrei Paskevich's avatar
Andrei Paskevich committed
469
470
471
472
473
474
475
476
## 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 ======"
477
##
Andrei Paskevich's avatar
Andrei Paskevich committed
478
479
480
481
482
## 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
483
484
##
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
485
486
487
488
489
490
## 	cp $(BINARY) $$HOME/bin/why
## 	cp $(WHYCONFIG) $$HOME/bin/why
## 	cp $(JESSIE) $$HOME/bin/jessie
## 	if test -f bin/why-ide.$(OCAMLBEST); then \
## 	  cp -f bin/why-ide.$(OCAMLBEST) $$HOME/bin/why-ide; \
## 	fi
491
##
Andrei Paskevich's avatar
Andrei Paskevich committed
492
## local: install
493
##
Andrei Paskevich's avatar
Andrei Paskevich committed
494
495
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
496
##
Andrei Paskevich's avatar
Andrei Paskevich committed
497
498
## 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
499

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
500
501
502
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
503

504
DOC = doc/manual.pdf doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
505

506
doc: $(DOC)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
507

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
508
509
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
510
511
512
513

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
514
515
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
516

517
##########
MARCHE Claude's avatar
API doc    
MARCHE Claude committed
518
# API DOC
519
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
520

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
521
522
.PHONY: apidoc

523
apidoc:
MARCHE Claude's avatar
API doc    
MARCHE Claude committed
524
	mkdir -p apidoc
525
526
	$(OCAMLDOC) -d apidoc -html -I src $(LIBINCLUDES) -I +sqlite3 \
	    $(LIBML) $(LIBMLI) $(MNGML) $(MNGMLI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
527

528
529
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530

531
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
532
# generic rules
533
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
534

Andrei Paskevich's avatar
Andrei Paskevich committed
535
%.cmi: %.mli
536
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
537

538
%.cmo %cmi: %.ml
539
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
540

541
%.cmx: %.ml
542
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
543

544
%.cmxs: %.ml
545
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
546

Andrei Paskevich's avatar
Andrei Paskevich committed
547
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
548
549
	$(OCAMLLEX) $<

Andrei Paskevich's avatar
Andrei Paskevich committed
550
%.ml %.mli %.output: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
551
552
	$(OCAMLYACC) -v $<

Andrei Paskevich's avatar
Andrei Paskevich committed
553
554
# .ml4.ml:
# 	$(CAMLP4) pr_o.cmo -impl $< > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
555

Andrei Paskevich's avatar
Andrei Paskevich committed
556
557
# lib/coq/%.vo: lib/coq/%.v
# 	$(COQC8) -I lib/coq $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
558

Andrei Paskevich's avatar
Andrei Paskevich committed
559
560
# lib/coq-v7/%.vo: lib/coq-v7/%.v
# 	$(COQC7) -I lib/coq-v7 $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
561

Andrei Paskevich's avatar
Andrei Paskevich committed
562
563
564
565
566
567
568
569
# 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
570
571
572
573
574
575
576
577
578
579
580

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

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

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

tags:
Francois Bobot's avatar
   
Francois Bobot committed
581
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
582
583
584
585
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
586
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
587
588
589
590
591
592
593
	      "--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
594
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
595

596
dep:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
597
	$(MAKE) depend
598
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
599
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
600

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
601
602
603
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
604
605
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
606
#
Andrei Paskevich's avatar
Andrei Paskevich committed
607
608
609
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
610
#
Andrei Paskevich's avatar
Andrei Paskevich committed
611
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
612
613
614
615
616
#       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 \
Andrei Paskevich's avatar
Andrei Paskevich committed
617
618
619
620
621
622
623
# 	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 \
624
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
# 	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* \
643
644
645
#	frama-c-plugin/Makefile frama-c-plugin/configure \
# 	frama-c-plugin/*.ml* frama-c-plugin/share/jessie/*.h
#
Andrei Paskevich's avatar
Andrei Paskevich committed
646
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
647
#
Andrei Paskevich's avatar
Andrei Paskevich committed
648
# distrib export: source export-doc export-www export-examples export-examples-c linux
649
#
Andrei Paskevich's avatar
Andrei Paskevich committed
650
651
652
653
# 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
654
#
Andrei Paskevich's avatar
Andrei Paskevich committed
655
656
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
657
#
Andrei Paskevich's avatar
Andrei Paskevich committed
658
659
660
661
662
663
# 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
664
665
#
# tarball-for-framac:
Andrei Paskevich's avatar
Andrei Paskevich committed
666
667
# 	make tarball
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
668
669
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
670
671
672
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
# 	make export/$(NAME).tar.gz
673
#
Andrei Paskevich's avatar
Andrei Paskevich committed
674
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
675
#
Andrei Paskevich's avatar
Andrei Paskevich committed
676
677
678
679
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
# 	make -C $(WWW)/examples clean depend
# 	echo "*** faire make all dans $(WWW)/examples ***"
680
#
Andrei Paskevich's avatar
Andrei Paskevich committed
681
682
683
684
685
686
# 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
687
#
Andrei Paskevich's avatar
Andrei Paskevich committed
688
689
690
691
692
693
694
695
# 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)
696
#
Andrei Paskevich's avatar
Andrei Paskevich committed
697
# OSTYPE  ?= linux
698
#
Andrei Paskevich's avatar
Andrei Paskevich committed
699
# BINARYNAME = $(NAME)-$(OSTYPE)
700
#
Andrei Paskevich's avatar
Andrei Paskevich committed
701
# linux: binary
702
703
704
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
705
706
707
708
709
# 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)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
710

711
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
712
# file headers
713
714
###############

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
715
headers:
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
716
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
717
	    Makefile.in configure.in */*.ml */*/*.ml */*/*.ml[ily4]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
718

719
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
720
# myself
721
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
722

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
723
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
724
725
726
727
	./config.status --file $@

src/config.ml: src/config.ml.in config.status
	./config.status --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
728

Andrei Paskevich's avatar
Andrei Paskevich committed
729
730
731
732
doc/version.tex: doc/version.tex.in config.status
	./config.status --file $@

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
733
734
735
	./config.status --recheck

configure: configure.in
736
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
737

738
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
739
# clean and depend
740
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
741

742
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
743

744
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
745
746
	rm -f config.status config.cache config.log \
	    Makefile src/config.ml doc/version.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
747
748
749
750
751
752
753
754

#################################################################
# 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:
755
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
756
757
758
759
760
761
762
763
# 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.