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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127 128 129
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130

131 132 133 134
all: @OCAMLBEST@
plugins: plugins.@OCAMLBEST@
opt: plugins.opt
byte: plugins.byte
Francois Bobot's avatar
Francois Bobot committed
135

136 137 138 139 140
ifeq (@enable_local@,yes)
all: install_local
endif

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

Andrei Paskevich's avatar
Andrei Paskevich committed
143 144 145 146
CLEANDIRS =
CLEANLIBS =
GENERATED =

147 148 149
##############
# Why3 library
##############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150

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

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

172
LIB_CORE = ident ty term pattern decl coercion theory \
173
	   task pretty_sig pretty dterm env trans printer model_parser
174

175
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
176 177 178 179
		whyconf autodetection \
		smt2_model_defs parse_smtv2_model_parser \
		collect_data_model parse_smtv2_model_lexer parse_smtv2_model \
		parse_smtv2_model
180

181
LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr \
182
          pinterp mltree compile pdriver cprinter ocaml_printer
183

184
LIB_PARSER = ptree glob typing parser lexer
185

186
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
Clément Fumex's avatar
Clément Fumex committed
187
		detect_polymorphism reduction_engine compute \
188
		eliminate_definition eliminate_algebraic \
189
		eliminate_inductive eliminate_let eliminate_if \
190 191 192 193
		libencoding discriminate encoding encoding_select \
		encoding_guards_full encoding_tags_full \
		encoding_guards encoding_tags encoding_twin \
		encoding_sort simplify_array filter_trigger \
194
		introduction abstraction close_epsilon lift_epsilon \
195
		eliminate_epsilon intro_projections_counterexmp \
196
		intro_vc_vars_counterexmp prepare_for_counterexmp \
Andrei Paskevich's avatar
Andrei Paskevich committed
197
		instantiate_predicate smoke_detector \
198
		induction_pr prop_curry eliminate_literal \
Sylvain Dailler's avatar
Sylvain Dailler committed
199
		args_wrapper generic_arg_trans_utils case apply \
200
		ind_itp destruct cut
201

Sylvain Dailler's avatar
Sylvain Dailler committed
202
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
203
	      pvs isabelle \
204
	      simplify gappa cvc3 yices mathematica
205

206 207 208
LIB_SESSION = compress xml termcode session_itp \
              strategy strategy_parser controller_itp \
	      server_utils itp_communication \
209
	      itp_server json_util
210

211
LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
212 213
	      $(addprefix src/core/, $(LIB_CORE)) \
	      $(addprefix src/driver/, $(LIB_DRIVER)) \
214
	      $(addprefix src/mlw/, $(LIB_MLW)) \
215
	      $(addprefix src/parser/, $(LIB_PARSER)) \
216
	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
François Bobot's avatar
François Bobot committed
217
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
218
	      $(addprefix src/session/, $(LIB_SESSION))
219

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

Andrei Paskevich's avatar
Andrei Paskevich committed
223
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
224 225
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
226

Andrei Paskevich's avatar
Andrei Paskevich committed
227
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
228
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
229
$(LIBCMX): OFLAGS += -for-pack Why3
230

231 232
$(LIBDEP): $(LIBGENERATED)

233 234 235
# Zarith

ifeq (@enable_zarith@,yes)
236
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
237
	cp lib/ocaml/why3__BigInt_zarith.ml $@
238
else
239
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
240
	cp lib/ocaml/why3__BigInt_num.ml $@
241 242
endif

243 244 245 246 247 248 249 250 251 252
# 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

253 254 255 256 257
# hide deprecated warnings for strings

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

258 259 260 261
# 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

262
# build targets
263

264 265
byte: lib/why3/why3.cma
opt:  lib/why3/why3.cmxa
266

267 268
lib/why3/why3.cma: lib/why3/why3.cmo
lib/why3/why3.cmxa: lib/why3/why3.cmx
269

270
lib/why3/why3.cmo: $(LIBCMO)
271 272
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
273

274
lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
275
	$(SHOW) 'Linking  $@'
