Makefile.in 37.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
CC        = @CC@
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
COQC      = @COQC@
COQDEP    = @COQDEP@
59 60
CAMLP5O   = @CAMLP5O@

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

71 72
RUBBER = @RUBBER@

73
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
74
#PDFVIEWER = @PDFVIEWER@
75

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

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

84 85
# external libraries common to all binaries

86
EXTOBJS =
Andrei Paskevich's avatar
Andrei Paskevich committed
87
EXTLIBS = str unix nums dynlink
88 89 90

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
91

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92 93 94
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95

96
all: @OCAMLBEST@ plugins
Francois Bobot's avatar
Francois Bobot committed
97

98 99 100 101
ifeq (@enable_local@,yes)
all: install_local
endif

102 103
plugins: plugins.@OCAMLBEST@

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
#############
108
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
110

111
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
112 113
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
François Bobot's avatar
François Bobot committed
114 115
	       src/driver/driver_lexer.ml src/coq_config.ml \
               src/session/xml.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116

117
LIB_UTIL = stdlib exn_printer pp debug loc print_tree print_number \
118
	   cmdline hashweak hashcons util sysutil rc plugin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119

120
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
121

122
LIB_PARSER = ptree denv typing parser lexer
123

124
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
125
	     whyconf autodetection
126

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

139
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
140
	      cvc3 yices
141

François Bobot's avatar
François Bobot committed
142 143
LIB_SESSION = xml termcode session session_tools session_scheduler

144
LIBMODULES = src/config src/coq_config \
145 146 147 148 149
	      $(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)) \
François Bobot's avatar
François Bobot committed
150 151
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
	      $(addprefix src/session/, $(LIB_SESSION))
152

François Bobot's avatar
François Bobot committed
153
LIBDIRS = util core parser driver transform printer session
154
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
155

