Makefile.in 72.1 KB
Newer Older
1 2 3
####################################################################
#                                                                  #
#  The Why3 Verification Platform   /   The Why3 Development Team  #
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
#  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  #
5 6 7 8 9 10
#                                                                  #
#  This software is distributed under the terms of the GNU Lesser  #
#  General Public License version 2.1, with the special exception  #
#  on linking described in file LICENSE.                           #
#                                                                  #
####################################################################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11

12 13 14
VERBOSEMAKE ?= @enable_verbose_make@

ifeq ($(VERBOSEMAKE),yes)
15 16
  SHOW = @true
  HIDE =
17
else
18 19
  SHOW = @echo
  HIDE = @
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
20 21
endif

22
# install the binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23
DESTDIR =
24

25
prefix	    = @prefix@
26 27 28 29 30
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
31
DATADIR = $(DESTDIR)@datarootdir@
32
MANDIR  = $(DESTDIR)@mandir@
33
TOOLDIR = $(LIBDIR)/why3/commands
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
34

Andrei Paskevich's avatar
Andrei Paskevich committed
35
# OS specific stuff
36
EXE   = @EXE@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
37 38

# other variables
39
CC        = @CC@
40 41 42
MKDIR_P   = @MKDIR_P@
INSTALL   = @INSTALL@
INSTALL_DATA = @INSTALL_DATA@
43 44 45 46 47 48 49
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
50
OCAMLINSTALLLIB  = $(DESTDIR)@OCAMLINSTALLLIB@
51 52
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
53 54
COQC      = @COQC@
COQDEP    = @COQDEP@
55 56
COQCAMLP  = @COQCAMLP@
COQCAMLPLIB = @COQCAMLPLIB@
MARCHE Claude's avatar
MARCHE Claude committed
57
FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
58

59 60 61 62 63 64
ifeq (@enable_menhirLib@,yes)
MENHIR	  = @MENHIR@ --table
else
MENHIR	  = @MENHIR@
endif

65
DEPFLAGS  = -slash -I lib/why3
66
ifeq (@OCAMLBEST@,opt)
67 68
# the semantics of the -native flag changed in ocaml 4.03.0
#DEPFLAGS += -native
69 70
endif

71
RUBBER = @RUBBER@
72
HEVEA = @HEVEA@
73
HACHA = @HACHA@
74
EMACS = @EMACS@
75

76
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
77
#PDFVIEWER = @PDFVIEWER@
78

79
INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
80 81 82 83 84 85 86 87 88 89

# warnings are enabled and non fatal by default, except:
# - disabled:
#   4    Fragile pattern matching: matching that will remain complete even
#        if additional constructors are added to one of the variant types
#        matched.
#   9    Missing fields in a record pattern.
#   41   Ambiguous constructor or label name.
#   44   Open statement shadows an already defined identifier.
#   45   Open statement shadows an already defined label or constructor.
90
#   50   Unexpected documentation comment.
91 92 93
#   52   The argument of this constructor should not be matched against a
#        constant pattern; the actual value of the argument could change
#        in the future.
94 95 96 97 98
# - fatal:
#   5    Partially applied function: expression whose result has function
#        type and is ignored.
#   48   Implicit elimination of optional arguments.

99
WARNINGS = A-4-9-41-44-45-50-52@5@48
100

101 102
OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
103 104 105

OLINKFLAGS = -linkall $(EXTCMXA)
BLINKFLAGS = -linkall $(EXTCMA)
106

107
ifeq (@enable_profiling@,yes)
108 109 110
OFLAGS += -g -p
endif

111 112 113
# see http://caml.inria.fr/mantis/view.php?id=4991
CMIHACK = -intf-suffix .cmi

114 115
# external libraries common to all binaries

116
EXTOBJS = @MENHIRLIB@
117
EXTLIBS = str unix nums dynlink @ZIPLIB@
118 119 120

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
121

122
INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
123
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
124

125 126
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})

127 128
# Variables added for checking realizations
GENERATED_PREFIX_COQ="lib/coq"
129
GENERATED_PREFIX_ISABELLE=lib/isabelle
130

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
131 132 133
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134