276
	$(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
277

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

280
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
281
-include $(LIBDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
282
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
283

284
depend: $(LIBDEP)
285

Andrei Paskevich's avatar
Andrei Paskevich committed
286 287 288
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
CLEANLIBS += lib/why3/why3session lib/why3/why3
GENERATED += $(LIBGENERATED)
289

290 291 292
###############
# installation
###############
293

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
294 295
clean_old_install::
	rm -rf $(LIBDIR)/why3
MARCHE Claude's avatar
MARCHE Claude committed
296
	rm -rf $(DATADIR)/why3
297
	rm -rf $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
298

299 300

install_no_local:: clean_old_install
301 302 303 304 305 306
	$(MKDIR_P) $(BINDIR)
	$(MKDIR_P) $(LIBDIR)/why3
	$(MKDIR_P) $(TOOLDIR)
	$(MKDIR_P) $(DATADIR)/why3
	$(MKDIR_P) $(DATADIR)/why3/images
	$(MKDIR_P) $(DATADIR)/why3/vim
307 308
	$(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
	$(MKDIR_P) $(DATADIR)/why3/vim/syntax
309 310 311 312 313 314 315 316 317 318
	$(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/
319 320
	for i in share/images/*.rc; do \
	     d=`basename $$i .rc`; \
321 322 323
	     $(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
	     $(MKDIR_P) $(DATADIR)/why3/images/$$d; \
	     $(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
324
	done
325 326 327
	$(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
	$(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3
	$(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3
328 329
	$(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
330
	$(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
331

MARCHE Claude's avatar
MARCHE Claude committed
332
install_no_local_lib::
333 334
	$(MKDIR_P) $(OCAMLINSTALLLIB)/why3
	$(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \
335
		lib/why3/META $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
336

337 338
ifeq (@enable_local@,yes)
install install-lib:
339 340
	@echo "Why3 is configured in local installation mode."
	@echo "To install Why3, run ./configure --disable-local ; make ; make install"
341
else
MARCHE Claude's avatar
MARCHE Claude committed
342
install: clean_old_install install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
343
install-lib: install_no_local_lib
344 345
endif

MARCHE Claude's avatar
MARCHE Claude committed
346 347
install-all: install install-lib

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
348 349 350 351 352 353
##################
# Uninstallation
##################

uninstall: clean_old_install

354 355 356 357 358 359 360
##################
# Why3 emacs mode
##################

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
361 362 363 364 365
clean_old_install::
	rm -f $(DATADIR)/emacs/site-lisp/why3.el
	rm -f $(DATADIR)/emacs/site-lisp/why3.elc

install_no_local::
366
	$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
367
	$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
368
ifeq (@enable_emacs_compilation@,yes)
369
	$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
370 371
endif

372
ifeq (@enable_emacs_compilation@,yes)
373
all: share/emacs/why3.elc
374 375
endif

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

377
##################
378
# Why3 plugins
379 380
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
381
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
382
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
383 384
		plugins/python/py_lexer.ml \
		plugins/python/py_parser.ml plugins/python/py_parser.mli \
385
		plugins/parser/dimacs.ml \
386

387
PLUG_PARSER = genequlin dimacs
388
PLUG_PRINTER =
389
PLUG_TRANSFORM =
390
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
391
PLUG_PYTHON = py_ast py_parser py_lexer py_main
392

393
PLUGINS = genequlin dimacs tptp python
394

Andrei Paskevich's avatar
Andrei Paskevich committed
395
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
396
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
Andrei Paskevich's avatar
Andrei Paskevich committed
397

Andrei Paskevich's avatar
Andrei Paskevich committed
398 399
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
400

401 402 403
PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))

404 405 406 407 408 409 410 411 412 413
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

414 415
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
416
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
417
	      $(TPTPMODULES) $(PYTHONMODULES)
418

Andrei Paskevich's avatar
Andrei Paskevich committed
419
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
420 421 422
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

423
PLUGDIRS = parser printer transform tptp python
424 425
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
426
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
427 428
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

429 430
$(PLUGDEP): $(PLUGGENERATED)

431 432 433 434 435
LIBPLUGCMO =  $(addsuffix .cmo,  $(addprefix lib/plugins/, $(PLUGINS)))
LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
436 437

lib/plugins/%.cmxs: plugins/parser/%.cmx
438 439
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
440 441

lib/plugins/%.cmo: plugins/parser/%.cmo
442 443
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
444 445

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
461
lib/plugins/tptp.cmxs: $(TPTPCMX)
462 463
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
464

Andrei Paskevich's avatar
Andrei Paskevich committed
465
lib/plugins/tptp.cmo: $(TPTPCMO)
466 467
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
468

469 470 471 472 473 474 475
lib/plugins/python.cmxs: $(PYTHONCMX)
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^

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

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

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

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

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

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

492 493 494 495
###############
# Why3 commands
###############

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

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

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

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

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

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

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

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

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

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

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

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

568
depend: $(TOOLSDEP)
569

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

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

576 577 578
##############
# test targets
##############
579

580 581
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
582

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

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

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

592
%.type: %.mlw bin/why3ide.opt
593
	bin/why3.opt --type-only $*.mlw
594

595 596 597 598
##############
# Why3server #
##############

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

608 609
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)

610
all: $(TOOLS)
611

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

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

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

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

clean::
628
	rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
629

630 631 632 633
##########
# gallery
##########

634
# we export exactly the programs that have a why3session.xml file
635 636 637

.PHONY: gallery

638 639 640 641 642
gallery:: gallery-simple gallery-subs

.PHONY: gallery-simple

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

657 658
.PHONY: gallery-subs

659
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp
660 661

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


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

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

.PHONY: xml-validate

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

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

710 711
ifeq (@enable_ide@,yes)

Sylvain Dailler's avatar
Sylvain Dailler committed
712
IDE_FILES = gconfig ide_utils why3ide
MARCHE Claude's avatar
MARCHE Claude committed
713 714 715

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

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

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

723
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
724

725 726
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
727

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
743 744
# depend and clean targets

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

Andrei Paskevich's avatar
Andrei Paskevich committed
749
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
750

Andrei Paskevich's avatar
Andrei Paskevich committed
751
CLEANDIRS += src/ide
MARCHE Claude's avatar
MARCHE Claude committed
752

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

756
install_no_local::
757
	$(INSTALL) bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
758

759
install_local:: bin/why3ide
760

761
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
762

763

764 765 766 767
###############
# WEBSERV
###############

768
WEBSERV_FILES = wserver why3web
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 809 810

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


811 812 813 814
###############
# Session
###############

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

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

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

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

# build targets

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

835
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
836 837
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
838

839
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
840 841
	$(SHOW) 'Linking  $@'
	$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
842 843 844

# depend and clean targets

845
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
846
-include $(SESSIONDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
847
endif
848

Andrei Paskevich's avatar
Andrei Paskevich committed
849
depend: $(SESSIONDEP)
850

Andrei Paskevich's avatar
Andrei Paskevich committed
851
CLEANDIRS += src/why3session
852

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
853 854 855
clean_old_install::
	rm -f $(BINDIR)/why3session$(EXE)

856
install_no_local::
857
	$(INSTALL) bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
858

859
install_local:: bin/why3session
860

MARCHE Claude's avatar
MARCHE Claude committed
861 862 863 864
###############
# Why3 Shell
###############

Sylvain Dailler's avatar
Sylvain Dailler committed
865
SHELL_FILES = unix_scheduler why3shell
MARCHE Claude's avatar
MARCHE Claude committed
866

867
SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
MARCHE Claude's avatar
MARCHE Claude committed
868 869 870 871 872

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

873 874
$(SHELLDEP): DEPFLAGS += -I src/tools
$(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
MARCHE Claude's avatar
MARCHE Claude committed
875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904

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

906 907 908
##############
# Coq plugin
##############
909

Andrei Paskevich's avatar
Andrei Paskevich committed
910
ifeq (@enable_coq_tactic@,yes)
911

912
COQPGENERATED = src/coq-tactic/why3tac.ml
913

914
COQP_FILES = why3tac
915

916
COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
917

918 919 920
COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
921

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

925
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
926
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
Andrei Paskevich's avatar
Andrei Paskevich committed
927 928
$(COQPCMO) $(COQPCMX): BFLAGS += -rectypes
$(COQPCMX): OFLAGS += -rectypes
929

930
$(COQPDEP): $(COQPGENERATED)
931

932 933
byte: lib/coq-tactic/why3tac.cma
opt:  lib/coq-tactic/why3tac.cmxs
934

935 936 937 938
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@)
939
lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cmo,  @MENHIRLIB@)
940

941 942
lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
943

944
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
945 946
	$(SHOW) 'Camlp    $<'
	$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
947

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

950 951 952 953 954
ifeq "$(OCAMLBEST)" "opt"
COQTACEXT = cmxs
else
COQTACEXT = cma
COQRTAC += -byte
Guillaume Melquiond's avatar
Guillaume Melquiond committed
955
endif
Guillaume Melquiond's avatar
Guillaume Melquiond committed
956

957
lib/coq-tactic/Why3.vo: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.$(COQTACEXT)
958
	$(SHOW) 'Coqc     $<'
959
	$(HIDE)WHY3CONFIG="" $(COQC) $(COQRTAC) $<
960

961
all: lib/coq-tactic/Why3.vo
962

963
# depend and clean targets
Andrei Paskevich's avatar
Andrei Paskevich committed
964

965
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
966
-include $(COQPDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
967
endif
968

969
depend: $(COQPDEP)
970

Andrei Paskevich's avatar
Andrei Paskevich committed
971 972 973 974
CLEANDIRS += src/coq-tactic
CLEANLIBS += lib/coq-tactic/why3tac
GENERATED += $(COQPGENERATED)

975
clean::
976
	rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
977

978
install_no_local::
979 980
	$(MKDIR_P) $(LIBDIR)/why3/coq-tactic
	$(INSTALL_DATA) lib/coq-tactic/* $(LIBDIR)/why3/coq-tactic
981

982 983 984 985 986 987
endif

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

988 989
ifeq (@enable_coq_support@,yes)

Guillaume Melquiond's avatar