Makefile.in 72.8 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) -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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
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 170
LIB_UTIL = config bigInt util opt lists strings \
	   extmap extset exthtbl weakhtbl \
171 172 173
	   hashcons stdlib exn_printer pp \
	   json_base json_parser json_lexer \
	   debug loc \
174
	   lexlib print_tree 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 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 dexpr pdecl pmodule
186

187 188
LIB_PARSER = ptree glob parser typing lexer

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

Sylvain Dailler's avatar
Sylvain Dailler committed
206
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
207
	      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
# hide deprecated warnings for strings

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

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

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

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 306
	rm -rf $(DATADIR)/why3

307 308 309 310
clean_old_install-lib::
	if test -d $(OCAMLINSTALLLIB) -a -w $(OCAMLINSTALLLIB); then \
	  rm -f $(OCAMLINSTALLLIB)/why3; \
	fi
311

312
install_no_local::
313 314 315 316 317 318
	$(MKDIR_P) $(BINDIR)
	$(MKDIR_P) $(LIBDIR)/why3
	$(MKDIR_P) $(TOOLDIR)
	$(MKDIR_P) $(DATADIR)/why3
	$(MKDIR_P) $(DATADIR)/why3/images
	$(MKDIR_P) $(DATADIR)/why3/vim
319 320
	$(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
	$(MKDIR_P) $(DATADIR)/why3/vim/syntax
321 322 323 324 325 326 327 328 329 330
	$(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/
331 332
	for i in share/images/*.rc; do \
	     d=`basename $$i .rc`; \
333 334 335
	     $(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
	     $(MKDIR_P) $(DATADIR)/why3/images/$$d; \
	     $(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
336
	done
337 338 339
	$(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
	$(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3
	$(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3
340 341
	$(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
342
	$(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
343

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

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

MARCHE Claude's avatar
MARCHE Claude committed
358 359
install-all: install install-lib

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
360 361 362 363
##################
# Uninstallation
##################

364 365 366 367 368 369
ifeq (@enable_local@,yes)
uninstall:
	@echo "Why3 is configured in local installation mode."
else
uninstall: clean_old_install clean_old_install-lib
endif
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
370

371 372 373 374 375 376 377
##################
# Why3 emacs mode
##################

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
378 379 380 381 382
clean_old_install::
	rm -f $(DATADIR)/emacs/site-lisp/why3.el
	rm -f $(DATADIR)/emacs/site-lisp/why3.elc

install_no_local::
383
	$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
384
	$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
385
ifeq (@enable_emacs_compilation@,yes)
386
	$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
387 388
endif

389
ifeq (@enable_emacs_compilation@,yes)
390
all: share/emacs/why3.elc
391 392
endif

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

394
##################
395
# Why3 plugins
396 397
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
398
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
399
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
400 401
		plugins/python/py_lexer.ml \
		plugins/python/py_parser.ml plugins/python/py_parser.mli \
402
		plugins/parser/dimacs.ml \
403

404
PLUG_PARSER = genequlin dimacs
405
PLUG_PRINTER =
406
PLUG_TRANSFORM =
407
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
408
PLUG_PYTHON = py_ast py_parser py_lexer py_main
409

410
PLUGINS = genequlin dimacs tptp python
411

Andrei Paskevich's avatar
Andrei Paskevich committed
412
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
413
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
Andrei Paskevich's avatar
Andrei Paskevich committed
414

Andrei Paskevich's avatar
Andrei Paskevich committed
415 416
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
417

418 419 420
PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))

421 422 423 424 425 426 427 428 429 430
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

431 432
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
433
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
434
	      $(TPTPMODULES) $(PYTHONMODULES)
435

Andrei Paskevich's avatar
Andrei Paskevich committed
436
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
437 438 439
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

440
PLUGDIRS = parser printer transform tptp python
441 442
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
443
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
444 445
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

446 447
$(PLUGDEP): $(PLUGGENERATED)

448 449 450 451 452
LIBPLUGCMO =  $(addsuffix .cmo,  $(addprefix lib/plugins/, $(PLUGINS)))
LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

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

454 455
lib/plugins:
	mkdir lib/plugins
456

457
lib/plugins/%.cmxs: | lib/plugins
458
	$(SHOW) 'Linking  $@'
459
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
460

461
lib/plugins/%.cmo: | lib/plugins
462
	$(SHOW) 'Linking  $@'
463
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
464

465 466
lib/plugins/%.cmxs: plugins/parser/%.cmx
lib/plugins/%.cmo: plugins/parser/%.cmo
467 468 469 470
lib/plugins/%.cmxs: plugins/printer/%.cmx
lib/plugins/%.cmo: plugins/printer/%.cmo
lib/plugins/%.cmxs: plugins/transform/%.cmx
lib/plugins/%.cmo: plugins/transform/%.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
471 472
lib/plugins/tptp.cmxs: $(TPTPCMX)
lib/plugins/tptp.cmo: $(TPTPCMO)
473 474
lib/plugins/python.cmxs: $(PYTHONCMX)
lib/plugins/python.cmo: $(PYTHONCMO)
475

Andrei Paskevich's avatar
Andrei Paskevich committed
476 477
# depend and clean targets

478
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
479
-include $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
480 481
endif

482
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
483

Andrei Paskevich's avatar
Andrei Paskevich committed
484 485
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
GENERATED += $(PLUGGENERATED)
486 487

install_no_local::
488 489
	$(MKDIR_P) $(LIBDIR)/why3/plugins
	$(INSTALL_DATA) $(wildcard $(LIBPLUGCMO) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins
490

491 492 493 494
###############
# Why3 commands
###############

Andrei Paskevich's avatar
Andrei Paskevich committed
495 496 497
TOOLSGENERATED = src/tools/why3wc.ml

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

Andrei Paskevich's avatar
Andrei Paskevich committed
500
TOOLS_FILES = main $(TOOLS_BIN)
501 502 503 504 505 506 507 508 509 510

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
511 512
$(TOOLSDEP): $(TOOLSGENERATED)

513 514 515
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt:  bin/why3.opt  $(TOOLS_BIN:%=bin/%.opt)

516 517 518
bin:
	mkdir bin

Andrei Paskevich's avatar
Andrei Paskevich committed
519 520
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
521 522
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
523 524 525 526 527 528 529 530
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
531 532
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
533 534 535
bin/why3wc.opt: src/tools/why3wc.cmx
bin/why3wc.byte: src/tools/why3wc.cmo

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
536
clean_old_install::
537
	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
538
	rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
539

540
install_no_local::
541 542 543 544 545 546 547 548
	$(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)
549 550

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

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

555 556 557 558 559 560 561 562 563 564 565
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

566
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
567
-include $(TOOLSDEP)
568 569
endif

570
depend: $(TOOLSDEP)
571

Andrei Paskevich's avatar
Andrei Paskevich committed
572 573 574
CLEANDIRS += src/tools
GENERATED += $(TOOLSGENERATED)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
575
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
576
	rm -f bin/why3*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
577

578 579 580
##############
# test targets
##############
581

582 583
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
584

585 586
%: %.mlw bin/why3.opt
	bin/why3.opt $*.mlw
587

588 589
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
590

591 592
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
593

594
%.type: %.mlw bin/why3ide.opt
595
	bin/why3.opt --type-only $*.mlw
596

597 598 599 600
##############
# Why3server #
##############

601 602 603 604 605 606 607 608
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)))
609

610 611
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)

612
all: $(TOOLS)
613

614
lib/why3server$(EXE): $(SERVER_O)
615 616 617 618
	$(CC) -Wall -o $@ $^

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

620
%.o: %.c
621
	$(CC) -Wall -O -g -o $@ -c $<
622 623

install_no_local::
624 625 626 627
	$(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
628 629

clean::
630
	rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
631

632 633 634 635
##########
# gallery
##########

636
# we export exactly the programs that have a why3session.xml file
637 638 639

.PHONY: gallery

640 641 642 643 644
gallery:: gallery-simple gallery-subs

.PHONY: gallery-simple

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

659 660
.PHONY: gallery-subs

661
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover
662 663

gallery-subs::
664
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
665 666
	@for d in $(GALLERYSUBS) ; do \
	  echo "exporting examples/$$d"; \
667
	  mkdir -p $(GALLERYDIR)/$$d; \
668
	  cd examples/$$d; \
669
	  WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../theories -L ../../modules -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
670
	  cd ..; \
671 672
	  rm -f $(GALLERYDIR)/$$d/$$d.zip; \
	  zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
673 674 675 676
	  cd ..; \
	done


677 678 679 680 681 682
%-gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	x=$*/why3session.xml; \
	d=`dirname $$x`; \
	f=`basename $$d`; \
	echo "exporting $$f"; \
683
	rm -f $$d/*.bak; \
684
	mkdir -p $(GALLERYDIR)/$$f; \
685
	WHY3CONFIG="" bin/why3session.@OCAMLBEST@ html $$d -o $(GALLERYDIR)/$$f; \
686 687
	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; \
688
	cd examples/; \
689 690
	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	zip -q -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
691

MARCHE Claude's avatar
MARCHE Claude committed
692 693 694 695 696 697 698 699
########
# XML DTD validation
########

.PHONY: xml-validate

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

703 704 705 706 707
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
708 709 710 711
###############
# IDE
###############

712 713
ifeq (@enable_ide@,yes)

Sylvain Dailler's avatar
Sylvain Dailler committed
714
IDE_FILES = gconfig ide_utils why3ide
MARCHE Claude's avatar
MARCHE Claude committed
715 716 717

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

Andrei Paskevich's avatar
Andrei Paskevich committed
718
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
719 720 721
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

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

725
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
726

727 728
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
729

730
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
Andrei Paskevich's avatar
Andrei Paskevich committed
731
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
732
bin/why3ide.byte: BLINKFLAGS += -custom
MARCHE Claude's avatar
MARCHE Claude committed
733

734 735
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
736

737
src/ide/resetgc.o: src/ide/resetgc.c
738 739
	$(SHOW) 'Ocamlc   $<'
	$(HIDE)$(OCAMLC) -c -ccopt "-Wall -o $@" $<
740

MARCHE Claude's avatar
MARCHE Claude committed
741 742
# depend and clean targets

743
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
744
-include $(IDEDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
745
endif
MARCHE Claude's avatar
MARCHE Claude committed
746

Andrei Paskevich's avatar
Andrei Paskevich committed
747
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
748

Andrei Paskevich's avatar
Andrei Paskevich committed
749
CLEANDIRS += src/ide
MARCHE Claude's avatar
MARCHE Claude committed
750

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
751 752 753
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

754
install_no_local::
755
	$(INSTALL) bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
756

757
install_local:: bin/why3ide
758

759
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
760

761

762 763 764 765
###############
# WEBSERV
###############

766
WEBSERV_FILES = wserver why3web
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 802 803 804 805 806 807 808

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


809 810 811 812
###############
# Session
###############

813
SESSION_FILES = why3session_lib why3session_info \
MARCHE Claude's avatar
MARCHE Claude committed
814
		why3session_html why3session_latex \
815
		why3session_main
816
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
MARCHE Claude's avatar
MARCHE Claude committed
817
#       why3session_output
818 819 820

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

Andrei Paskevich's avatar
Andrei Paskevich committed
821
SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
822 823 824
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
825
$(SESSIONDEP): DEPFLAGS += -I src/why3session
826 827 828 829 830 831 832
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

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

833 834
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
835 836 837

# depend and clean targets

838
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
839
-include $(SESSIONDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
840
endif
841

Andrei Paskevich's avatar
Andrei Paskevich committed
842
depend: $(SESSIONDEP)
843

Andrei Paskevich's avatar
Andrei Paskevich committed
844
CLEANDIRS += src/why3session
845

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
846 847 848
clean_old_install::
	rm -f $(BINDIR)/why3session$(EXE)

849
install_no_local::
850
	$(INSTALL) bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
851

852
install_local:: bin/why3session
853

MARCHE Claude's avatar
MARCHE Claude committed
854 855 856 857
###############
# Why3 Shell
###############

Sylvain Dailler's avatar
Sylvain Dailler committed
858
SHELL_FILES = unix_scheduler why3shell
MARCHE Claude's avatar
MARCHE Claude committed
859

860
SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
MARCHE Claude's avatar
MARCHE Claude committed
861 862 863 864 865

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

866 867
$(SHELLDEP): DEPFLAGS += -I src/tools
$(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
MARCHE Claude's avatar
MARCHE Claude committed
868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897

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

899 900 901
##############
# Coq plugin
##############
902

Andrei Paskevich's avatar
Andrei Paskevich committed
903
ifeq (@enable_coq_tactic@,yes)
904

905
COQPGENERATED = src/coq-tactic/why3tac.ml
906

907
COQP_FILES = why3tac
908

909
COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
910

911 912 913
COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
914

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

918
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
919
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
Andrei Paskevich's avatar
Andrei Paskevich committed
920 921
$(COQPCMO) $(COQPCMX): BFLAGS += -rectypes
$(COQPCMX): OFLAGS += -rectypes
922

923
$(COQPDEP): $(COQPGENERATED)
924

925 926
byte: lib/coq-tactic/why3tac.cma
opt:  lib/coq-tactic/why3tac.cmxs
927

928 929 930 931
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@)
932
lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cmo,  @MENHIRLIB@)
933

934 935
lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
936

937
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
938 939
	$(SHOW) 'Camlp    $<'
	$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
940

941
COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3 -I lib/coq-tactic
Guillaume Melquiond's avatar
Guillaume Melquiond committed
942

943 944 945 946 947
ifeq "$(OCAMLBEST)" "opt"
COQTACEXT = cmxs
else
COQTACEXT = cma
COQRTAC += -byte
Guillaume Melquiond's avatar
Guillaume Melquiond committed
948
endif
Guillaume Melquiond's avatar
Guillaume Melquiond committed
949

950
lib/coq-tactic/Why3.vo: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.$(COQTACEXT)
951
	$(SHOW) 'Coqc     $<'
952
	$(HIDE)WHY3CONFIG="" $(COQC) $(COQRTAC) $<
953

954
all: lib/coq-tactic/Why3.vo
955

956
# depend and clean targets
Andrei Paskevich's avatar
Andrei Paskevich committed
957

958
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
959
-include $(COQPDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
960
endif
961

962
depend: $(COQPDEP)
963

Andrei Paskevich's avatar
Andrei Paskevich committed
964 965 966 967
CLEANDIRS += src/coq-tactic
CLEANLIBS += lib/coq-tactic/why3tac
GENERATED += $(COQPGENERATED)

968
clean::
969
	rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
970

971
install_no_local::
972 973
	$(MKDIR_P) $(LIBDIR)/why3/coq-tactic
	$(INSTALL_DATA) lib/coq-tactic/* $(LIBDIR)/why3/coq-tactic
974

975 976 977 978 979 980
endif

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

981
COQVERSIONSPECIFIC=
982 983 984 985 986 987 988 989 990 991 992 993 994

COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
COQVERSIONSPECIFICSOURCES=$(addsuffix .@coq_compat_version@, $(COQVERSIONSPECIFICTARGETS))

$(COQVERSIONSPECIFICTARGETS): $(COQVERSIONSPECIFICSOURCES)
	for i in $(COQVERSIONSPECIFIC); do \
		cp lib/coq/$$i.@coq_compat_version@ lib/coq/$$i ; \
	done

clean::
	rm -f $(COQVERSIONSPECIFICTARGETS)


995
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf
996 997
COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
998