Makefile.in 37.3 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 src/coq_config.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 src/coq_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 360
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
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 = bench benchrc benchdb whybench
727 728 729

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

730
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
731 732 733 734 735 736

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

737
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
738 739 740

# build targets

741 742
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
743

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

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

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

756 757 758
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

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

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

install_local: bin/why3bench
778

779 780
endif

781 782 783
##############
# Coq plugin
##############
784

785
ifeq (@enable_coq_plugin@,yes)
786

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

800
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
801

802 803
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
804

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

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

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

814 815 816 817
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
818

819
include .depend.coq-plugin
820

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

824
depend: .depend.coq-plugin
825 826 827 828 829 830

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

endif

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

ifeq (@enable_coq_libs@,yes)

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

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

847 848 849 850 851
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
852 853

COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
854 855 856 857 858 859 860

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

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

861 862 863 864 865 866 867 868 869
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 "]" >> $@

870 871 872 873
all: $(COQVO)

install_no_local::
	mkdir -p $(LIBDIR)/why3/coq
874 875
	mkdir -p $(LIBDIR)/why3/coq/int
	cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
876
	mkdir -p $(LIBDIR)/why3/coq/real
877
	cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
878 879
ifeq (@enable_coq_fp_libs@,yes)
	mkdir -p $(LIBDIR)/why3/coq/floating_point
880
	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
881
endif
882 883 884 885 886 887 888 889 890 891 892 893 894

install_local: $(COQVO)

include .depend.coq-libs

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

depend: .depend.coq-libs

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

896 897 898 899 900
else

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

901
endif
902

903 904 905
########
# Tptp2why
########
906

907
ifeq (@enable_whytptp@,yes)
908

909 910
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
911

François Bobot's avatar
François Bobot committed
912
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
913

914
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
915 916 917 918 919 920

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

921 922
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
923 924 925

# build targets

Andrei Paskevich's avatar
Andrei Paskevich committed
926 927
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt  opt : lib/plugins/whytptp.cmxs
928

Andrei Paskevich's avatar
Andrei Paskevich committed
929 930
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
931

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

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

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

943 944 945 946 947 948 949 950 951 952 953
# 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)
954
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
955
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts