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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

155
156
$(LIBCMI) : why.cmo why.cmx
	@echo -n
Francois Bobot's avatar
Francois Bobot committed
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
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
175
176
src/main.cmx : $(LIBCMI)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177
178
179
180
181
182
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) $^
183

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

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

PGM_GENERATED = src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \
Francois Bobot's avatar
Francois Bobot committed
193
194
195
196
	        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
197
198
199
200
201

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
202
$(PGM_CMO) $(PGM_CMX): $(LIBCMI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203

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

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

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

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

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

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

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

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

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

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

bin/whyide.opt: $(LIBCMXA) $(IDE_CMX)
266
	$(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
267
268
269
	$(STRIP)    $@

bin/whyide.byte: $(GCMO)
270
	$(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
271
272
273
274
275
276
277
278
279
280
281

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
282

283
284
285
286
##############
# Coq plugin
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
287
288
289
290
ifeq (@enable_coq_support@,yes)
byte: src/coq-plugin/whytac.cmo
opt:  src/coq-plugin/whytac.cmxs
endif
291
292

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

294
295
296
297
298
299
300
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 $^

301
302
303
# test targets
##############

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

329
330
testl: bin/whyml.byte
	ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw
331

332
333
examples/programs/%: bin/whyml.byte
	bin/whyml.byte -I theories examples/programs/$*.mlw
334

Francois Bobot's avatar
Francois Bobot committed
335
336
337
#tools
######

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
338
339
340
341
TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345
346
347
clean::
	rm -f bin/why-cpulimit

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348
# bench
349
#######
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350
351
352

.PHONY: bench test

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

Francois Bobot's avatar
   
Francois Bobot committed
356
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
357
358
359
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

Francois Bobot's avatar
Francois Bobot committed
360
361
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
	$(TOOLS)
362
363
364
365
366
367
	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
368

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
369
370
371
# installation
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
## 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
439

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
440
441
442
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
443

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
444
DOC=doc/manual.pdf doc/manual.html 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
445
446
447

doc:: $(DOC)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448
449
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
450
451
452
453

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
454
455
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
457
# API DOC
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
458
459
##############

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
460
461
462
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
463
	src/manager/db.mli
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
464

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
465
466
467
468
469
470
.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
471
			-I +sqlite3 $(APIDOCSRC)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
472
473
474
475
476


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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
491
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
492
493
	$(OCAMLLEX) $<

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
506
507
508
509
510
511
512
513
# 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
514
515
516
517
518
519
520
521
522
523
524

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
540
541
dep: 
	$(MAKE) depend
542
	cat .depend | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
543
#	$(PDFVIEWER) dep.pdf
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
547
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
# 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
654
655
656
657

# file headers
##############
headers:
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
658
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
659
	    Makefile.in configure.in */*.ml */*/*.ml */*/*.ml[ily4]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
660
661
662

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
664
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
665
666
667
668
	./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
669

Andrei Paskevich's avatar
Andrei Paskevich committed
670
671
672
673
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
674
675
676
677
678
679
680
681
682
	./config.status --recheck

configure: configure.in
	autoconf 

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
685
distclean:: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
686
687
	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
688
689
690
691
692
693
694
695

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