135 136 137 138
all: @OCAMLBEST@
plugins: plugins.@OCAMLBEST@
opt: plugins.opt
byte: plugins.byte
Francois Bobot's avatar
Francois Bobot committed
139

140 141 142 143 144
ifeq (@enable_local@,yes)
all: install_local
endif

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

147 148 149 150
CLEANDIRS =
CLEANLIBS =
GENERATED =

151 152 153
##############
# Why3 library
##############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
154

155
LIBGENERATED = src/util/config.ml \
156 157 158 159
	       src/util/rc.ml src/util/lexlib.ml \
	       src/util/json_parser.mli src/util/json_parser.ml \
	       src/util/json_lexer.ml \
	       src/parser/lexer.ml \
160 161
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
162
	       src/driver/driver_lexer.ml \
163 164
	       src/driver/parse_smtv2_model_parser.mli src/driver/parse_smtv2_model_parser.ml \
	       src/driver/parse_smtv2_model_lexer.ml \
165
	       src/session/compress.ml src/session/xml.ml \
166
	       src/session/strategy_parser.ml \
167
	       lib/ocaml/why3__BigInt_compat.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
168

169
LIB_UTIL = config bigInt util opt lists strings \
170
	   pp extmap extset exthtbl weakhtbl \
171
	   hashcons stdlib exn_printer \
172
	   json_base json_parser json_lexer \
173
	   debug loc lexlib print_tree \
174
	   cmdline warning sysutil rc plugin bigInt number pqueue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175

176
LIB_CORE = ident ty term pattern decl coercion theory \
177
	   task pretty_sig pretty dterm env trans printer model_parser
178

179
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
180 181 182 183
		whyconf autodetection \
		smt2_model_defs parse_smtv2_model_parser \
		collect_data_model parse_smtv2_model_lexer parse_smtv2_model \
		parse_smtv2_model
184

185
LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr \
186
          pinterp mltree compile pdriver cprinter ocaml_printer
187

188
LIB_PARSER = ptree glob typing parser lexer
189

190
LIB_TRANSFORM = simplify_formula inlining split_goal \
191
		args_wrapper detect_polymorphism reduction_engine compute \
192
		eliminate_definition eliminate_algebraic \
193
		eliminate_inductive eliminate_let eliminate_if \
194 195 196 197
		libencoding discriminate encoding encoding_select \
		encoding_guards_full encoding_tags_full \
		encoding_guards encoding_tags encoding_twin \
		encoding_sort simplify_array filter_trigger \
198
		introduction abstraction close_epsilon lift_epsilon \
199
		eliminate_epsilon intro_projections_counterexmp \
200
		intro_vc_vars_counterexmp prepare_for_counterexmp \
Andrei Paskevich's avatar
Andrei Paskevich committed
201
		instantiate_predicate smoke_detector \
Guillaume Melquiond's avatar
Guillaume Melquiond committed
202
		prop_curry eliminate_literal \
203
		generic_arg_trans_utils case apply \
204
		ind_itp destruct cut \
205
		induction induction_pr matching reification
206

Sylvain Dailler's avatar
Sylvain Dailler committed
207
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
208
	      pvs isabelle \
209
	      simplify gappa cvc3 yices mathematica
210

211 212 213
LIB_SESSION = compress xml termcode session_itp \
              strategy strategy_parser controller_itp \
	      server_utils itp_communication \
214
	      itp_server json_util
215

216
LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
217 218
	      $(addprefix src/core/, $(LIB_CORE)) \
	      $(addprefix src/driver/, $(LIB_DRIVER)) \
219
	      $(addprefix src/mlw/, $(LIB_MLW)) \
220
	      $(addprefix src/parser/, $(LIB_PARSER)) \
221
	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
François Bobot's avatar
François Bobot committed
222
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
223
	      $(addprefix src/session/, $(LIB_SESSION))
224

225
LIBDIRS = util core driver mlw parser transform printer session
226
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
227

Andrei Paskevich's avatar
Andrei Paskevich committed
228
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
229 230
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
231