156
ifeq (@enable_hypothesis_selection@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
157 158 159
  LIB_TRANSFORM += hypothesis_selection
  INCLUDES += -I @OCAMLGRAPHLIB@
  EXTLIBS += graph
160 161
endif

162 163 164 165
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
166

167
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
168
$(LIBCMX): OFLAGS += -for-pack Why3
169

170
# build targets
171

172 173
byte: src/why3.cma
opt:  src/why3.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174

175
src/why3.cma: src/why3.cmo
176 177
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

178
src/why3.cmxa: src/why3.cmx
179 180
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

181
src/why3.cmo: $(LIBCMO)
182
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
183

184
src/why3.cmx: $(LIBCMX)
185 186 187
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
188

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
191
.depend.lib: src/config.ml $(LIBGENERATED)
192
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193 194 195

depend: .depend.lib

196 197
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
198
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
199 200
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
201 202
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
203 204 205 206 207
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
208
	rm -f src/why3.cm[aiox] src/why3.[ao] src/why3.cmxa
209
	rm -f .depend.lib
210

211 212 213
###############
# installation
###############
214

215
install_no_local::
216 217
	mkdir -p $(BINDIR)
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
218
	mkdir -p $(DATADIR)/why3/emacs
219
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
220
	mkdir -p $(DATADIR)/why3/theories
221
	mkdir -p $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
222 223
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
224
	cp -f modules/*.mlw $(DATADIR)/why3/modules
Andrei Paskevich's avatar
Andrei Paskevich committed
225
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
226 227
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
228
	cp -rf share/javascript $(DATADIR)/why3/javascript
MARCHE Claude's avatar
MARCHE Claude committed
229
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
230 231
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

MARCHE Claude's avatar
MARCHE Claude committed
232 233
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
234
	cp -f src/why3.cm* $(OCAMLLIB)/why3
235
	cp -f META $(OCAMLLIB)/why3
236
	if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
237

238 239 240 241 242
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
243
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
244
install-lib: install_no_local_lib
245 246
endif

MARCHE Claude's avatar
MARCHE Claude committed
247 248
install-all: install install-lib

249 250 251 252 253 254 255
##################
# Why plugins
##################

PLUGGENERATED =

PLUG_PARSER = genequlin
256
PLUG_PRINTER = tptpfof
257 258
PLUG_TRANSFORM =

259
PLUGINS = genequlin tptpfof
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326

PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGMLI = $(addsuffix .mli, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

PLUGDIRS = parser printer transform
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

plugins.byte: $(addsuffix .cmo, $(addprefix lib/plugins/, $(PLUGINS)))
plugins.opt : $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

lib/plugins/%.cmxs: plugins/parser/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/parser/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

lib/plugins/%.cmxs: plugins/printer/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/printer/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

lib/plugins/%.cmxs: plugins/transform/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/transform/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

include .depend.plugins

.depend.plugins: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I plugins $(PLUGINCLUDES) \
		$(PLUGML) $(PLUGMLI) > $@

depend: .depend.plugins

PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
	    $(addsuffix /*.annot, $(PLUGSDIRS)) \
	    $(addsuffix /*.output, $(PLUGSDIRS)) \
	    $(addsuffix /*.automaton, $(PLUGSDIRS)) \
	    $(addsuffix /*.o, $(PLUGSDIRS)) \
	    $(addsuffix /*~, $(PLUGSDIRS))

clean::
	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
	rm -f lib/plugins/*
	rm -f .depend.plugins

install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
	cp -f lib/plugins/* $(LIBDIR)/why3/plugins

327

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328
##################
329
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330 331
##################

332 333
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334

335
bin/why3.opt: src/why3.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
336 337
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
338 339
	$(STRIP) $@

340
bin/why3.byte: src/why3.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
341 342
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
343

344 345 346
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

347 348
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
349

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
351
	rm -f src/main.cm[iox] src/main.annot src/main.o
352
	rm -f bin/why3.byte bin/why3.opt bin/why3
353

354
install_no_local::
355
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
356 357

install_local: bin/why3
358

359 360 361
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
362

363
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
364
	    pgm_module pgm_wp pgm_env pgm_typing pgm_ocaml pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
365

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

368 369 370 371 372
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

373
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
374 375

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

377 378
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
379

380
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
381 382
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383 384
	$(STRIP) $@

385
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
386 387 388
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

389 390 391
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

392
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
393 394

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
399 400 401
depend: .depend.programs

clean::
402 403
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
404
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
405
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406

407 408
# test target

409 410
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
411

412 413
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
414

415 416
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
417

418 419
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
420

421 422 423
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

424
install_no_local::
425
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml$(EXE)
426

427
install_local: bin/why3ml
428

429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
########
# Whyml (new API)
########

MLW_FILES = mlw_ty

MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))

MLWML  = $(addsuffix .ml,  $(MLWMODULES))
MLWMLI = $(addsuffix .mli, $(MLWMODULES))
MLWCMO = $(addsuffix .cmo, $(MLWMODULES))
MLWCMX = $(addsuffix .cmx, $(MLWMODULES))

$(MLWCMO) $(MLWCMX): INCLUDES += -I src/whyml

# build targets

byte: $(MLWCMX)
opt:  $(MLWCMO)

# depend and clean targets

include .depend.whyml

.depend.whyml:
	$(OCAMLDEP) -slash -I src -I src/whyml $(MLWML) $(MLWMLI) > $@

depend: .depend.whyml

clean::
	rm -f src/whyml/*.cm[iox] src/whyml/*.o
	rm -f src/whyml/*.annot src/whyml/*~
#	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
	rm -f .depend.whyml

464 465 466 467
##########
# gallery
##########

468
# we export exactly the programs that have a why3session.xml file
469 470 471

.PHONY: gallery

472 473
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
474 475 476
	@for x in `find examples/programs/ -name why3session.xml`; do \
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
477 478 479
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
480 481 482 483
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	  cd examples/programs/; \
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
	  cd ../..; \
484
	done
485

486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
########
# 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

503 504
byte: bin/why3config.byte
opt:  bin/why3config.opt
505

506
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
507 508 509 510
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

511
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
512 513 514
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

515 516 517
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

518 519 520 521 522 523 524 525 526 527 528 529 530
# 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
531
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
532 533
	rm -f .depend.config

534 535
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
536
		--detect --conf_file why.conf
537

538
install_no_local::
539
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
540

541
install_local: bin/why3config
542

MARCHE Claude's avatar
MARCHE Claude committed
543 544 545 546
###############
# IDE
###############

547 548
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
549
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
550 551 552 553 554 555 556 557

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

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

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

560
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
561

562 563
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
564

565
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
566
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
567
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
568

569
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
570
	$(if $(QUIET), @echo 'Linking  $@' &&) \
571
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
572 573
	$(STRIP) $@

574
bin/why3ide.byte: src/why3.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
575
	$(if $(QUIET),@echo 'Linking  $@' &&) \
576
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
577

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

MARCHE Claude's avatar
MARCHE Claude committed
581 582 583 584
# depend and clean targets

include .depend.ide

François Bobot's avatar
François Bobot committed
585
.depend.ide:
586
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
587 588 589 590

depend: .depend.ide

clean::
591
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
592 593
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
594
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
595 596
	rm -f .depend.ide

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

install_local: bin/why3ide
601

602
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
603

604

MARCHE Claude's avatar
MARCHE Claude committed
605 606 607 608
###############
# Replayer
###############

François Bobot's avatar
François Bobot committed
609
REPLAYER_FILES = replay
MARCHE Claude's avatar
MARCHE Claude committed
610 611 612 613 614 615 616 617

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
618
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
619 620 621 622 623 624

# build targets

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

625
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
626 627 628 629
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

630
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
631 632 633 634 635 636 637 638 639 640
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

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

# depend and clean targets

include .depend.replayer

François Bobot's avatar
François Bobot committed
641
.depend.replayer:
MARCHE Claude's avatar
MARCHE Claude committed
642 643 644 645 646 647 648 649 650 651 652
	$(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@

depend: .depend.replayer

clean::
	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::
653
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
MARCHE Claude's avatar
MARCHE Claude committed
654 655 656

install_local: bin/why3replayer

657 658 659 660
###############
# Stats
###############

François Bobot's avatar
François Bobot committed
661
STATS_FILES = stats
662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692

STATSMODULES = $(addprefix src/ide/, $(STATS_FILES))

STATSML  = $(addsuffix .ml,  $(STATSMODULES))
STATSMLI = $(addsuffix .mli, $(STATSMODULES))
STATSCMO = $(addsuffix .cmo, $(STATSMODULES))
STATSCMX = $(addsuffix .cmx, $(STATSMODULES))

$(STATSCMO) $(STATSCMX): INCLUDES += -I src/ide

# build targets

byte: bin/why3stats.byte
opt:  bin/why3stats.opt

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

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

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

# depend and clean targets

include .depend.stats

François Bobot's avatar
François Bobot committed
693
.depend.stats:
694 695 696 697 698 699 700 701 702 703 704 705 706
	$(OCAMLDEP) -slash -I src -I src/ide $(STATSML) $(STATSMLI) > $@

depend: .depend.stats

clean::
	rm -f bin/why3stats.byte bin/why3stats.opt bin/why3stats
	rm -f .depend.stats

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

install_local: bin/why3stats

707 708 709 710
###############
# Html
###############

François Bobot's avatar
François Bobot committed
711
HTML_FILES = html_session
712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742

HTMLMODULES = $(addprefix src/ide/, $(HTML_FILES))

HTMLML  = $(addsuffix .ml,  $(HTMLMODULES))
HTMLMLI = $(addsuffix .mli, $(HTMLMODULES))
HTMLCMO = $(addsuffix .cmo, $(HTMLMODULES))
HTMLCMX = $(addsuffix .cmx, $(HTMLMODULES))

$(HTMLCMO) $(HTMLCMX): INCLUDES += -I src/ide

# build targets

byte: bin/why3html.byte
opt:  bin/why3html.opt

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

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

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

# depend and clean targets

include .depend.html

François Bobot's avatar
François Bobot committed
743
.depend.html:
744 745 746 747 748 749 750 751 752 753 754 755 756
	$(OCAMLDEP) -slash -I src -I src/ide $(HTMLML) $(HTMLMLI) > $@

depend: .depend.html

clean::
	rm -f bin/why3html.byte bin/why3html.opt bin/why3html
	rm -f .depend.html

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

install_local: bin/why3html

MARCHE Claude's avatar
MARCHE Claude committed
757

758
###############
759
# Bench
760 761
###############

762 763
ifeq (@enable_bench@,yes)

764
BENCH_FILES = worker db bench benchrc benchdb whybench
765 766 767 768 769 770 771 772

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

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

773
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/bench -I @SQLITE3LIB@
774 775 776

# build targets

777 778
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
779

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

783
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
784 785 786 787
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

788
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
789 790 791
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

792 793 794
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

795 796 797 798 799 800 801 802 803 804 805 806
# 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/*~
807
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
808 809 810
	rm -f .depend.bench

install_no_local::
811
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
812 813

install_local: bin/why3bench
814

815 816
endif

817 818 819
##############
# Coq plugin
##############
820

821
ifeq (@enable_coq_plugin@,yes)
822

823 824 825 826 827 828 829 830 831 832 833 834 835
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))

836
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
837

838 839
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
840

841 842
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
843

844
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
845 846
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

847
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
848 849
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

850 851 852 853
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
854

855
include .depend.coq-plugin
856

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

860
depend: .depend.coq-plugin
861 862 863 864 865 866

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)
867 868 869 870 871 872 873 874 875 876
	rm -f .depend.coq-plugin

endif

####################
# Coq realizations
####################

ifeq (@enable_coq_libs@,yes)

877
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
878 879
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))

880
COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
881 882
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))

883 884 885 886 887
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding Single Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
888 889

COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
890 891 892 893 894 895 896

COQV  = $(addsuffix .v,  $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))

%.vo: %.v
	$(COQC) -R lib/coq Why3 $<

897 898 899 900 901 902 903 904 905
src/coq_config.ml:
	echo "let realized_theories = [" > $@
	for f in $(COQLIBS_INT_FILES); do echo '  ["int"; "'"$$f"'"];'; done >> $@
	for f in $(COQLIBS_REAL_FILES); do echo '  ["real"; "'"$$f"'"];'; done >> $@
ifeq (@enable_coq_fp_libs@,yes)
	for f in $(COQLIBS_FP_FILES); do echo '  ["floating_point"; "'"$$f"'"];'; done >> $@
endif
	echo "]" >> $@

906 907 908 909
all: $(COQVO)

install_no_local::
	mkdir -p $(LIBDIR)/why3/coq
910 911
	mkdir -p $(LIBDIR)/why3/coq/int
	cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
912
	mkdir -p $(LIBDIR)/why3/coq/real
913
	cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
914 915
ifeq (@enable_coq_fp_libs@,yes)
	mkdir -p $(LIBDIR)/why3/coq/floating_point
916
	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
917
endif
918 919 920 921 922 923 924 925 926 927 928

install_local: $(COQVO)

include .depend.coq-libs

.depend.coq-libs:
	$(COQDEP) -slash -R lib/coq Why3 $(COQV) > $@

depend: .depend.coq-libs

clean::
929
	rm -f $(COQVO) $(addsuffix .glob, $(COQLIBS_FILES))
930
	rm -f .depend.coq-libs
931

932 933 934 935 936
else

src/coq_config.ml:
	echo "let realized_theories = []" > $@

937
endif
938

939 940 941
########
# Tptp2why
########
942

943
ifeq (@enable_whytptp@,yes)
944

945 946
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
947

François Bobot's avatar
François Bobot committed
948
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
949

950
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
951 952 953 954 955 956

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

957 958
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
959 960 961

# build targets

Andrei Paskevich's avatar
Andrei Paskevich committed
962 963
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt  opt : lib/plugins/whytptp.cmxs
964

Andrei Paskevich's avatar
Andrei Paskevich committed
965 966
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
967

Andrei Paskevich's avatar
Andrei Paskevich committed
968
lib/plugins/whytptp.cmxs: $(TPTPCMX)
969
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
970
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
971

Andrei Paskevich's avatar
Andrei Paskevich committed
972
lib/plugins/whytptp.cmo: $(TPTPCMO)
973
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
974 975
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
976
install_no_local::
Andrei Paskevich's avatar
Andrei Paskevich committed
977
	cp -f lib/plugins/whytptp.cm* $(LIBDIR)/why3/plugins/
François Bobot's avatar
François Bobot committed
978

979 980 981 982 983 984 985 986 987 988 989
# 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)
990
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
991
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
992
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
Andrei Paskevich's avatar
Andrei Paskevich committed
993
	rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
994 995
	rm -f .depend.tptp2why

996
endif
997

998 999 1000 1001
#######
# tools
#######