Makefile.in 31.9 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
3
#  Copyright (C) 2010-2011                                               #
4 5 6
#    François Bobot                                                      #
#    Jean-Christophe Filliâtre                                           #
#    Claude Marché                                                       #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
#    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
prefix	    = @prefix@
34 35 36 37 38
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
39
DATADIR = $(DESTDIR)@datarootdir@
40
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 55 56
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@

57 58
CAMLP5O   = @CAMLP5O@

59
ifeq (@enable_menhirlib@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
60 61
  MENHIR    = @MENHIR@ --table
  MENHIRINC = -I @MENHIRLIB@
62 63
  MENHIRLIB = menhirLib
else
Andrei Paskevich's avatar
Andrei Paskevich committed
64
  MENHIR    = @MENHIR@
65 66 67 68
  MENHIRINC =
  MENHIRLIB =
endif

69 70
RUBBER = @RUBBER@

71
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
72
#PDFVIEWER = @PDFVIEWER@
73

74 75
BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aer-29 -dtypes    -I src $(INCLUDES)
76

77
ifeq (@enable_profiling@,yes)
78 79 80 81
OFLAGS += -g -p
STRIP = true
endif

82 83
# external libraries common to all binaries

84
EXTOBJS =
François Bobot's avatar
META  
François Bobot committed
85
EXTLIBS = str unix nums @META_DYNLINK@
86 87 88

EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90 91 92
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93

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

96 97 98 99
ifeq (@enable_local@,yes)
all: install_local
endif

100 101
plugins: plugins.@OCAMLBEST@

102
.PHONY: byte opt clean depend all install install_local install_no_local
103
.PHONY: plugins plugins.byte plugins.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
#############
106
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

109
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
110 111
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
112
	       src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113

François Bobot's avatar
François Bobot committed
114
LIB_UTIL = stdlib exn_printer debug pp loc print_tree \
115
	   cmdline hashweak hashcons util sysutil rc plugin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116

117
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
118

119
LIB_PARSER = ptree denv typing parser lexer
120

121
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
122
	     whyconf autodetection
123

124
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
125
		inlining split_goal \
126
		eliminate_definition eliminate_algebraic \
127
		eliminate_inductive eliminate_let eliminate_if \
128 129
		libencoding discriminate protect_enumeration \
		encoding encoding_select \
130
		encoding_decorate encoding_bridge encoding_twin \
François Bobot's avatar
François Bobot committed
131
		encoding_explicit encoding_guard encoding_sort \
132
		encoding_instantiate simplify_array filter_trigger \
133 134
		introduction abstraction close_epsilon lift_epsilon \
	        eval_match
135

136 137
LIB_PRINTER = print_real alt_ergo why3printer smtv1 smtv2 \
		coq tptp simplify gappa cvc3
138

139 140 141 142 143 144
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)) \
145
	      $(addprefix src/printer/, $(LIB_PRINTER))
146

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

