Makefile.in 21 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 64 65 66
BFLAGS = -w Aelz -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aelz -dtypes    -I src $(INCLUDES)

# 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

MARCHE Claude's avatar
MARCHE Claude committed
89
LIBGENERATED = src/config.ml src/userconf/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
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 = driver_ast call_provers driver_parser driver_lexer driver
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
LIB_USERCONF = rc whyconf
112

113 114 115 116 117 118 119 120
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)) \
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
	      $(addprefix src/userconf/, $(LIB_USERCONF))
121

122 123
LIBDIRS = util core parser driver transform printer userconf
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
124

125 126 127 128
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
129

130 131
$(LIBCMO) $(LIBCMX): INCLUDES = $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why
132

133
# build targets
134

135 136
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137

138
src/why.cma: src/why.cmo
139 140
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

141
src/why.cmxa: src/why.cmx
142 143
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

144 145
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
146

147 148 149 150
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

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

153
# depend target
154

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155 156 157
include .depend.lib

.depend.lib: $(LIBGENERATED)
158
	$(OCAMLDEP) -slash $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
159 160 161

depend: .depend.lib

162 163 164 165 166 167 168 169 170 171 172 173
# clean target

LIBSDIRS = $(addprefix src/, $(LIBDIRS))
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
174
##################
175
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
176 177 178 179 180
##################

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

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

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

190 191
src/main.cmo src/main.cmx: src/why.cmi

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
192 193 194
clean::
	rm -f src/main.cm[iox] src/main.annot
	rm -f bin/why.byte bin/why.opt
195

196 197 198
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199

200 201
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
202

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

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

207 208 209 210 211 212 213 214 215
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
216

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
217
byte: bin/whyml.byte
218
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
219

220 221 222
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
223 224
	$(STRIP) $@

225 226 227 228 229
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
230 231

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236 237 238
depend: .depend.programs

clean::
239 240 241
	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
242 243 244
	rm -f bin/whyml.byte bin/whyml.opt

###############
245
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
246 247
###############

248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266
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

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

268 269 270
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
271

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

include .depend.manager

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

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

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

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

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

292 293 294 295 296 297 298 299 300 301 302
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
303

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

309
bin/whyide.opt: src/why.cmxa $(IDE_CMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
310 311 312 313
	$(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
314

315
bin/whyide.byte: src/why.cma $(IDE_CMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
316 317 318
	$(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
319

320 321
# depend and clean targets

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
322 323 324
include .depend.ide

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

depend: .depend.ide

clean::
330 331
	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
332
	rm -f bin/whyide.byte bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
333

334 335 336 337
##############
# Coq plugin
##############

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

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

345 346 347 348
#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
349 350
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes

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

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

###############
392
# test targets
393
###############
394

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

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

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

426
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427
# installation
428
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498 499 500
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
501

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

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

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

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

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

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
519 520
.PHONY: apidoc

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

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

529
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530
# generic rules
531
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
532

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

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

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

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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
560 561 562 563 564 565 566 567
# 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
568 569 570 571 572 573 574 575 576 577 578

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

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
599 600 601
# distrib
#########

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

709
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
710
# file headers
711 712
###############

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
721
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
722 723 724 725
	./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
726

Andrei Paskevich's avatar
Andrei Paskevich committed
727 728 729 730
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
731 732 733
	./config.status --recheck

configure: configure.in
734
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
735

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

740
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
741

742
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
743 744
	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
745 746 747 748 749 750 751 752

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