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

Andrei Paskevich's avatar
Andrei Paskevich committed
22
ifeq (@enable_verbose_make@,yes)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23
24
25
26
27
28
29
30
31
 QUIET = 
else    
 QUIET = yes
endif

# where to install the binaries
DESTDIR =
prefix=@prefix@
exec_prefix=@exec_prefix@
Andrei Paskevich's avatar
Andrei Paskevich committed
32
datarootdir=@datarootdir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33
34
BINDIR=$(DESTDIR)@bindir@
LIBDIR=$(DESTDIR)@libdir@
Andrei Paskevich's avatar
Andrei Paskevich committed
35
36
DATADIR=$(DESTDIR)@datadir@
MANDIR=$(DESTDIR)@mandir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
37

Andrei Paskevich's avatar
Andrei Paskevich committed
38
# OS specific stuff
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39
40
41
42
43
44
45
46
47
48
49
50
51
EXE=@EXE@
STRIP=@STRIP@

# other variables
OCAMLC   = @OCAMLC@ 
OCAMLOPT = @OCAMLOPT@ 
OCAMLDEP = @OCAMLDEP@
OCAMLLEX = @OCAMLLEX@
OCAMLYACC= @OCAMLYACC@
OCAMLDOC = @OCAMLDOC@
OCAMLLIB = @OCAMLLIB@
OCAMLBEST= @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
Andrei Paskevich's avatar
Andrei Paskevich committed
52
53
54
#CAMLP4   = @CAMLP4O@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
55

Andrei Paskevich's avatar
Andrei Paskevich committed
56
ifeq (@enable_plugins@,yes)
57
58
DYNLINKCMA  = dynlink.cma
DYNLINKCMXA = dynlink.cmxa
59
else
Andrei Paskevich's avatar
Andrei Paskevich committed
60
DYNLINKCMA  = 
61
DYNLINKCMXA = 
62
63
endif

Andrei Paskevich's avatar
Andrei Paskevich committed
64
65
BFLAGS = -w Aelz -dtypes -g $(INCLUDES)
OFLAGS = -w Aelz -dtypes    $(INCLUDES)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66

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

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

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
84
LIBGENERATED = src/config.ml src/userconf/rc.ml \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
86
87
          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 \
Andrei Paskevich's avatar
Andrei Paskevich committed
88
	    src/driver/driver_parser.output
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89

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

MARCHE Claude's avatar
MARCHE Claude committed
92
LIBDIRS=core util parser transform driver printer userconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93
94
95
96
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
97

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106
UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
MARCHE Claude's avatar
MARCHE Claude committed
107
            sysutil.cmo hashweak.cmo 
108
109
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))

110
PARSER_CMO := ptree.cmo parser.cmo lexer.cmo denv.cmo typing.cmo 
111
112
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))

Francois Bobot's avatar
   
Francois Bobot committed
113
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
114
	split_conjunction.cmo encoding_decorate.cmo\
115
	remove_logic_definition.cmo eliminate_inductive.cmo\
116
	compile_match.cmo eliminate_algebraic.cmo\
117
	eliminate_let.cmo eliminate_definition.cmo
118
119
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))

Andrei Paskevich's avatar
Andrei Paskevich committed
120
DRIVER_CMO := driver_ast.cmo call_provers.cmo \
MARCHE Claude's avatar
MARCHE Claude committed
121
              driver_parser.cmo driver_lexer.cmo driver.cmo  
122
DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
123

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

MARCHE Claude's avatar
MARCHE Claude committed
127
128
129
USERCONF_CMO := rc.cmo whyconf.cmo
USERCONF_CMO := $(addprefix src/userconf/,$(USERCONF_CMO))

130
LIBCMO = src/config.cmo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
MARCHE Claude's avatar
MARCHE Claude committed
131
         $(TRANSFORM_CMO) $(PRINTER_CMO) $(USERCONF_CMO)
132
133
LIBCMX = $(LIBCMO:.cmo=.cmx)

