Makefile.in 71.8 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
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  #
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
# 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

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
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
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 270
byte: lib/why3/why3.cma
opt:  lib/why3/why3.cmxa
271

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

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

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

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

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

289
depend: $(LIBDEP)
290

Andrei Paskevich's avatar
Andrei Paskevich committed
291 292 293
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
CLEANLIBS += lib/why3/why3session lib/why3/why3
GENERATED += $(LIBGENERATED)
294

295 296 297
###############
# installation
###############
298

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
299 300
clean_old_install::
	rm -rf $(LIBDIR)/why3
MARCHE Claude's avatar
MARCHE Claude committed
301 302
	rm -rf $(DATADIR)/why3

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

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

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

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

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
355 356 357 358
##################
# Uninstallation
##################

359 360 361 362 363 364
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
365

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

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

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

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

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

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

389
##################
390
# Why3 plugins
391 392
##################

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

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

405
PLUGINS = genequlin dimacs tptp python
406

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

Andrei Paskevich's avatar
Andrei Paskevich committed
410 411
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
412

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

416 417 418 419 420 421 422 423 424 425
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

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

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

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

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

441 442
$(PLUGDEP): $(PLUGGENERATED)

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

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

449 450
lib/plugins:
	mkdir lib/plugins
451

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

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

460 461
lib/plugins/%.cmxs: plugins/parser/%.cmx
lib/plugins/%.cmo: plugins/parser/%.cmo
462 463 464 465
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
466 467
lib/plugins/tptp.cmxs: $(TPTPCMX)
lib/plugins/tptp.cmo: $(TPTPCMO)
468 469
lib/plugins/python.cmxs: $(PYTHONCMX)
lib/plugins/python.cmo: $(PYTHONCMO)
470

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
479 480
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
GENERATED += $(PLUGGENERATED)
481 482

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

486 487 488 489
###############
# Why3 commands
###############

Andrei Paskevich's avatar
Andrei Paskevich committed
490 491
TOOLSGENERATED = src/tools/why3wc.ml

492
TOOLS_BIN = why3config why3execute why3extract why3prove \
Andrei Paskevich's avatar
Andrei Paskevich committed
493 494
	    why3realize why3replay why3wc

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

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
506 507
$(TOOLSDEP): $(TOOLSGENERATED)

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

511 512 513
bin:
	mkdir bin

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

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

535
install_no_local::
536 537 538 539 540 541 542 543
	$(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)
544 545

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

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

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

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

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

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

562
depend: $(TOOLSDEP)
563

Andrei Paskevich's avatar
Andrei Paskevich committed
564 565 566
CLEANDIRS += src/tools
GENERATED += $(TOOLSGENERATED)

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

570 571 572
##############
# test targets
##############
573

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

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

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

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

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

589 590 591 592
##############
# Why3server #
##############

593 594 595 596 597 598 599 600
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)))
601

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

604
all: $(TOOLS)
605

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

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

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

install_no_local::
616 617 618 619
	$(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
620 621

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

624 625 626 627
##########
# gallery
##########

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

.PHONY: gallery

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

.PHONY: gallery-simple

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

651 652
.PHONY: gallery-subs

653
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover
654 655

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


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

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

.PHONY: xml-validate

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

695 696 697 698 699
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
700 701 702 703
###############
# IDE
###############

704 705
ifeq (@enable_ide@,yes)

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

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

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

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

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

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

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

726 727
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
728

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
741
CLEANDIRS += src/ide
MARCHE Claude's avatar
MARCHE Claude committed
742

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
743 744 745
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

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

749
install_local:: bin/why3ide
750

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

753

754 755 756 757
###############
# WEBSERV
###############

758
WEBSERV_FILES = wserver why3web
759 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

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


801 802 803 804
###############
# Session
###############

805
SESSION_FILES = why3session_lib why3session_info \
MARCHE Claude's avatar
MARCHE Claude committed
806
		why3session_html why3session_latex \
807
		why3session_main
808
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
MARCHE Claude's avatar
MARCHE Claude committed
809
#       why3session_output
810 811 812

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

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

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

# build targets

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

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

# depend and clean targets

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
836
CLEANDIRS += src/why3session
837

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
838 839 840
clean_old_install::
	rm -f $(BINDIR)/why3session$(EXE)

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

844
install_local:: bin/why3session
845

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

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

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

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

858 859
$(SHELLDEP): DEPFLAGS += -I src/tools
$(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
MARCHE Claude's avatar
MARCHE Claude committed
860 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

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

891 892 893
##############
# Coq plugin
##############
894

Andrei Paskevich's avatar
Andrei Paskevich committed
895
ifeq (@enable_coq_tactic@,yes)
896

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

899
COQP_FILES = why3tac
900

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

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

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

910
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
911
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
Andrei Paskevich's avatar
Andrei Paskevich committed
912 913
$(COQPCMO) $(COQPCMX): BFLAGS += -rectypes
$(COQPCMX): OFLAGS += -rectypes
914

915
$(COQPDEP): $(COQPGENERATED)
916

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

920 921 922 923
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@)
924
lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cmo,  @MENHIRLIB@)
925

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

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

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

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

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

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

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

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

954
depend: $(COQPDEP)
955

Andrei Paskevich's avatar
Andrei Paskevich committed
956 957 958 959
CLEANDIRS += src/coq-tactic
CLEANLIBS += lib/coq-tactic/why3tac
GENERATED += $(COQPGENERATED)

960
clean::
961
	rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
962

963
install_no_local::