Makefile.in 37.5 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 \
114
	       src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
115

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

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

121
LIB_PARSER = ptree denv typing parser lexer
122

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

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

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

141
LIBMODULES = src/config \
142 143 144 145 146
	      $(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)) \
147
	      $(addprefix src/printer/, $(LIB_PRINTER))
148

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

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

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

163
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
164
$(LIBCMX): OFLAGS += -for-pack Why3
165

166
# build targets
167

168 169
byte: src/why3.cma
opt:  src/why3.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
170

171
src/why3.cma: src/why3.cmo
172 173
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

174
src/why3.cmxa: src/why3.cmx
175 176
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

177
src/why3.cmo: $(LIBCMO)
178
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
179

180
src/why3.cmx: $(LIBCMX)
181 182 183
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
184

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
185 186
include .depend.lib

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

depend: .depend.lib

192 193
# clean target

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

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
204
	rm -f src/why3.cm[aiox] src/why3.[ao] src/why3.cmxa
205
	rm -f .depend.lib
206

207 208 209
###############
# installation
###############
210

211
install_no_local::
212 213
	mkdir -p $(BINDIR)
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
214
	mkdir -p $(DATADIR)/why3/emacs
215
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
216
	mkdir -p $(DATADIR)/why3/theories
217
	mkdir -p $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