Andrei Paskevich's avatar
Andrei Paskevich committed
134
LIBINCLUDES = -I src $(addprefix -I src/, $(LIBDIRS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135
$(LIBCMO) $(LIBCMX): INCLUDES=$(LIBINCLUDES)
136
137
$(LIBCMX): OFLAGS+=-for-pack Why

Francois Bobot's avatar
Francois Bobot committed
138
LIBCMI  = why.cmi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139
140
LIBCMA  = why.cma
LIBCMXA = why.cmxa
141

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142
143
144
145
byte: $(LIBCMA)
opt: $(LIBCMA) $(LIBCMXA)

$(LIBCMA): why.cmo
146
147
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148
$(LIBCMXA): why.cmx
149
150
151
152
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

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

154
155
$(LIBCMI) : why.cmo why.cmx
	@echo -n
Francois Bobot's avatar
Francois Bobot committed
156

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160
161
162
163
164
165
166
167
168
169
170
171
172
173
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

Francois Bobot's avatar
Francois Bobot committed
174
175
src/main.cmx : $(LIBCMI)

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189
190
191
192
193
##########
# whyml
##########

PGM_GENERATED = src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \
Francois Bobot's avatar
Francois Bobot committed
194
195
196
197
	        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_ttree.cmo pgm_ptree.cmo
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198
199
200
201
202

PGM_CMO := $(addprefix src/programs/, $(PGM_CMO))
PGM_CMX = $(PGM_CMO:.cmo=.cmx)

$(PGM_CMO) $(PGM_CMX): INCLUDES=-I src/programs/
Francois Bobot's avatar
Francois Bobot committed
203
$(PGM_CMO) $(PGM_CMX): $(LIBCMI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
204

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
205
206
207
208
209
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
210
211
	$(STRIP) $@

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212
213
214
215
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
216

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
217
218
.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
219

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220
221
222
223
224
225
226
227
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

###############
228
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
229
230
###############

MARCHE Claude's avatar
whyrc    
MARCHE Claude committed
231
MANAGER_CMO := db.cmo test.cmo
MARCHE Claude's avatar
MARCHE Claude committed
232
233
MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))

MARCHE Claude's avatar
whyrc    
MARCHE Claude committed
234
$(MANAGER_CMO): INCLUDES=-I src/manager -I +sqlite3 -I +threads
Francois Bobot's avatar
Francois Bobot committed
235
$(MANAGER_CMO): $(LIBCMI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236
237

bin/manager.byte: $(LIBCMA) $(MANAGER_CMO)
MARCHE Claude's avatar
MARCHE Claude committed
238
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) \
MARCHE Claude's avatar
MARCHE Claude committed
239
240
241
242
243
244
245
246
247
248
249
250
		-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
251
252
253
254
255
256
257
258

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
259
$(IDE_CMO) $(IDE_CMX): INCLUDES=-I src/ide/ -I +lablgtk2 -I +threads
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
260

Andrei Paskevich's avatar
Andrei Paskevich committed
261
262
263
264
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt:  bin/whyide.opt
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
266

bin/whyide.opt: $(LIBCMXA) $(IDE_CMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
267
268
269
270
	$(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
271
272

bin/whyide.byte: $(GCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
273
274
275
	$(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
276
277
278
279
280
281
282
283
284
285
286

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
287

288
289
290
291
##############
# Coq plugin
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
292
293
294
295
ifeq (@enable_coq_support@,yes)
byte: src/coq-plugin/whytac.cmo
opt:  src/coq-plugin/whytac.cmxs
endif
296
297

COQSUBTREES = kernel lib interp parsing proofs pretyping tactics library
Andrei Paskevich's avatar
Andrei Paskevich committed
298

299
300
301
302
303
304
305
src/coq-plugin/whytac.cmo src/coq-plugin/whytac.cmxs: INCLUDES=$(COQSUBTREES:%=-I @COQLIB@/%) 
src/coq-plugin/whytac.cmo: BFLAGS+=-rectypes
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes

src/coq-plugin/whytac.cmxs: $(LIBCMXA) src/coq-plugin/whytac.ml
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

306
307
308
# test targets
##############

Francois Bobot's avatar
Francois Bobot committed
309
test: bin/why.byte  $(TOOLS)
310
	mkdir -p output_why3
311
312
313
314
315
316
317
318
319
320
	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
321
	@printf "*** Checking Coq file generation ***\\n"
322
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
323
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
324
325
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
326
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
327
		; do \
MARCHE Claude's avatar
MARCHE Claude committed
328
	  printf "Generating Coq file for $$i\\n" && bin/why.byte \
329
330
		-D drivers/coq.drv -I theories/ \
		-o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
331
	@printf "*** Checking Coq compilation ***\\n"
332
	@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
333

334
335
testl: bin/whyml.byte
	ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw
336

337
338
examples/programs/%: bin/whyml.byte
	bin/whyml.byte -I theories examples/programs/$*.mlw
339

Francois Bobot's avatar
Francois Bobot committed
340
341
342
#tools
######

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343
344
345
346
TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350
351
352
clean::
	rm -f bin/why-cpulimit

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
353
# bench
354
#######
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355
356
357

.PHONY: bench test

Andrei Paskevich's avatar
Andrei Paskevich committed
358
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359
	sh bench/bench "bin/why.@OCAMLBEST@ -I theories/" "bin/whyml.@OCAMLBEST@ -I theories"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360

Francois Bobot's avatar
   
Francois Bobot committed
361
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
362
363
364
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

Francois Bobot's avatar
Francois Bobot committed
365
366
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
	$(TOOLS)
367
368
369
370
371
372
	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
373

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
374
375
376
# installation
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
## install: install-binary install-lib install-man 
## 
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST) 
## 
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
## install-binary: 
## 	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
## 
## install-lib: 
## 	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
## 
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte 
## 	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
## 
## 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
444

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
445
446
447
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
449
DOC=doc/manual.pdf doc/manual.html 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
450
451
452

doc:: $(DOC)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
453
454
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
455
456
457
458

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
459
460
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
461

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
462
# API DOC
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
463
464
##############

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
465
466
467
APIDOCSRC = $(UTIL_CMO:.cmo=.mli) $(CORE_CMO:.cmo=.mli) \
	src/driver/call_provers.mli \
	src/driver/driver.mli \
MARCHE Claude's avatar
more db    
MARCHE Claude committed
468
	src/manager/db.mli
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
469

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
470
471
472
473
474
475
.PHONY: apidoc

apidoc: $(APIDOCSRC)
	rm -f apidoc/* 
	mkdir -p apidoc
	$(OCAMLDOC) -d apidoc -html -I src/util -I src/core -I src/driver \
MARCHE Claude's avatar
more db    
MARCHE Claude committed
476
			-I +sqlite3 $(APIDOCSRC)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
477
478
479
480
481


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

Francois Bobot's avatar
Francois Bobot committed
482
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs .output
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483

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

Andrei Paskevich's avatar
Andrei Paskevich committed
487
%.cmo %.cmi: %.ml
488
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
489

Andrei Paskevich's avatar
Andrei Paskevich committed
490
%.cmx %.o: %.ml
491
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
492

Francois Bobot's avatar
   
Francois Bobot committed
493
%.cmxs: %.ml %.cmx
494
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
495

Andrei Paskevich's avatar
Andrei Paskevich committed
496
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
497
498
	$(OCAMLLEX) $<

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
511
512
513
514
515
516
517
518
# 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
519
520
521
522
523
524
525
526
527
528
529

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

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

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

tags:
Francois Bobot's avatar
   
Francois Bobot committed
530
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
531
532
533
534
535
536
537
538
539
540
541
542
	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
543
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
544

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
550
551
552
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
# 
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
# 
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
#        mix/*.ml* \
#        version.sh Version Makefile.in configure.in configure .depend .depend.coq \
#        config/check_ocamlgraph.ml \
#        README INSTALL COPYING LICENSE CHANGES \
#        doc/Makefile doc/manual.ps doc/why.1 \
# 	examples-c/*/*.h examples-c/*/*.c \
# 	examples-c/Makefile examples-c/*/Makefile \
# 	examples-c/*/coq/*.v \
# 	examples/Makefile* \
# 	examples/*/*.mlw examples/*/*.why examples/*/*.v examples/*/*.sx \
# 	examples/*/.depend examples/*/Makefile \
# 	bench/bench.in bench/good*/*.mlw bench/good*/*.v \
#         bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
# 	bench/jc/bench bench/jc/good/*.jc \
# 	bench/java/bench bench/java/*/*.java bench/provers/*.mlw \
# 	tests/regtest.sh tests/java/*.java \
# 	tests/java/coq/*.v \
# 	tests/java/result/README tests/java/oracle/*.oracle \
# 	lib/coq*/*.v \
# 	lib/pvs/pvscontext.el lib/pvs/*.pvs lib/pvs/*.prf \
# 	lib/mizar/why.miz lib/mizar/dict/why.voc \
# 	lib/why/*.why lib/isabelle/*.thy lib/hol4/*.ml lib/harvey/*.rv \
# 	lib/java_api/java/*/*.java \
# 	lib/javacard_api/java/lang/*.java \
# 	lib/javacard_api/javacard/*/*.java \
# 	lib/javacard_api/javacardx/crypto/*.java \
# 	lib/javacard_api/com/sun/javacard/impl/*.java \
# 	lib/images/*.png \
# 	atp/*.ml atp/LICENSE.txt atp/Makefile atp/Mk_ml_file \
# 	ocamlgraph/configure.in ocamlgraph/configure ocamlgraph/.depend \
# 	ocamlgraph/Makefile.in ocamlgraph/META.in ocamlgraph/*/*.ml* \
#         frama-c-plugin/Makefile frama-c-plugin/configure \
# 	frama-c-plugin/*.ml* frama-c-plugin/share/jessie/*.h 
# 
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
# 
# distrib export: source export-doc export-www export-examples export-examples-c linux
# 
# export-www:
# 	echo "<#def version>$(VERSION)</#def>" > /users/demons/filliatr/www/why/version.prehtml
# 	echo "<#def cversion>$(CVERSION)</#def>" >> /users/demons/filliatr/www/why/version.prehtml
# 	make -C /users/demons/filliatr/www/why install
# 
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
# 
# export/$(NAME).tar.gz: $(FILES)
# 	rm -rf $(EXPORT)
# 	mkdir -p $(EXPORT)/bin
# 	cp --parents $(FILES) $(EXPORT)
# 	cd $(EXPORT); rm -f $(GENERATED)
# 	cd export; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
# 
# tarball-for-framac: 
# 	make tarball
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
# 
# tarball: 
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
# 	make export/$(NAME).tar.gz
# 
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
# 
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
# 	make -C $(WWW)/examples clean depend
# 	echo "*** faire make all dans $(WWW)/examples ***"
# 
# export-examples-c:
# 	mkdir -p $(WWW)/caduceus/examples
# 	cd examples-c; cp --parents */*.c */*.h $(WWW)/caduceus/examples
# 	mkdir -p $(WWW)/caduceus/examples/bench
# 	cp bench/c/good/*.c $(WWW)/caduceus/examples/bench
# 	rm -f $(WWW)/caduceus/examples/bench/test.c
# 
# export-doc: $(DOC)
# 	cp doc/manual.ps doc/manual.html $(WWW)/manual
# 	cp doc/logic_syntax.bnf $(WWW)/manual
# 	(cd $(WWW)/manual; hacha manual.html)
# 	cp doc/caduceus.ps doc/caduceus.html $(WWW)/caduceus/manual
# 	(cd $(WWW)/caduceus/manual; hacha caduceus.html)
# 	cp doc/krakatoa.pdf doc/krakatoa.html $(WWWKRAKATOA)/manual
# 	(cd $(WWWKRAKATOA)/manual; hacha krakatoa.html)
# 
# OSTYPE  ?= linux
# 
# BINARYNAME = $(NAME)-$(OSTYPE)
# 
# linux: binary
# 
# ALLBINARYFILES = $(FILES) $(BINARYFILES) 
# 
# binary: $(ALLBINARYFILES)
# 	mkdir -p export/$(BINARYNAME)
# 	cp --parents $(ALLBINARYFILES) export/$(BINARYNAME)
# 	(cd export; tar czf $(BINARYNAME).tar.gz $(BINARYNAME))
# 	cp export/$(BINARYNAME).tar.gz $(FTP)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
659
660
661
662

# file headers
##############
headers:
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
663
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
664
	    Makefile.in configure.in */*.ml */*/*.ml */*/*.ml[ily4]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
665
666
667

# myself
########
Andrei Paskevich's avatar
Andrei Paskevich committed
668

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
669
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
670
671
672
673
	./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
674

Andrei Paskevich's avatar
Andrei Paskevich committed
675
676
677
678
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
679
680
681
682
683
684
685
686
687
	./config.status --recheck

configure: configure.in
	autoconf 

# clean and depend
##################

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
690
distclean:: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
691
692
	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
693
694
695
696
697
698
699
700

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