150
ifeq (@enable_hypothesis_selection@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
151 152 153
  LIB_TRANSFORM += hypothesis_selection
  INCLUDES += -I @OCAMLGRAPHLIB@
  EXTLIBS += graph
154 155
endif

156 157 158 159
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
160

161
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
162
$(LIBCMX): OFLAGS += -for-pack Why
163

164
# build targets
165

166 167
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
168

169
src/why.cma: src/why.cmo
170 171
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

172
src/why.cmxa: src/why.cmx
173 174
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

175 176
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
177

178 179 180 181
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
182

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183 184
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
185
.depend.lib: src/config.ml $(LIBGENERATED)
186
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
187 188 189

depend: .depend.lib

190 191
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
192
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
193 194
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
195 196
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
197 198 199 200 201 202
	   $(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
203
	rm -f .depend.lib
204

205 206 207
###############
# installation
###############
208

209
install_no_local::
210
	mkdir -p $(BINDIR)
211
	mkdir -p $(LIBDIR)/why3
212
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
213
	mkdir -p $(DATADIR)/why3/emacs
214
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
215 216
	mkdir -p $(DATADIR)/why3/theories
	mkdir -p $(DATADIR)/why3/theories/transform
217
	mkdir -p $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
218 219 220
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
	cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
221
	cp -f modules/*.mlw $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
222
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
223 224
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
225
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
226 227
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

MARCHE Claude's avatar
MARCHE Claude committed
228 229 230
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
	cp -f src/why.cm* $(OCAMLLIB)/why3
231
	cp -f META $(OCAMLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
232 233
	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi

234 235 236 237 238
ifeq (@enable_local@,yes)
install install-lib:
	@echo "Why is configured in local installation mode."
	@echo "To install Why, run ./configure --disable-local ; make ; make install"
else
239
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
240
install-lib: install_no_local_lib
241 242
endif

MARCHE Claude's avatar
MARCHE Claude committed
243 244
install-all: install install-lib

245

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
246
##################
247
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248 249
##################

250 251
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
252

253
bin/why3.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
254 255
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
256 257
	$(STRIP) $@

258
bin/why3.byte: src/why.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
259 260
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
261

262 263 264
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

265 266
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
267

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
268
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
269
	rm -f src/main.cm[iox] src/main.annot src/main.o
270
	rm -f bin/why3.byte bin/why3.opt bin/why3
271

272
install_no_local::
273 274 275
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3

install_local: bin/why3
276

277 278 279
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280

281 282
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
	    pgm_module pgm_wp pgm_env pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
283

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

286 287 288 289 290
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

291
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
292 293

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

295 296
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
297

298
bin/why3ml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
299 300
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
301 302
	$(STRIP) $@

303
bin/why3ml.byte: src/why.cma $(PGMCMO) src/main.cmo
304 305 306
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

307 308 309
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

310
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
311 312

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

314
.depend.programs:
315
	$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
317 318 319
depend: .depend.programs

clean::
320 321
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
322
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
323
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324

325 326
# test target

327 328
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
329

330 331
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
332

333 334
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
335

336 337
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
338

339 340 341
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

342
install_no_local::
343
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
344

345
install_local: bin/why3ml
346

347 348 349 350
##########
# gallery
##########

351
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
352
        power mergesort_list mac_carthy isqrt insertion_sort_list flag \
353
	distance muller fib_memo fibonacci \
354 355
        vstte10_aqueue vstte10_inverting vstte10_max_sum \
	vstte10_queens vstte10_search_list \
356
        vacid_0_sparse_array
357 358 359

.PHONY: gallery

360 361 362 363 364 365 366
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	@for f in $(GALLERYPGMS); do \
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
	done
367

368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
########
# Config
########

CONFIG_FILES = whyconfig

CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))

CONFIGML  = $(addsuffix .ml,  $(CONFIGMODULES))
CONFIGMLI = $(addsuffix .mli, $(CONFIGMODULES))
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

$(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs

# build targets

385 386
byte: bin/why3config.byte
opt:  bin/why3config.opt
387

388
bin/why3config.opt: src/why.cmxa $(CONFIGCMX)
389 390 391 392
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

393
bin/why3config.byte: src/why.cma $(CONFIGCMO)
394 395 396
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

397 398 399
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

400 401 402 403 404 405 406 407 408 409 410 411 412
# depend and clean targets

include .depend.config

.depend.config: $(CONFIGGENERATED)
	$(OCAMLDEP) -slash -I src -I src/config $(CONFIGML) $(CONFIGMLI) > $@

depend: .depend.config

clean::
	rm -f src/config/*.cm[iox] src/config/*.o
	rm -f src/config/*.annot src/config/*~
	rm -f src/config/*.output src/config/*.automaton
413
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
414 415 416
	rm -f .why.conf
	rm -f .depend.config

417 418
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
419
		--detect --conf_file why.conf
420

421
install_no_local::
422
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
423

424
install_local: bin/why3config
425

MARCHE Claude's avatar
MARCHE Claude committed
426 427 428 429
###############
# IDE
###############

430 431
ifeq (@enable_ide@,yes)

432
IDE_FILES = xml session gconfig newmain
MARCHE Claude's avatar
MARCHE Claude committed
433 434 435 436 437 438 439 440

IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))

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

441
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
442

443
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
444

445 446
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
447

448
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
449
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
450
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
451

452
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
453
	$(if $(QUIET), @echo 'Linking  $@' &&) \
454
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
455 456
	$(STRIP) $@

457
bin/why3ide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
458
	$(if $(QUIET),@echo 'Linking  $@' &&) \
459
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
460

461 462 463
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
464 465 466 467
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
468
.depend.ide: src/ide/xml.ml
469
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
470 471 472 473

depend: .depend.ide

clean::
474
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
475 476
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
477
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
478 479
	rm -f .depend.ide

480
install_no_local::
481 482 483
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
484

485
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
486

487

MARCHE Claude's avatar
MARCHE Claude committed
488 489 490 491 492 493 494 495 496 497 498 499 500
###############
# Replayer
###############

REPLAYER_FILES = xml session replay

REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES))

REPLAYERML  = $(addsuffix .ml,  $(REPLAYERMODULES))
REPLAYERMLI = $(addsuffix .mli, $(REPLAYERMODULES))
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
501
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529

# build targets

byte: bin/why3replayer.byte
opt:  bin/why3replayer.opt

bin/why3replayer.opt: src/why.cmxa $(PGMCMX) $(REPLAYERCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why3replayer.byte: src/why.cma $(PGMCMO) $(REPLAYERCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

bin/why3replayer: bin/why3replayer.@OCAMLBEST@
	ln -sf why3replayer.@OCAMLBEST@ $@

# depend and clean targets

include .depend.replayer

.depend.replayer: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@

depend: .depend.replayer

clean::
530
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
531 532 533 534 535 536 537 538 539 540 541
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
	rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
	rm -f .depend.replayer

install_no_local::
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer

install_local: bin/why3replayer


542
###############
543
# Bench
544 545
###############

546 547
ifeq (@enable_bench@,yes)

548
BENCH_FILES = bench benchrc benchdb whybench
549 550 551

BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))

552
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
553 554 555 556 557 558

BENCHML  = $(addsuffix .ml,  $(BENCHMODULES))
BENCHMLI = $(addsuffix .mli, $(BENCHMODULES))
BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))

559
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
560 561 562

# build targets

563 564
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
565

Andrei Paskevich's avatar
Andrei Paskevich committed
566
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
567
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
568

569
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
570 571 572 573
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

574
bin/why3bench.byte: src/why.cma  $(PGMCMO) $(BENCHCMO)
575 576 577
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

578 579 580
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

581 582 583 584 585 586 587 588 589 590 591 592
# depend and clean targets

include .depend.bench

.depend.bench:
	$(OCAMLDEP) -slash -I src -I src/bench -I src/ide $(BENCHML) $(BENCHMLI) > $@

depend: .depend.bench

clean::
	rm -f src/bench/*.cm[iox] src/bench/*.o
	rm -f src/bench/*.annot src/bench/*~
593
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
594 595 596
	rm -f .depend.bench

install_no_local::
597 598 599
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
600

601 602
endif

603 604 605
##############
# Coq plugin
##############
606

607
ifeq (@enable_coq_support@,yes)
608

609 610 611 612 613 614 615 616 617 618 619 620 621
COQGENERATED = src/coq-plugin/g_whytac.ml

COQ_FILES = whytac g_whytac

COQMODULES = $(addprefix src/coq-plugin/, $(COQ_FILES))

COQML  = $(addsuffix .ml,  $(COQMODULES))
COQCMO = $(addsuffix .cmo, $(COQMODULES))
COQCMX = $(addsuffix .cmx, $(COQMODULES))

COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
COQINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQTREES))

622
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
623

624 625
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
626

627 628
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
629

630
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
631 632
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

633
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
634 635
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

636 637 638 639
src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
	$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@

# depend and clean targets
Andrei Paskevich's avatar
Andrei Paskevich committed
640

641 642 643 644 645 646 647 648 649 650 651 652 653 654
include .depend.coq

.depend.coq: $(COQGENERATED)
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

depend: .depend.coq

clean::
	rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
	rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
	rm -f src/coq-plugin/*.annot src/coq-plugin/*~
	rm -f $(COQGENERATED)
	rm -f .depend.coq

655
endif
656

657 658 659
########
# Tptp2why
########
660

661
ifeq (@enable_whytptp@,yes)
662

663 664
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
665

François Bobot's avatar
François Bobot committed
666
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
667

668
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
669 670 671 672 673 674

TPTPML  = $(addsuffix .ml,  $(TPTPMODULES))
TPTPMLI = $(addsuffix .mli, $(TPTPMODULES))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))

675 676
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
677 678 679

# build targets

François Bobot's avatar
François Bobot committed
680
plugins.byte byte: plugins/whytptp.cmo
681
plugins.opt  opt : plugins/whytptp.cmxs
682

François Bobot's avatar
François Bobot committed
683 684
plugins/whytptp.cmxs plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
plugins/whytptp.cmxs plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
685

686
plugins/whytptp.cmxs: $(TPTPCMX)
687
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
688
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
689

690
plugins/whytptp.cmo: $(TPTPCMO)
691
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
692 693
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
694
install_no_local::
695
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/
François Bobot's avatar
François Bobot committed
696

697 698 699 700 701 702 703 704 705 706 707
# depend and clean targets

include .depend.tptp2why

.depend.tptp2why: $(TPTPGENERATED)
	$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@

depend: .depend.tptp2why

clean::
	rm -f $(TPTPGENERATED)
708
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
709
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
710
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
711
	rm -f plugins/whytptp.cm* plugins/whytptp.o
712 713
	rm -f .depend.tptp2why

714
endif
715

716 717 718 719
#######
# tools
#######

720
TOOLS = bin/why3-cpulimit
721 722 723

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
724
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
725
	$(CC) -Wall -o $@ $^
726 727

clean::
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
728
	rm -f bin/why3-cpulimit src/tools/*~
729

730
install_no_local::
731
	cp -f bin/why3-cpulimit $(BINDIR)/why3-cpulimit
732

733 734 735 736
#########
# why3doc
#########

737 738
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762

WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))

WHY3DOCML  = $(addsuffix .ml,  $(WHY3DOCMODULES))
WHY3DOCMLI = $(addsuffix .mli, $(WHY3DOCMODULES))
WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))

$(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc

# build targets

byte: bin/why3doc.byte
opt:  bin/why3doc.opt

bin/why3doc.opt: src/why.cmxa $(WHY3DOCCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why3doc.byte: src/why.cma $(WHY3DOCCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

763 764 765
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

766 767 768
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

769 770
# depend and clean targets

771 772
WHY3DOCGENERATED=src/why3doc/to_html.ml

773 774
include .depend.why3doc

775
.depend.why3doc: $(WHY3DOCGENERATED)
776 777 778 779 780
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
781
	rm -f $(WHY3DOCGENERATED)
782 783
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
784
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
785 786
	rm -f .depend.why3doc

787 788
install_local: bin/why3doc

789 790 791 792
########
# bench
########

François Bobot's avatar
François Bobot committed
793
.PHONY: bench test comp_bench_plugins
794

795 796
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
	$(MAKE) test-api
797
	sh bench/bench \
798 799
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
800

801
BENCH_PLUGINS_CMO := helloworld.cmo
802 803 804
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

François Bobot's avatar
François Bobot committed
805 806 807
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
808
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
809 810 811
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
812 813

###############
814
# test targets
815
###############
816

817 818
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
819

820
test: bin/why3.byte plugins.byte $(TOOLS)
821
	mkdir -p output_why3
822 823 824 825 826
	bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
	# bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
	# bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
	# bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
	echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
827
	@printf "*** Checking Coq file generation ***\\n"
828
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
829
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
830 831
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
832
		floating_point.Test map.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
833
		; do \
834
	  printf "Generating Coq file for $$i\\n" && \
835
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
836
	@printf "*** Checking Coq compilation ***\\n"
837
	@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
838

839 840 841
testl: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
	ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
842

843 844
testl-debug: bin/why3ml.opt
	bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
845

846 847
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
848

849 850
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
851

MARCHE Claude's avatar
MARCHE Claude committed
852
test-api: src/why.cma
Andrei Paskevich's avatar
Andrei Paskevich committed
853
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/use_api.ml \
MARCHE Claude's avatar
MARCHE Claude committed
854
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
855

MARCHE Claude's avatar
MARCHE Claude committed
856
bts12244: src/why.cma
Andrei Paskevich's avatar
Andrei Paskevich committed
857
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/bts12244.ml
MARCHE Claude's avatar
MARCHE Claude committed
858

859 860

## Examples : Plugins ##
861

862
ifeq (@enable_plugins@,yes)
863

864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901
PLUGDIR = examples/plugins/
PLUG_FILES = genequlin

PLUGMODULES = $(addprefix $(PLUGDIR), $(PLUG_FILES))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES))

# ifeq (@enable_plug_support@,yes)
# byte: src/plug-plugin/whytac.cma
# opt:  src/plug-plugin/whytac.cmxs
# endif

# $(PLUGCMO):  src/why.cma
# $(PLUGCMXS): src/why.cmxa

.PHONY: examples_plugins.byte examples_plugins.opt

examples_plugins.byte : $(PLUGCMO)
examples_plugins.opt : $(PLUGCMXS)

# depend and clean targets

include .depend.plug

.depend.plug: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I $(PLUGDIR) $(PLUGML) | sed "s/cmx/cmxs/" > $@

depend: .depend.plug

clean::
	rm -f $(PLUGDIR)/*.cm[iox] $(PLUGDIR)/*.o
	rm -f $(PLUGDIR)/*.cma $(PLUGDIR)/*.cmxs
	rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~
	rm -f $(PLUGGENERATED)
	rm -f .depend.plug
902

903
endif
904

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
905 906 907
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
908

909 910 911 912 913
.PHONY: doc

ifeq (@enable_doc@,yes)

doc: doc/manual.pdf
MARCHE Claude's avatar
MARCHE Claude committed
914
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
915

916 917
BNF = qualid constant operator term type formula theory why_file  \
      typev expr module whyml_file
918
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
919 920 921 922 923 924 925 926

doc/%_bnf.tex: doc/%.bnf doc/bnf
	doc/bnf $< > $@

doc/bnf: doc/bnf.mll
	$(OCAMLLEX) $<
	$(OCAMLOPT) -o $@ doc/bnf.ml

927 928 929 930
DOC = api glossary ide intro library macros manpages \
      manual starting syntax syntaxref version whyml

DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
931

932
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
933
	cd doc; $(RUBBER) -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
934

935 936
# 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
937

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
938
clean::
939 940 941 942 943 944 945
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
946

947
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
948
# API DOC
949
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
950

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
951 952
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
953
MODULESTODOC = util/util util/hashweak \
954
	core/ident core/ty core/term core/decl core/theory \