Andrei Paskevich's avatar
Andrei Paskevich committed
232
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
233
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
234
$(LIBCMX): OFLAGS += -for-pack Why3
235

236 237
$(LIBDEP): $(LIBGENERATED)

238 239 240
# Zarith

ifeq (@enable_zarith@,yes)
241
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
242
	cp lib/ocaml/why3__BigInt_zarith.ml $@
243
else
244
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
245
	cp lib/ocaml/why3__BigInt_num.ml $@
246 247
endif

248 249 250 251 252 253 254 255 256 257
# Ocamlzip

ifeq (@enable_zip@,yes)
src/session/compress.ml: config.status src/session/compress_z.ml
	cp src/session/compress_z.ml $@
else
src/session/compress.ml: config.status src/session/compress_none.ml
	cp src/session/compress_none.ml $@
endif

258 259
# hide deprecated warnings for strings

260 261
src/util/strings.cmo: WARNINGS:=$(WARNINGS)-3
src/util/strings.cmx: WARNINGS:=$(WARNINGS)-3
262

263 264
# hide warning 'no cmx file was found in path for module ..., and its interface was not compiled with -opaque' for the coq tactic

265
src/coq-tactic/why3tac.cmx: WARNINGS:=$(WARNINGS)-58
266

267
# build targets
268

269
byte: lib/why3/why3.cma
270
opt:  lib/why3/why3.cmxa lib/why3/why3.cmxs
271

272 273
lib/why3/why3.cma: lib/why3/why3.cmo
lib/why3/why3.cmxa: lib/why3/why3.cmx
274
lib/why3/why3.cmxs: lib/why3/why3.cmx
275

276
lib/why3/why3.cmo: $(LIBCMO)
277 278
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
279

280
lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
281
	$(SHOW) 'Linking  $@'
