Makefile.in 72.9 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
####################################################################
#                                                                  #
#  The Why3 Verification Platform   /   The Why3 Development Team  #
MARCHE Claude's avatar
MARCHE Claude committed
4
#  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  #
Andrei Paskevich's avatar
Andrei Paskevich committed
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) -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -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 114 115
ifeq (@enable_bin_annot@,yes)
OFLAGS += -bin-annot
BFLAGS += -bin-annot
endif

116 117 118
# see http://caml.inria.fr/mantis/view.php?id=4991
CMIHACK = -intf-suffix .cmi

119 120
# external libraries common to all binaries

121
EXTOBJS = @MENHIRLIB@
122
EXTLIBS = str unix nums dynlink @ZIPLIB@
123 124 125

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
126

Andrei Paskevich's avatar
Andrei Paskevich committed
127
INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
128
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
Andrei Paskevich's avatar
Andrei Paskevich committed
129

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
148 149 150 151
CLEANDIRS =
CLEANLIBS =
GENERATED =

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

156
LIBGENERATED = src/util/config.ml \
157 158 159 160
	       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 \
161 162
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
163
	       src/driver/driver_lexer.ml \
164 165
	       src/driver/parse_smtv2_model_parser.mli src/driver/parse_smtv2_model_parser.ml \
	       src/driver/parse_smtv2_model_lexer.ml \
166
	       src/session/compress.ml src/session/xml.ml \
167
	       src/session/strategy_parser.ml \
168
	       lib/ocaml/why3__BigInt_compat.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169

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

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

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

186
LIB_MLW = ity expr dexpr pdecl pmodule
187

188 189
LIB_PARSER = ptree glob parser typing lexer

190
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
Clément Fumex's avatar
Clément Fumex committed
191
		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 \
MARCHE Claude's avatar
MARCHE Claude committed
201
		eval_match instantiate_predicate smoke_detector \
202
		induction_pr prop_curry \
MARCHE Claude's avatar
MARCHE Claude committed
203 204
		args_wrapper case \
		eliminate_literal
205

206 207
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 smtv2_cvc_ce coq\
	      pvs isabelle \
208
	      simplify gappa cvc3 yices mathematica
209

210
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
211
	    mlw_dexpr mlw_typing mlw_driver mlw_exec mlw_ocaml \
212
	    mlw_main mlw_interp
213

214 215 216
LIB_SESSION = compress xml termcode session_itp \
              strategy strategy_parser controller_itp \
	      server_utils itp_communication \
217
	      itp_server json_util
218

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

229
LIBDIRS = util core driver mlw parser transform printer whyml session
230
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
231

Andrei Paskevich's avatar
Andrei Paskevich committed
232
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
233 234
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
235

Andrei Paskevich's avatar
Andrei Paskevich committed
236
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
237
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
238
$(LIBCMX): OFLAGS += -for-pack Why3
239

240 241
$(LIBDEP): $(LIBGENERATED)

242 243 244
# Zarith

ifeq (@enable_zarith@,yes)
245
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
246
	cp lib/ocaml/why3__BigInt_zarith.ml $@
247
else
248
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
249
	cp lib/ocaml/why3__BigInt_num.ml $@
250 251
endif

252 253 254 255 256 257 258 259 260 261
# 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

262 263 264 265 266
# hide deprecated warnings for strings

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

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

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

271
# build targets
272

273 274
byte: lib/why3/why3.cma
opt:  lib/why3/why3.cmxa
275

276 277
lib/why3/why3.cma: lib/why3/why3.cmo
lib/why3/why3.cmxa: lib/why3/why3.cmx
278

279
lib/why3/why3.cmo: $(LIBCMO)
280 281
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
282

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

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

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

293
depend: $(LIBDEP)
294

Andrei Paskevich's avatar
Andrei Paskevich committed
295 296 297
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
CLEANLIBS += lib/why3/why3session lib/why3/why3
GENERATED += $(LIBGENERATED)
298

299 300 301
###############
# installation
###############
302

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
303 304
clean_old_install::
	rm -rf $(LIBDIR)/why3
MARCHE Claude's avatar
MARCHE Claude committed
305
	rm -rf $(DATADIR)/why3