218 219
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
220
	cp -f modules/*.mlw $(DATADIR)/why3/modules
Andrei Paskevich's avatar
Andrei Paskevich 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
224
	cp -rf share/javascript $(DATADIR)/why3/javascript
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
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
230
	cp -f src/why3.cm* $(OCAMLLIB)/why3
231
	cp -f META $(OCAMLLIB)/why3
232
	if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
233

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 246 247 248 249 250 251
##################
# Why plugins
##################

PLUGGENERATED =

PLUG_PARSER = genequlin
252
PLUG_PRINTER = tptpfof
253 254
PLUG_TRANSFORM =

255
PLUGINS = genequlin tptpfof
256 257 258 259 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

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

323

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324
##################
325
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326 327
##################

328 329
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330

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

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

340 341 342
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

343 344
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
345

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
347
	rm -f src/main.cm[iox] src/main.annot src/main.o
348
	rm -f bin/why3.byte bin/why3.opt bin/why3
349

350
install_no_local::
351
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
352 353

install_local: bin/why3
354

355 356 357
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
358

359
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
360
	    pgm_module pgm_wp pgm_env pgm_typing pgm_ocaml pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
361

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

364 365 366 367 368
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

369
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
370 371

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

373 374
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
375

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

381
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
382 383 384
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

385 386 387
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

388
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389 390

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
395 396 397
depend: .depend.programs

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

403 404
# test target

405 406
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
407

408 409
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
410

411 412
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
413

414 415
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
416

417 418 419
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

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

423
install_local: bin/why3ml
424

425 426 427 428
##########
# gallery
##########

429
# we export exactly the programs that have a why3session.xml file
430 431 432

.PHONY: gallery

433 434
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
435 436 437
	@for x in `find examples/programs/ -name why3session.xml`; do \
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
438 439 440
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
441 442 443 444
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	  cd examples/programs/; \
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
	  cd ../..; \
445
	done
446

447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
########
# 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

464 465
byte: bin/why3config.byte
opt:  bin/why3config.opt
466

467
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
468 469 470 471
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

472
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
473 474 475
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

476 477 478
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

479 480 481 482 483 484 485 486 487 488 489 490 491
# 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
492
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
493 494
	rm -f .depend.config

495 496
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
497
		--detect --conf_file why.conf
498

499
install_no_local::
500
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
501

502
install_local: bin/why3config
503

MARCHE Claude's avatar
MARCHE Claude committed
504 505 506 507
###############
# IDE
###############

508 509
ifeq (@enable_ide@,yes)

510
IDE_FILES = xml termcode session gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
511 512 513 514 515 516 517 518

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

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

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

521
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
522

523 524
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
525

526
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
527
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
528
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
529

530
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
531
	$(if $(QUIET), @echo 'Linking  $@' &&) \
532
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
533 534
	$(STRIP) $@

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

539 540 541
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
542 543 544 545
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
546
.depend.ide: src/ide/xml.ml
547
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
548 549 550 551

depend: .depend.ide

clean::
552
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
553 554
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
555
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
556 557
	rm -f .depend.ide

558
install_no_local::
559
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE)
560 561

install_local: bin/why3ide
562

563
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
564

565

MARCHE Claude's avatar
MARCHE Claude committed
566 567 568 569
###############
# Replayer
###############

MARCHE Claude's avatar
MARCHE Claude committed
570
REPLAYER_FILES = xml termcode session replay
MARCHE Claude's avatar
MARCHE Claude committed
571 572 573 574 575 576 577 578

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
579
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
580 581 582 583 584 585

# build targets

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

586
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
587 588 589 590
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

591
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607
	$(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::
608
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
609 610 611 612 613 614
	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::
615
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
MARCHE Claude's avatar
MARCHE Claude committed
616 617 618

install_local: bin/why3replayer

619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
###############
# Stats
###############

STATS_FILES = xml termcode session session_ro stats

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

.depend.stats: src/ide/xml.ml
	$(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

669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718
###############
# Html
###############

HTML_FILES = xml termcode session session_ro html_session

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

.depend.html: src/ide/xml.ml
	$(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
719

720
###############
721
# Bench
722 723
###############

724 725
ifeq (@enable_bench@,yes)

726
BENCH_FILES = worker db bench benchrc benchdb whybench
727 728 729 730 731 732 733 734

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

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

735
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/bench -I @SQLITE3LIB@
736 737 738

# build targets

739 740
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
741

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

745
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
746 747 748 749
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

750
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
751 752 753
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

754 755 756
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

757 758 759 760 761 762 763 764 765 766 767 768
# 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/*~
769
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
770 771 772
	rm -f .depend.bench

install_no_local::
773
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
774 775

install_local: bin/why3bench
776

777 778
endif

779 780 781
##############
# Coq plugin
##############
782

783
ifeq (@enable_coq_plugin@,yes)
784

785 786 787 788 789 790 791 792 793 794 795 796 797
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))

798
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
799

800 801
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
802

803 804
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
805

806
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
807 808
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

809
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
810 811
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

812 813 814 815
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
816

817
include .depend.coq-plugin
818

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

822
depend: .depend.coq-plugin
823 824 825 826 827 828

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)
829 830 831 832 833 834 835 836 837 838
	rm -f .depend.coq-plugin

endif

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

ifeq (@enable_coq_libs@,yes)

839
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
840 841
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))

842
COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
843 844
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))

845 846 847 848 849
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
850 851

COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
852 853 854 855 856 857 858

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

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

859 860 861 862
drivers/coq-realizations.aux:
	echo "(* generated automatically at compilation time *)" > $@
	for f in $(COQLIBS_INT_FILES); do echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done >> $@
	for f in $(COQLIBS_REAL_FILES); do echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done >> $@
863
ifeq (@enable_coq_fp_libs@,yes)
864
	for f in $(COQLIBS_FP_FILES); do echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done >> $@
865 866
endif

867
opt byte: $(COQVO)
868 869 870

install_no_local::
	mkdir -p $(LIBDIR)/why3/coq
871 872
	mkdir -p $(LIBDIR)/why3/coq/int
	cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
873
	mkdir -p $(LIBDIR)/why3/coq/real
874
	cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
875 876
ifeq (@enable_coq_fp_libs@,yes)
	mkdir -p $(LIBDIR)/why3/coq/floating_point
877
	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
878
endif
879
	cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
880

881
install_local: $(COQVO) drivers/coq-realizations.aux
882 883 884 885 886 887 888 889 890

include .depend.coq-libs

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

depend: .depend.coq-libs

clean::
891
	rm -f $(COQVO) $(addsuffix .glob, $(COQLIBS_FILES))
892
	rm -f .depend.coq-libs
893

894 895
else

896 897
drivers/coq-realizations.aux:
	echo "(* generated automatically at compilation time *)" > $@
898

899
endif
900

901 902 903 904 905
opt byte: drivers/coq-realizations.aux

clean::
	rm -f drivers/coq-realizations.aux

906 907 908
########
# Tptp2why
########
909

910
ifeq (@enable_whytptp@,yes)
911

912 913
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
914

François Bobot's avatar
François Bobot committed
915
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
916

917
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
918 919 920 921 922 923

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

924 925
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
926 927 928

# build targets

Andrei Paskevich's avatar
Andrei Paskevich committed
929 930
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt  opt : lib/plugins/whytptp.cmxs
931

Andrei Paskevich's avatar
Andrei Paskevich committed
932 933
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
934

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

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

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

946 947 948 949 950 951 952 953 954 955 956
# 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)
957
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
958
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
959
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
Andrei Paskevich's avatar
Andrei Paskevich committed
960
	rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
961 962
	rm -f .depend.tptp2why

963
endif
964

965 966 967 968
#######
# tools
#######

969
TOOLS = bin/why3-cpulimit$(EXE)
970 971 972

byte opt: $(TOOLS)

973
bin/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
974
	$(CC) -Wall -o $@ $^
975 976

clean::
977
	rm -f bin/why3-cpulimit$(EXE) src/tools/*~
Andrei Paskevich's avatar