282
	$(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
283

Andrei Paskevich's avatar
Andrei Paskevich committed
284
# clean and depend
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
285

286
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
287
-include $(LIBDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
288
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
289

290
depend: $(LIBDEP)
291

292 293 294
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
CLEANLIBS += lib/why3/why3session lib/why3/why3
GENERATED += $(LIBGENERATED)
295

296 297 298
###############
# installation
###############
299

Kate's avatar
Kate committed
300 301
clean_old_install::
	rm -rf $(LIBDIR)/why3
MARCHE Claude's avatar
MARCHE Claude committed
302 303
	rm -rf $(DATADIR)/why3

304 305
clean_old_install-lib::
	if test -d $(OCAMLINSTALLLIB) -a -w $(OCAMLINSTALLLIB); then \
Guillaume Melquiond's avatar
Guillaume Melquiond committed
306
	  rm -rf $(OCAMLINSTALLLIB)/why3; \
307
	fi
308

309
install_no_local::
310 311 312 313 314 315
	$(MKDIR_P) $(BINDIR)
	$(MKDIR_P) $(LIBDIR)/why3
	$(MKDIR_P) $(TOOLDIR)
	$(MKDIR_P) $(DATADIR)/why3
	$(MKDIR_P) $(DATADIR)/why3/images
	$(MKDIR_P) $(DATADIR)/why3/vim
316 317
	$(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
	$(MKDIR_P) $(DATADIR)/why3/vim/syntax
318
	$(MKDIR_P) $(DATADIR)/why3/lang
319 320
	$(MKDIR_P) $(DATADIR)/why3/stdlib
	$(MKDIR_P) $(DATADIR)/why3/stdlib/mach
321
	$(MKDIR_P) $(DATADIR)/why3/drivers
322 323
	$(INSTALL_DATA) stdlib/*.why stdlib/*.mlw $(DATADIR)/why3/stdlib
	$(INSTALL_DATA) stdlib/mach/*.mlw $(DATADIR)/why3/stdlib/mach
324 325 326
	$(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
	$(INSTALL_DATA) LICENSE $(DATADIR)/why3/
	$(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
327 328
	for i in share/images/*.rc; do \
	     d=`basename $$i .rc`; \
329 330 331
	     $(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
	     $(MKDIR_P) $(DATADIR)/why3/images/$$d; \
	     $(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
332
	done
333 334 335
	$(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
	$(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3
	$(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3
336 337
	$(INSTALL_DATA) share/vim/ftdetect/why3.vim $(DATADIR)/why3/vim/ftdetect/why3.vim
	$(INSTALL_DATA) share/vim/syntax/why3.vim $(DATADIR)/why3/vim/syntax/why3.vim
338
	$(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
339

MARCHE Claude's avatar
MARCHE Claude committed
340
install_no_local_lib::
341 342
	$(MKDIR_P) $(OCAMLINSTALLLIB)/why3
	$(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \
343
		lib/why3/META $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
344

345 346
ifeq (@enable_local@,yes)
install install-lib:
347 348
	@echo "Why3 is configured in local installation mode."
	@echo "To install Why3, run ./configure --disable-local ; make ; make install"
349
else
MARCHE Claude's avatar
MARCHE Claude committed
350
install: clean_old_install install_no_local
351
install-lib: clean_old_install-lib install_no_local_lib
352 353
endif

MARCHE Claude's avatar
MARCHE Claude committed
354 355
install-all: install install-lib

Kate's avatar
Kate committed
356 357 358 359
##################
# Uninstallation
##################

360 361 362 363 364 365
ifeq (@enable_local@,yes)
uninstall:
	@echo "Why3 is configured in local installation mode."
else
uninstall: clean_old_install clean_old_install-lib
endif
Kate's avatar
Kate committed
366

367 368 369 370 371 372 373
##################
# Why3 emacs mode
##################

%.elc: %.el
	$(EMACS) --batch --no-init-file -f batch-byte-compile $<

Kate's avatar
Kate committed
374 375 376 377 378
clean_old_install::
	rm -f $(DATADIR)/emacs/site-lisp/why3.el
	rm -f $(DATADIR)/emacs/site-lisp/why3.elc

install_no_local::
379
	$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
380
	$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
381
ifeq (@enable_emacs_compilation@,yes)
382
	$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
Kate's avatar
Kate committed
383 384
endif

385
ifeq (@enable_emacs_compilation@,yes)
386
all: share/emacs/why3.elc
387 388
endif

Kate's avatar
Kate committed
389

390
##################
391
# Why3 plugins
392 393
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
394
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
395
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
396 397
		plugins/python/py_lexer.ml \
		plugins/python/py_parser.ml plugins/python/py_parser.mli \
398
		plugins/parser/dimacs.ml \
399

400
PLUG_PARSER = genequlin dimacs
401
PLUG_PRINTER =
402
PLUG_TRANSFORM =
403
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
404
PLUG_PYTHON = py_ast py_parser py_lexer py_main
405

406
PLUGINS = genequlin dimacs tptp python
407

408
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
409
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
Andrei Paskevich's avatar
Andrei Paskevich committed
410

411 412
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
413

414 415 416
PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))

417 418 419 420 421 422 423 424 425 426
ifeq (@enable_hypothesis_selection@,yes)
PLUG_TRANSFORM += hypothesis_selection
PLUGINS += hypothesis_selection

lib/plugins/hypothesis_selection.cmxs: INCLUDES += -I @OCAMLGRAPHLIB@
lib/plugins/hypothesis_selection.cmo:  INCLUDES += -I @OCAMLGRAPHLIB@
lib/plugins/hypothesis_selection.cmxs: OFLAGS += graph.cmxa
lib/plugins/hypothesis_selection.cmo:  BFLAGS += graph.cmo
endif

427 428
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
429
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
430
	      $(TPTPMODULES) $(PYTHONMODULES)
431

Andrei Paskevich's avatar
Andrei Paskevich committed
432
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
433 434 435
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

436
PLUGDIRS = parser printer transform tptp python
437 438
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
439
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
440 441
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

442 443
$(PLUGDEP): $(PLUGGENERATED)

444 445 446 447 448
LIBPLUGCMO =  $(addsuffix .cmo,  $(addprefix lib/plugins/, $(PLUGINS)))
LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
449

450 451
lib/plugins:
	mkdir lib/plugins
452

453
lib/plugins/%.cmxs: | lib/plugins
454
	$(SHOW) 'Linking  $@'
455
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
456

457
lib/plugins/%.cmo: | lib/plugins
458
	$(SHOW) 'Linking  $@'
459
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
460

461 462
lib/plugins/%.cmxs: plugins/parser/%.cmx
lib/plugins/%.cmo: plugins/parser/%.cmo
463 464 465 466
lib/plugins/%.cmxs: plugins/printer/%.cmx
lib/plugins/%.cmo: plugins/printer/%.cmo
lib/plugins/%.cmxs: plugins/transform/%.cmx
lib/plugins/%.cmo: plugins/transform/%.cmo
467 468
lib/plugins/tptp.cmxs: $(TPTPCMX)
lib/plugins/tptp.cmo: $(TPTPCMO)
469 470
lib/plugins/python.cmxs: $(PYTHONCMX)
lib/plugins/python.cmo: $(PYTHONCMO)
471

Andrei Paskevich's avatar
Andrei Paskevich committed
472 473
# depend and clean targets

474
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
475
-include $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
476 477
endif

478
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
479

480 481
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
GENERATED += $(PLUGGENERATED)
482 483

install_no_local::
484 485
	$(MKDIR_P) $(LIBDIR)/why3/plugins
	$(INSTALL_DATA) $(wildcard $(LIBPLUGCMO) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins
486

487 488 489 490
###############
# Why3 commands
###############

491 492
TOOLSGENERATED = src/tools/why3wc.ml

493
TOOLS_BIN = why3config why3execute why3extract why3prove \
494 495
	    why3realize why3replay why3wc

Andrei Paskevich's avatar
Andrei Paskevich committed
496
TOOLS_FILES = main $(TOOLS_BIN)
497 498 499 500 501 502 503 504 505 506

TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))

TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES))
TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES))
TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))

$(TOOLSDEP): DEPFLAGS += -I src/tools
$(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools

507 508
$(TOOLSDEP): $(TOOLSGENERATED)

509 510 511
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt:  bin/why3.opt  $(TOOLS_BIN:%=bin/%.opt)

512 513 514
bin:
	mkdir bin

Andrei Paskevich's avatar
Andrei Paskevich committed
515 516
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
517 518
bin/why3config.opt: lib/why3/why3.cmxa src/tools/why3config.cmx
bin/why3config.byte: lib/why3/why3.cma src/tools/why3config.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
519 520 521 522 523 524 525 526
bin/why3execute.opt: lib/why3/why3.cmxa src/tools/why3execute.cmx
bin/why3execute.byte: lib/why3/why3.cma src/tools/why3execute.cmo
bin/why3extract.opt: lib/why3/why3.cmxa src/tools/why3extract.cmx
bin/why3extract.byte: lib/why3/why3.cma src/tools/why3extract.cmo
bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx
bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo
bin/why3realize.opt: lib/why3/why3.cmxa src/tools/why3realize.cmx
bin/why3realize.byte: lib/why3/why3.cma src/tools/why3realize.cmo
527 528
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/unix_scheduler.cmx src/tools/why3replay.cmx
bin/why3replay.byte: lib/why3/why3.cma src/tools/unix_scheduler.cmo src/tools/why3replay.cmo
529 530 531
bin/why3wc.opt: src/tools/why3wc.cmx
bin/why3wc.byte: src/tools/why3wc.cmo

Kate's avatar
Kate committed
532
clean_old_install::
533
	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
534
	rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
Kate's avatar
Kate committed
535

536
install_no_local::
537 538 539 540 541 542 543 544
	$(INSTALL) bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
	$(INSTALL) bin/why3config.@OCAMLBEST@  $(TOOLDIR)/why3config$(EXE)
	$(INSTALL) bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE)
	$(INSTALL) bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE)
	$(INSTALL) bin/why3prove.@OCAMLBEST@   $(TOOLDIR)/why3prove$(EXE)
	$(INSTALL) bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
	$(INSTALL) bin/why3replay.@OCAMLBEST@  $(TOOLDIR)/why3replay$(EXE)
	$(INSTALL) bin/why3wc.@OCAMLBEST@      $(TOOLDIR)/why3wc$(EXE)
545 546

install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
547

548
bin/%:	bin/%.@OCAMLBEST@
549
	ln -sf $(notdir $<) $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
550

551
install_local:: share/drivers share/stdlib
552 553 554 555

share/drivers:
	ln -snf ../drivers share/drivers

556 557
share/stdlib:
	ln -snf ../stdlib share/stdlib
558

559
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
560
-include $(TOOLSDEP)
561 562
endif

563
depend: $(TOOLSDEP)
564

565 566 567
CLEANDIRS += src/tools
GENERATED += $(TOOLSGENERATED)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
568
clean::
569
	rm -f bin/why3*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
570

571 572 573
##############
# test targets
##############
574

575 576
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
577

578 579
%: %.mlw bin/why3.opt
	bin/why3.opt $*.mlw
580

581 582
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
583

584 585
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
586

587
%.type: %.mlw bin/why3ide.opt
588
	bin/why3.opt --type-only $*.mlw
589

590 591 592 593
##############
# Why3server #
##############

594 595 596 597 598 599 600 601
SERVER_MODULES := logging arraylist options queue readbuf request \
		  writebuf server-unix server-win

CPULIM_MODULES := cpulimit-unix cpulimit-win

SERVER_O := $(addprefix src/server/, $(addsuffix .o, $(SERVER_MODULES)))

CPULIM_O := $(addprefix src/server/, $(addsuffix .o, $(CPULIM_MODULES)))
602

603 604
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)

605
all: $(TOOLS)
606

607
lib/why3server$(EXE): $(SERVER_O)
608 609 610 611
	$(CC) -Wall -o $@ $^

lib/why3cpulimit$(EXE): $(CPULIM_O)
	$(CC) -Wall -o $@ $^
612

613
%.o: %.c
614
	$(CC) -Wall -O -g -o $@ -c $<
615 616

install_no_local::
617 618 619 620
	$(MKDIR_P) $(LIBDIR)/why3
	$(INSTALL) lib/why3server$(EXE) $(LIBDIR)/why3/why3server$(EXE)
	$(INSTALL) lib/why3cpulimit$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
	$(INSTALL) lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
621 622

clean::
623
	rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
624

625 626 627 628
##########
# gallery
##########

629
# we export exactly the programs that have a why3session.xml file
630 631 632

.PHONY: gallery

633 634 635 636 637
gallery:: gallery-simple gallery-subs

.PHONY: gallery-simple

gallery-simple::
638
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
Andrei Paskevich's avatar
Andrei Paskevich committed
639
	@for x in examples/*/why3session.xml ; do \
640 641
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
642 643
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
644 645
	  WHY3CONFIG="" bin/why3session.@OCAMLBEST@ html $$x -o $(GALLERYDIR)/$$f; \
	  cp examples/$$f.mlw $(GALLERYDIR)/$$f/; \
Andrei Paskevich's avatar
Andrei Paskevich committed
646
	  cd examples/; \
647
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
648
	  zip -q -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
649
	  cd ..; \
650
	done
651

652 653
.PHONY: gallery-subs

654
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover
655 656

gallery-subs::
657
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
658 659
	@for d in $(GALLERYSUBS) ; do \
	  echo "exporting examples/$$d"; \
660
	  mkdir -p $(GALLERYDIR)/$$d; \
661
	  cd examples/$$d; \
662
	  WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
663
	  cd ..; \
664
	  rm -f $(GALLERYDIR)/$$d/$$d.zip; \
665
	  zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
666 667 668 669
	  cd ..; \
	done


670 671 672 673 674 675
%-gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	x=$*/why3session.xml; \
	d=`dirname $$x`; \
	f=`basename $$d`; \
	echo "exporting $$f"; \
676
	rm -f $$d/*.bak; \
677
	mkdir -p $(GALLERYDIR)/$$f; \
678
	WHY3CONFIG="" bin/why3session.@OCAMLBEST@ html $$d -o $(GALLERYDIR)/$$f; \
679 680
	if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
	if test -f examples/$$f.why; then cp examples/$$f.why $(GALLERYDIR)/$$f/; fi; \
681
	cd examples/; \
682
	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
683
	zip -q -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
684

MARCHE Claude's avatar
MARCHE Claude committed
685 686 687 688 689 690 691 692
########
# XML DTD validation
########

.PHONY: xml-validate

xml-validate:
	@for x in `find examples/ -name why3session.xml`; do \
MARCHE Claude's avatar
MARCHE Claude committed
693
	  xmllint --noout --valid $$x 2>&1 | head -1; \
MARCHE Claude's avatar
MARCHE Claude committed
694 695
	done

696 697 698 699 700
xml-validate-local:
	@for x in `find examples/ -name why3session.xml`; do \
	  xmllint --noout --dtdvalid share/why3session.dtd $$x 2>&1 | head -1; \
	done

MARCHE Claude's avatar
MARCHE Claude committed
701 702 703 704
###############
# IDE
###############

705 706
ifeq (@enable_ide@,yes)

Sylvain Dailler's avatar
Sylvain Dailler committed
707
IDE_FILES = gconfig ide_utils why3ide
MARCHE Claude's avatar
MARCHE Claude committed
708 709 710

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

Andrei Paskevich's avatar
Andrei Paskevich committed
711
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
712 713 714
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
715
$(IDEDEP): DEPFLAGS += -I src/ide
716
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
717

718
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
719

720 721
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
722

723
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
724
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
725
bin/why3ide.byte: BLINKFLAGS += -custom
MARCHE Claude's avatar
MARCHE Claude committed
726

727 728
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
729

730
src/ide/resetgc.o: src/ide/resetgc.c
731 732
	$(SHOW) 'Ocamlc   $<'
	$(HIDE)$(OCAMLC) -c -ccopt "-Wall -o $@" $<
733

MARCHE Claude's avatar
MARCHE Claude committed
734 735
# depend and clean targets

736
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
737
-include $(IDEDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
738
endif
MARCHE Claude's avatar
MARCHE Claude committed
739

Andrei Paskevich's avatar
Andrei Paskevich committed
740
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
741

742
CLEANDIRS += src/ide
MARCHE Claude's avatar
MARCHE Claude committed
743

Kate's avatar
Kate committed
744 745 746
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

747
install_no_local::
748
	$(INSTALL) bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
749

750
install_local:: bin/why3ide
751

752
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
753

754

755 756 757 758
###############
# WEBSERV
###############

759
WEBSERV_FILES = wserver why3web
760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801

WEBSERVMODULES = $(addprefix src/ide/, $(WEBSERV_FILES))

WEBSERVDEP = $(addsuffix .dep, $(WEBSERVMODULES))
WEBSERVCMO = $(addsuffix .cmo, $(WEBSERVMODULES))
WEBSERVCMX = $(addsuffix .cmx, $(WEBSERVMODULES))

$(WEBSERVDEP): DEPFLAGS += -I src/ide
$(WEBSERVCMO) $(WEBSERVCMX): INCLUDES += -I src/ide

# build targets

byte: bin/why3webserver.byte
opt:  bin/why3webserver.opt

bin/why3webserver.opt: lib/why3/why3.cmxa $(WEBSERVCMX)
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

bin/why3webserver.byte: lib/why3/why3.cma $(WEBSERVCMO)
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^

# depend and clean targets

ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WEBSERVDEP)
endif

depend: $(WEBSERVDEP)

CLEANDIRS += src/ide

clean_old_install::
	rm -f $(BINDIR)/why3webserver$(EXE)

install_no_local::
	$(INSTALL) bin/why3webserver.@OCAMLBEST@ $(TOOLDIR)/why3webserver$(EXE)

install_local:: bin/why3webserver


802 803 804 805
###############
# Session
###############

806
SESSION_FILES = why3session_lib why3session_info \
807
		why3session_html why3session_latex \
808
		why3session_main
809
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
810
#       why3session_output
811 812 813

SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))

Andrei Paskevich's avatar
Andrei Paskevich committed
814
SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
815 816 817
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
818
$(SESSIONDEP): DEPFLAGS += -I src/why3session
819 820 821 822 823 824 825
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

byte: bin/why3session.byte
opt:  bin/why3session.opt

826 827
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
828 829 830

# depend and clean targets

831
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
832
-include $(SESSIONDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
833
endif
834

Andrei Paskevich's avatar
Andrei Paskevich committed
835
depend: $(SESSIONDEP)
836

837
CLEANDIRS += src/why3session
838

Kate's avatar
Kate committed
839 840 841
clean_old_install::
	rm -f $(BINDIR)/why3session$(EXE)

842
install_no_local::
843
	$(INSTALL) bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
844

845
install_local:: bin/why3session
846

MARCHE Claude's avatar
MARCHE Claude committed
847 848 849 850
###############
# Why3 Shell
###############

Sylvain Dailler's avatar
Sylvain Dailler committed
851
SHELL_FILES = unix_scheduler why3shell
MARCHE Claude's avatar
MARCHE Claude committed
852

853
SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
MARCHE Claude's avatar
MARCHE Claude committed
854 855 856 857 858

SHELLDEP = $(addsuffix .dep, $(SHELLMODULES))
SHELLCMO = $(addsuffix .cmo, $(SHELLMODULES))
SHELLCMX = $(addsuffix .cmx, $(SHELLMODULES))

859 860
$(SHELLDEP): DEPFLAGS += -I src/tools
$(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
MARCHE Claude's avatar
MARCHE Claude committed
861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890

# build targets

byte: bin/why3shell.byte
opt:  bin/why3shell.opt

bin/why3shell.opt: lib/why3/why3.cmxa $(SHELLCMX)
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

bin/why3shell.byte: lib/why3/why3.cma $(SHELLCMO)
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

# depend and clean targets

ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(SHELLDEP)
endif

depend: $(SHELLDEP)

clean_old_install::
	rm -f $(BINDIR)/why3shell$(EXE)

install_no_local::
	$(INSTALL) bin/why3shell.@OCAMLBEST@ $(TOOLDIR)/why3shell$(EXE)

install_local:: bin/why3shell

MARCHE Claude's avatar
MARCHE Claude committed
891

892 893 894
##############
# Coq plugin
##############
895

896
ifeq (@enable_coq_tactic@,yes)
897

898
COQPGENERATED = src/coq-tactic/why3tac.ml
899

900
COQP_FILES = why3tac
901

902
COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
903

904 905 906
COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
907

Guillaume Melquiond's avatar
Guillaume Melquiond committed
908
COQPTREES = engine interp intf kernel lib library ltac parsing pretyping printing proofs tactics toplevel vernac plugins/ltac
909
COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
910

911
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
912
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
913 914
$(COQPCMO) $(COQPCMX): BFLAGS += -rectypes
$(COQPCMX): OFLAGS += -rectypes
915

916
$(COQPDEP): $(COQPGENERATED)
917

918 919
byte: lib/coq-tactic/why3tac.cma
opt:  lib/coq-tactic/why3tac.cmxs
920

921 922 923 924
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@)
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmx,  @MENHIRLIB@)

lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cma,  @ZIPLIB@)
925
lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cmo,  @MENHIRLIB@)
926

927 928
lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
929

930
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
931 932
	$(SHOW) 'Camlp    $<'
	$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
933

934
COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3 -I lib/coq-tactic
935

936 937 938 939 940
ifeq "$(OCAMLBEST)" "opt"
COQTACEXT = cmxs
else
COQTACEXT = cma
COQRTAC += -byte
Guillaume Melquiond's avatar
Guillaume Melquiond committed
941
endif
942

943
lib/coq-tactic/Why3.vo: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.$(COQTACEXT)
944
	$(SHOW) 'Coqc     $<'
945
	$(HIDE)WHY3CONFIG="" $(COQC) $(COQRTAC) $<
946

947
all: lib/coq-tactic/Why3.vo
948

949
# depend and clean targets
Andrei Paskevich's avatar
Andrei Paskevich committed
950

951
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
952
-include $(COQPDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
953
endif
954

955
depend: $(COQPDEP)
956

Andrei Paskevich's avatar