306
	rm -rf $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
307

308 309

install_no_local:: clean_old_install
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 319 320 321 322 323 324 325 326 327
	$(MKDIR_P) $(DATADIR)/why3/lang
	$(MKDIR_P) $(DATADIR)/why3/theories
	$(MKDIR_P) $(DATADIR)/why3/modules/mach
	$(MKDIR_P) $(DATADIR)/why3/drivers
	$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories
	$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules
	$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
	$(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
	$(INSTALL_DATA) LICENSE $(DATADIR)/why3/
	$(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
328 329
	for i in share/images/*.rc; do \
	     d=`basename $$i .rc`; \
330 331 332
	     $(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
	     $(MKDIR_P) $(DATADIR)/why3/images/$$d; \
	     $(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
333
	done
334 335 336
	$(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
	$(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3
	$(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3
337 338
	$(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
339
	$(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
340

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

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

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
357 358 359 360 361 362
##################
# Uninstallation
##################

uninstall: clean_old_install

363 364 365 366 367 368 369
##################
# Why3 emacs mode
##################

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
370 371 372 373 374
clean_old_install::
	rm -f $(DATADIR)/emacs/site-lisp/why3.el
	rm -f $(DATADIR)/emacs/site-lisp/why3.elc

install_no_local::
375
	$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
376
	$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
377
ifeq (@enable_emacs_compilation@,yes)
378
	$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
379 380
endif

381
ifeq (@enable_emacs_compilation@,yes)
382
all: share/emacs/why3.elc
383 384
endif

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
385

386
##################
387
# Why3 plugins
388 389
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
390
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
391
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
392 393
		plugins/python/py_lexer.ml \
		plugins/python/py_parser.ml plugins/python/py_parser.mli \
394
		plugins/parser/dimacs.ml \
395

396
PLUG_PARSER = genequlin dimacs
397
PLUG_PRINTER =
398
PLUG_TRANSFORM =
399
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
400
PLUG_PYTHON = py_ast py_parser py_lexer py_main
401

402
PLUGINS = genequlin dimacs tptp python
403

Andrei Paskevich's avatar
Andrei Paskevich committed
404
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
405
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
Andrei Paskevich's avatar
Andrei Paskevich committed
406

Andrei Paskevich's avatar
Andrei Paskevich committed
407 408
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
409

410 411 412
PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))

413 414 415 416 417 418 419 420 421 422
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

423 424
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
425
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
426
	      $(TPTPMODULES) $(PYTHONMODULES)
427

Andrei Paskevich's avatar
Andrei Paskevich committed
428
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
429 430 431
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

432
PLUGDIRS = parser printer transform tptp python
433 434
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
435
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
436 437
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

438 439
$(PLUGDEP): $(PLUGGENERATED)

440 441 442 443 444
LIBPLUGCMO =  $(addsuffix .cmo,  $(addprefix lib/plugins/, $(PLUGINS)))
LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
445 446

lib/plugins/%.cmxs: plugins/parser/%.cmx
447 448
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
449 450

lib/plugins/%.cmo: plugins/parser/%.cmo
451 452
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
453 454

lib/plugins/%.cmxs: plugins/printer/%.cmx
455 456
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
457 458

lib/plugins/%.cmo: plugins/printer/%.cmo
459 460
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
461 462

lib/plugins/%.cmxs: plugins/transform/%.cmx
463 464
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
465 466

lib/plugins/%.cmo: plugins/transform/%.cmo
467 468
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
469

Andrei Paskevich's avatar
Andrei Paskevich committed
470
lib/plugins/tptp.cmxs: $(TPTPCMX)
471 472
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
473

Andrei Paskevich's avatar
Andrei Paskevich committed
474
lib/plugins/tptp.cmo: $(TPTPCMO)
475 476
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
477

478 479 480 481 482 483 484
lib/plugins/python.cmxs: $(PYTHONCMX)
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^

lib/plugins/python.cmo: $(PYTHONCMO)
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
485

Andrei Paskevich's avatar
Andrei Paskevich committed
486 487
# depend and clean targets

488
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
489
-include $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
490 491
endif

492
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
493

Andrei Paskevich's avatar
Andrei Paskevich committed
494 495
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
GENERATED += $(PLUGGENERATED)
496 497

install_no_local::
498 499
	$(MKDIR_P) $(LIBDIR)/why3/plugins
	$(INSTALL_DATA) $(wildcard $(LIBPLUGCMO) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins
500

501 502 503 504
###############
# Why3 commands
###############

Andrei Paskevich's avatar
Andrei Paskevich committed
505 506 507
TOOLSGENERATED = src/tools/why3wc.ml

TOOLS_BIN = why3config why3execute why3extract why3prove \
508
	    why3realize why3replay why3wc
Andrei Paskevich's avatar
Andrei Paskevich committed
509

Andrei Paskevich's avatar
Andrei Paskevich committed
510
TOOLS_FILES = main $(TOOLS_BIN)
511 512 513 514 515 516 517 518 519 520

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

Andrei Paskevich's avatar
Andrei Paskevich committed
521 522
$(TOOLSDEP): $(TOOLSGENERATED)

523 524 525
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt:  bin/why3.opt  $(TOOLS_BIN:%=bin/%.opt)

Andrei Paskevich's avatar
Andrei Paskevich committed
526 527
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
528 529
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
530 531 532 533 534 535 536 537
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
538 539
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
Andrei Paskevich's avatar
Andrei Paskevich committed
540 541 542
bin/why3wc.opt: src/tools/why3wc.cmx
bin/why3wc.byte: src/tools/why3wc.cmo

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
543
clean_old_install::
544
	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
545
	rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
546

547
install_no_local::
548 549 550 551 552 553 554 555
	$(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)
556 557

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

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

562 563 564 565 566 567 568 569 570 571 572
install_local:: share/drivers share/modules share/theories

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

share/modules:
	ln -snf ../modules share/modules

share/theories:
	ln -snf ../theories share/theories

573
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
574
-include $(TOOLSDEP)
575 576
endif

577
depend: $(TOOLSDEP)
578

Andrei Paskevich's avatar
Andrei Paskevich committed
579 580 581
CLEANDIRS += src/tools
GENERATED += $(TOOLSGENERATED)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
582
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
583
	rm -f bin/why3*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
584

585 586 587
##############
# test targets
##############
588

589 590
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
591

592 593
%: %.mlw bin/why3.opt
	bin/why3.opt $*.mlw
594

595 596
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
597

598 599
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
600

601
%.type: %.mlw bin/why3ide.opt
602
	bin/why3.opt --type-only $*.mlw
603

604 605 606 607
##############
# Why3server #
##############

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

617 618
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)

619
all: $(TOOLS)
620

621
lib/why3server$(EXE): $(SERVER_O)
622 623 624 625
	$(CC) -Wall -o $@ $^

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

627
%.o: %.c
628
	$(CC) -Wall -O -g -o $@ -c $<
629 630

install_no_local::
631 632 633 634
	$(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
635 636

clean::
637
	rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
638

639 640 641 642
##########
# gallery
##########

643
# we export exactly the programs that have a why3session.xml file
644 645 646

.PHONY: gallery

647 648 649 650 651
gallery:: gallery-simple gallery-subs

.PHONY: gallery-simple

gallery-simple::
652
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
Andrei Paskevich's avatar
Andrei Paskevich committed
653
	@for x in examples/*/why3session.xml ; do \
654 655
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
656
	  why3 session html $$x; \
657 658
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
659
	  cp examples/$$f.mlw examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
660
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
Andrei Paskevich's avatar
Andrei Paskevich committed
661
	  cd examples/; \
662
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
663
	  cd ..; \
664
	done
665

666 667
.PHONY: gallery-subs

668
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp
669 670

gallery-subs::
671
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
672 673 674 675 676 677 678 679 680 681 682
	@for d in $(GALLERYSUBS) ; do \
	  echo "exporting examples/$$d"; \
	  rm -f $(GALLERYDIR)/$$d/$$d.zip; \
	  cd examples/$$d; \
	  why3 -L . doc --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
	  cd ..; \
	  zip -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
	  cd ..; \
	done


683 684 685 686 687
%-gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	x=$*/why3session.xml; \
	d=`dirname $$x`; \
	f=`basename $$d`; \
688
	why3 session html $$d; \
689
	rm $$d/*.bak; \
690 691
	echo "exporting $$f"; \
	mkdir -p $(GALLERYDIR)/$$f; \
692 693
	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; \
694
	cp examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
695 696
	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	cd examples/; \
697
	zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
698

MARCHE Claude's avatar
MARCHE Claude committed
699 700 701 702 703 704 705 706
########
# XML DTD validation
########

.PHONY: xml-validate

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

710 711 712 713 714
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
715 716 717 718
###############
# IDE
###############

719 720
ifeq (@enable_ide@,yes)

Sylvain Dailler's avatar
Sylvain Dailler committed
721
IDE_FILES = gconfig ide_utils why3ide
MARCHE Claude's avatar
MARCHE Claude committed
722 723 724

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

Andrei Paskevich's avatar
Andrei Paskevich committed
725
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
726 727 728
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

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

732
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
733

734 735
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
736

737
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
Andrei Paskevich's avatar
Andrei Paskevich committed
738
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
739

740
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
741 742
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
MARCHE Claude's avatar
MARCHE Claude committed
743

744
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
745 746
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
MARCHE Claude's avatar
MARCHE Claude committed
747

748
src/ide/resetgc.o: src/ide/resetgc.c
749 750
	$(SHOW) 'Ocamlc   $<'
	$(HIDE)$(OCAMLC) -c -ccopt "-Wall -o $@" $<
751

MARCHE Claude's avatar
MARCHE Claude committed
752 753
# depend and clean targets

754
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
755
-include $(IDEDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
756
endif
MARCHE Claude's avatar
MARCHE Claude committed
757

Andrei Paskevich's avatar
Andrei Paskevich committed
758
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
759

Andrei Paskevich's avatar
Andrei Paskevich committed
760
CLEANDIRS += src/ide
MARCHE Claude's avatar
MARCHE Claude committed
761

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
762 763 764
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

765
install_no_local::
766
	$(INSTALL) bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
767

768
install_local:: bin/why3ide
769

770
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
771

772

773 774 775 776
###############
# WEBSERV
###############

777
WEBSERV_FILES = wserver why3web
778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819

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


820 821 822 823
###############
# Session
###############

824
SESSION_FILES = why3session_lib why3session_info \
MARCHE Claude's avatar
MARCHE Claude committed
825
		why3session_html why3session_latex \
826
		why3session_main
827
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
MARCHE Claude's avatar
MARCHE Claude committed
828
#       why3session_output
829 830 831

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

Andrei Paskevich's avatar
Andrei Paskevich committed
832
SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
833 834 835
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
836
$(SESSIONDEP): DEPFLAGS += -I src/why3session
837 838 839 840 841 842 843
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

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

844
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
845 846
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
847

848
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
849 850
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
851 852 853

# depend and clean targets

854
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
855
-include $(SESSIONDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
856
endif
857

Andrei Paskevich's avatar
Andrei Paskevich committed
858
depend: $(SESSIONDEP)
859

Andrei Paskevich's avatar
Andrei Paskevich committed
860
CLEANDIRS += src/why3session
861

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
862 863 864
clean_old_install::
	rm -f $(BINDIR)/why3session$(EXE)

865
install_no_local::
866
	$(INSTALL) bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
867

868
install_local:: bin/why3session
869

MARCHE Claude's avatar
MARCHE Claude committed
870 871 872 873
###############
# Why3 Shell
###############

Sylvain Dailler's avatar
Sylvain Dailler committed
874
SHELL_FILES = unix_scheduler why3shell
MARCHE Claude's avatar
MARCHE Claude committed
875

876
SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
MARCHE Claude's avatar
MARCHE Claude committed
877 878 879 880 881

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

882 883
$(SHELLDEP): DEPFLAGS += -I src/tools
$(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
MARCHE Claude's avatar
MARCHE Claude committed
884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913

# 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
914

915 916 917
##############
# Coq plugin
##############
918

Andrei Paskevich's avatar
Andrei Paskevich committed
919
ifeq (@enable_coq_tactic@,yes)
920

921
COQPGENERATED = src/coq-tactic/why3tac.ml
922

923
COQP_FILES = why3tac