Makefile.in 31.3 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
3
#  Copyright (C) 2010-2011                                               #
MARCHE Claude's avatar
MARCHE Claude committed
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
LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3
137

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

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

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

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

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

163
# build targets
164

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

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

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

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

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

# depend target
181

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

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

depend: .depend.lib

189 190
# clean target

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

204 205 206
###############
# installation
###############
207

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

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

233 234 235 236 237
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
238
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
239
install-lib: install_no_local_lib
240 241
endif

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

244

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

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

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

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

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

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

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

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

install_local: bin/why3
275

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

280 281
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
282

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

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

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

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

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

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

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

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

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

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

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

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

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

324 325
# test target

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

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

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

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

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

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

344
install_local: bin/why3ml
345

346 347 348 349
##########
# gallery
##########

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

.PHONY: gallery

359 360 361 362 363 364 365
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
366

367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
########
# 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

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

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

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

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

399 400 401 402 403 404 405 406 407 408 409 410 411
# 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
412
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
413 414 415
	rm -f .why.conf
	rm -f .depend.config

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

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

423
install_local: bin/why3config
424

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

429 430
ifeq (@enable_ide@,yes)

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

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

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

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

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

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

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

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

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

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

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

include .depend.ide

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

depend: .depend.ide

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

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

install_local: bin/why3ide
483

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

486

MARCHE Claude's avatar
MARCHE Claude committed
487 488 489 490 491 492 493 494 495 496 497 498 499
###############
# 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
500
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
501 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

# 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::
529
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
530 531 532 533 534 535 536 537 538 539 540
	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


541
###############
542
# Bench
543 544
###############

545 546
ifeq (@enable_bench@,yes)

547
BENCH_FILES = bench benchrc benchdb whybench
548 549 550

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

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

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

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

# build targets

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

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

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

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

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

580 581 582 583 584 585 586 587 588 589 590 591
# 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/*~
592
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
593 594 595
	rm -f .depend.bench

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

install_local: bin/why3bench
599

600 601
endif

602 603 604
##############
# Coq plugin
##############
605

606
ifeq (@enable_coq_support@,yes)
607

608 609 610 611 612 613 614 615 616 617 618 619 620
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))

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

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

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

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

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

635 636 637 638
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
639

640 641 642 643 644 645 646 647 648 649 650 651 652 653
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

654
endif
655

656 657 658
########
# Tptp2why
########
659

660
ifeq (@enable_whytptp@,yes)
661

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

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

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

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

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

# build targets

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

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

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

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

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

696 697 698 699 700 701 702 703 704 705 706
# 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)
707
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
708
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
709
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
710
	rm -f plugins/whytptp.cm* plugins/whytptp.o
711 712
	rm -f .depend.tptp2why

713
endif
714

715 716 717 718
#######
# tools
#######

719
TOOLS = bin/why3-cpulimit
720 721 722

byte opt: $(TOOLS)

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

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

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

732 733 734 735
#########
# why3doc
#########

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

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) $^

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

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

768 769
# depend and clean targets

770 771
WHY3DOCGENERATED=src/why3doc/to_html.ml

772 773
include .depend.why3doc

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

depend: .depend.why3doc

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

786 787
install_local: bin/why3doc

788 789 790 791
########
# bench
########

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

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

800
BENCH_PLUGINS_CMO := helloworld.cmo
801 802 803
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
804 805 806
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

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

###############
813
# test targets
814
###############
815

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

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

838 839 840
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
841

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

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

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

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

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

858 859

## Examples : Plugins ##
860

861
ifeq (@enable_plugins@,yes)
862

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

902
endif
903

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

908 909 910 911 912
.PHONY: doc

ifeq (@enable_doc@,yes)

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

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

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

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

926 927 928 929
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
930

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

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

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

else

doc:

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
952
MODULESTODOC = util/util util/hashweak \
953
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
954
	core/env core/task \
955 956
	driver/whyconf driver/driver \
	ide/session
MARCHE Claude's avatar
MARCHE Claude committed
957 958
#	transform/introduction \
#	ide/db