Makefile.in 66.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
####################################################################
#                                                                  #
#  The Why3 Verification Platform   /   The Why3 Development Team  #
Andrei Paskevich's avatar
Andrei Paskevich committed
4
#  Copyright 2010-2016   --   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
15
16
17
VERBOSEMAKE ?= @enable_verbose_make@

ifeq ($(VERBOSEMAKE),yes)
  QUIET =
else
  QUIET = yes
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
18
19
endif

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

23
prefix	    = @prefix@
24
25
26
27
28
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

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

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

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

54
55
56
57
58
59
ifeq (@enable_menhirLib@,yes)
MENHIR	  = @MENHIR@ --table
else
MENHIR	  = @MENHIR@
endif

60
DEPFLAGS  = -slash -I lib/why3
61
ifeq (@OCAMLBEST@,opt)
Andrei Paskevich's avatar
Andrei Paskevich committed
62
DEPFLAGS += -native
63
64
endif

65
RUBBER = @RUBBER@
66
HEVEA = @HEVEA@
67
HACHA = @HACHA@
68
EMACS = @EMACS@
69

70
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
71
#PDFVIEWER = @PDFVIEWER@
72

73
INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
74
75
76
77
78
79
80
81
82
83

# 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.
84
#   50   Unexpected documentation comment.
85
86
87
88
89
# - fatal:
#   5    Partially applied function: expression whose result has function
#        type and is ignored.
#   48   Implicit elimination of optional arguments.

90
WARNINGS = A-4-9-41-44-45-50@5@48
91

92
93
OFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
94
95
96

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

98
ifeq (@enable_profiling@,yes)
99
100
101
OFLAGS += -g -p
endif

102
103
104
105
106
ifeq (@enable_bin_annot@,yes)
OFLAGS += -bin-annot
BFLAGS += -bin-annot
endif

107
108
# external libraries common to all binaries

109
EXTOBJS = @MENHIRLIB@
110
EXTLIBS = str unix nums dynlink @ZIPLIB@
111
112
113

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
114

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

118
119
TARGET_EMACS = share/emacs/why3.elc

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
120
121
122
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123

124
125
126
127
all: @OCAMLBEST@
plugins: plugins.@OCAMLBEST@
opt: plugins.opt
byte: plugins.byte
Francois Bobot's avatar
Francois Bobot committed
128

129
130
131
132
133
ifeq (@enable_local@,yes)
all: install_local
endif

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

Andrei Paskevich's avatar
Andrei Paskevich committed
136
137
138
139
CLEANDIRS =
CLEANLIBS =
GENERATED =

140
141
142
##############
# Why3 library
##############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
143

144
LIBGENERATED = src/util/config.ml \
145
	       src/util/rc.ml src/util/lexlib.ml src/parser/lexer.ml \
146
147
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
148
	       src/driver/driver_lexer.ml \
149
150
               src/driver/parse_smtv2_model_parser.mli src/driver/parse_smtv2_model_parser.ml \
               src/driver/parse_smtv2_model_lexer.ml \
151
	       src/session/compress.ml src/session/xml.ml \
152
	       src/session/strategy_parser.ml \
153
	       lib/ocaml/why3__BigInt_compat.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
154

155
156
LIB_UTIL = config bigInt util opt lists strings \
	   extmap extset exthtbl weakhtbl \
157
	   hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
158
	   cmdline warning sysutil rc plugin bigInt number pqueue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
159

160
LIB_CORE = ident ty term pattern decl theory \
161
	   task pretty dterm env trans printer model_parser
162

163
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
164
	     whyconf autodetection \
165
             parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
166

167
LIB_MLW = ity expr dexpr pdecl pmodule
168

169
170
LIB_PARSER = ptree glob parser typing lexer

171
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
172
		detect_polymorphism \
173
		reduction_engine compute \
174
		eliminate_definition eliminate_algebraic \
175
		eliminate_inductive eliminate_let eliminate_if \
176
177
178
179
		libencoding discriminate encoding encoding_select \
		encoding_guards_full encoding_tags_full \
		encoding_guards encoding_tags encoding_twin \
		encoding_sort simplify_array filter_trigger \
180
		introduction abstraction close_epsilon lift_epsilon \
181
		eliminate_epsilon intro_projections_counterexmp \
182
		intro_vc_vars_counterexmp prepare_for_counterexmp \
MARCHE Claude's avatar
MARCHE Claude committed
183
		eval_match instantiate_predicate smoke_detector \
184
		induction_pr prop_curry
185

186
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
187
	      simplify gappa cvc3 yices mathematica
188

189
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
190
	    mlw_dexpr mlw_typing mlw_driver mlw_exec mlw_ocaml \
191
	    mlw_main mlw_interp
192

193
194
195
LIB_SESSION = compress xml termcode session session_tools strategy \
              strategy_parser session_scheduler

196
LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
197
198
	      $(addprefix src/core/, $(LIB_CORE)) \
	      $(addprefix src/driver/, $(LIB_DRIVER)) \
199
	      $(addprefix src/mlw/, $(LIB_MLW)) \
200
	      $(addprefix src/parser/, $(LIB_PARSER)) \
201
	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
François Bobot's avatar
François Bobot committed
202
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
203
204
	      $(addprefix src/whyml/, $(LIB_WHYML)) \
	      $(addprefix src/session/, $(LIB_SESSION))
205

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

Andrei Paskevich's avatar
Andrei Paskevich committed
209
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
210
211
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
212

Andrei Paskevich's avatar
Andrei Paskevich committed
213
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
214
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
215
$(LIBCMX): OFLAGS += -for-pack Why3
216

217
218
$(LIBDEP): $(LIBGENERATED)

219
220
221
# Zarith

ifeq (@enable_zarith@,yes)
222
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
223
	cp lib/ocaml/why3__BigInt_zarith.ml $@
224
else
225
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
226
	cp lib/ocaml/why3__BigInt_num.ml $@
227
228
endif

229
230
231
232
233
234
235
236
237
238
# 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

Johannes Kanig's avatar
Johannes Kanig committed
239
src/driver/vc_client.o: src/driver/vc_client.c
240
	gcc -O -mms-bitfields -Wall -Wno-unused -c -I$(OCAMLLIB) -fPIC $^
Johannes Kanig's avatar
Johannes Kanig committed
241
242
	mv $(CURDIR)/vc_client.o $@

243
244
245
src/driver/vc_client.so: src/driver/vc_client.c
	gcc -shared -O -mms-bitfields -Wall -Wno-unused -I$(OCAMLLIB) -fPIC $^ -o $@

246
247
248
249
250
# hide deprecated warnings for strings

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

251
# build targets
252

253
254
byte: lib/why3/why3.cma
opt:  lib/why3/why3.cmxa
255

256
lib/why3/why3.cma: src/driver/vc_client.so lib/why3/why3.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
257
	$(if $(QUIET),@echo 'Linking  $@' &&) \
258
	    $(OCAMLC)  -a $(BFLAGS) -o $@ $^
259

260
lib/why3/why3.cmxa: src/driver/vc_client.o lib/why3/why3.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
261
262
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) -a $(OFLAGS) -o $@ $^
263

264
lib/why3/why3.cmo: $(LIBCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
265
266
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
267

268
lib/why3/why3.cmx: $(LIBCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
269
270
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
271

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

274
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
275
include $(LIBDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
276
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277

278
depend: $(LIBDEP)
279

Andrei Paskevich's avatar
Andrei Paskevich committed
280
281
282
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
CLEANLIBS += lib/why3/why3session lib/why3/why3
GENERATED += $(LIBGENERATED)
283

284
285
286
###############
# installation
###############
287

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
288
289
clean_old_install::
	rm -rf $(LIBDIR)/why3
MARCHE Claude's avatar
MARCHE Claude committed
290
	rm -rf $(DATADIR)/why3
291
	rm -rf $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
292

293

294
ifeq ($(EMACS),no)
295
install_no_local:: clean_old_install
296
297
298
else
install_no_local:: clean_old_install $(TARGET_EMACS)
endif
299
	mkdir -p $(BINDIR)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
300
	mkdir -p $(LIBDIR)/why3
301
	mkdir -p $(TOOLDIR)
302
	mkdir -p $(DATADIR)/why3
303
	mkdir -p $(DATADIR)/why3/images
304
	mkdir -p $(DATADIR)/why3/vim
305
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
306
	mkdir -p $(DATADIR)/why3/theories
307
	mkdir -p $(DATADIR)/why3/modules/mach
MARCHE Claude's avatar
MARCHE Claude committed
308
	mkdir -p $(DATADIR)/why3/drivers
309
	mkdir -p $(DATADIR)/emacs/site-lisp/
MARCHE Claude's avatar
MARCHE Claude committed
310
	cp -f theories/*.why $(DATADIR)/why3/theories
311
	cp -f modules/*.mlw $(DATADIR)/why3/modules
312
	cp -f modules/mach/*.mlw $(DATADIR)/why3/modules/mach
Andrei Paskevich's avatar
Andrei Paskevich committed
313
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
MARCHE Claude's avatar
MARCHE Claude committed
314
	cp -f LICENSE $(DATADIR)/why3/
315
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
316
317
318
319
320
321
	for i in share/images/*.rc; do \
	     d=`basename $$i .rc`; \
	     cp -f $$i $(DATADIR)/why3/images; \
	     mkdir $(DATADIR)/why3/images/$$d; \
	     cp -f share/images/$$d/* $(DATADIR)/why3/images/$$d; \
	done
322
	cp -f share/images/*.png $(DATADIR)/why3/images
323
	cp -f share/why3session.dtd $(DATADIR)/why3
324
	cp -f share/Makefile.config $(DATADIR)/why3
325
326
	cp -f share/vim/why3.vim $(DATADIR)/why3/vim/why3.vim
	cp -f share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
327

MARCHE Claude's avatar
MARCHE Claude committed
328
install_no_local_lib::
329
	mkdir -p $(OCAMLINSTALLLIB)/why3
330
	cp -f $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \
331
		lib/why3/META $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
332

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

MARCHE Claude's avatar
MARCHE Claude committed
342
343
install-all: install install-lib

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
344
345
346
347
348
349
##################
# Uninstallation
##################

uninstall: clean_old_install

350
351
352
353
354
355
356
##################
# Why3 emacs mode
##################

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
357
358
359
360
361
362
363
364
365
366
367
368
369
clean_old_install::
	rm -f $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no)
	rm -f $(DATADIR)/emacs/site-lisp/why3.elc
endif

install_no_local::
	cp -f share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no)
	cp -f share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
endif


370
##################
371
# Why3 plugins
372
373
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
374
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
375
376
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
		plugins/parser/dimacs.ml \
377

378
PLUG_PARSER = genequlin dimacs
379
PLUG_PRINTER =
380
PLUG_TRANSFORM =
381
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
382

383
PLUGINS = genequlin dimacs tptp
384

Andrei Paskevich's avatar
Andrei Paskevich committed
385
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
Andrei Paskevich's avatar
Andrei Paskevich committed
386

Andrei Paskevich's avatar
Andrei Paskevich committed
387
388
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
389

390
391
392
393
394
395
396
397
398
399
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

400
401
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
402
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
403
	      $(TPTPMODULES)
404

Andrei Paskevich's avatar
Andrei Paskevich committed
405
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
406
407
408
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
409
PLUGDIRS = parser printer transform tptp
410
411
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
412
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
413
414
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

415
416
$(PLUGDEP): $(PLUGGENERATED)

417
418
419
420
421
LIBPLUGCMO =  $(addsuffix .cmo,  $(addprefix lib/plugins/, $(PLUGINS)))
LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
422
423

lib/plugins/%.cmxs: plugins/parser/%.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
424
	$(if $(QUIET),@echo 'Linking  $@' &&) \
425
426
427
428
429
430
431
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/parser/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

lib/plugins/%.cmxs: plugins/printer/%.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
432
	$(if $(QUIET),@echo 'Linking  $@' &&) \
433
434
435
436
437
438
439
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/printer/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

lib/plugins/%.cmxs: plugins/transform/%.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
440
	$(if $(QUIET),@echo 'Linking  $@' &&) \
441
442
443
444
445
446
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/transform/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

Andrei Paskevich's avatar
Andrei Paskevich committed
447
lib/plugins/tptp.cmxs: $(TPTPCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
448
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
449
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
450

Andrei Paskevich's avatar
Andrei Paskevich committed
451
lib/plugins/tptp.cmo: $(TPTPCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
452
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
453
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
454

Andrei Paskevich's avatar
Andrei Paskevich committed
455
456
# depend and clean targets

457
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
Andrei Paskevich's avatar
Andrei Paskevich committed
458
459
460
include $(PLUGDEP)
endif

461
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
462

Andrei Paskevich's avatar
Andrei Paskevich committed
463
464
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
GENERATED += $(PLUGGENERATED)
465
466
467

install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
468
	cp -f $(wildcard $(LIBPLUGCMO) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins
469

470
471
472
473
###############
# Why3 commands
###############

Andrei Paskevich's avatar
Andrei Paskevich committed
474
475
476
477
478
TOOLSGENERATED = src/tools/why3wc.ml

TOOLS_BIN = why3config why3execute why3extract why3prove \
	    why3realize why3replay why3wc

Andrei Paskevich's avatar
Andrei Paskevich committed
479
TOOLS_FILES = main $(TOOLS_BIN)
480
481
482
483
484
485
486
487
488
489

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
490
491
$(TOOLSDEP): $(TOOLSGENERATED)

492
493
494
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt:  bin/why3.opt  $(TOOLS_BIN:%=bin/%.opt)

Andrei Paskevich's avatar
Andrei Paskevich committed
495
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
496
497
498
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
499
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
500
501
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
502

503
504
505
506
507
508
509
510
bin/why3config.opt: lib/why3/why3.cmxa src/tools/why3config.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

bin/why3config.byte: lib/why3/why3.cma src/tools/why3config.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
511
bin/why3execute.opt: lib/why3/why3.cmxa src/tools/why3execute.cmx
512
513
514
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
515
bin/why3execute.byte: lib/why3/why3.cma src/tools/why3execute.cmo
516
517
518
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
519
bin/why3extract.opt: lib/why3/why3.cmxa src/tools/why3extract.cmx
520
521
522
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
523
bin/why3extract.byte: lib/why3/why3.cma src/tools/why3extract.cmo
524
525
526
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
527
bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx
528
529
530
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
531
bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo
532
533
534
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
535
bin/why3realize.opt: lib/why3/why3.cmxa src/tools/why3realize.cmx
536
537
538
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
539
bin/why3realize.byte: lib/why3/why3.cma src/tools/why3realize.cmo
540
541
542
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

543
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/why3replay.cmx
544
545
546
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

547
bin/why3replay.byte: lib/why3/why3.cma src/tools/why3replay.cmo
548
549
550
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

Andrei Paskevich's avatar
Andrei Paskevich committed
551
552
553
554
555
556
557
558
bin/why3wc.opt: src/tools/why3wc.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

bin/why3wc.byte: src/tools/why3wc.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
559
clean_old_install::
560
	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
561
	rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
562

563
install_no_local::
564
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
565
	cp -f bin/why3server$(EXE) $(BINDIR)/why3$(EXE)
566
	cp -f bin/why3config.@OCAMLBEST@  $(TOOLDIR)/why3config$(EXE)
567
568
569
	cp -f bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE)
	cp -f bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE)
	cp -f bin/why3prove.@OCAMLBEST@   $(TOOLDIR)/why3prove$(EXE)
570
	cp -f bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
571
	cp -f bin/why3replay.@OCAMLBEST@  $(TOOLDIR)/why3replay$(EXE)
Andrei Paskevich's avatar
Andrei Paskevich committed
572
	cp -f bin/why3wc.@OCAMLBEST@      $(TOOLDIR)/why3wc$(EXE)
573
574

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

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

579
580
581
582
583
584
585
586
587
588
589
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

590
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
591
include $(TOOLSDEP)
592
593
endif

594
depend: $(TOOLSDEP)
595

Andrei Paskevich's avatar
Andrei Paskevich committed
596
597
598
CLEANDIRS += src/tools
GENERATED += $(TOOLSGENERATED)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
599
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
600
	rm -f bin/why3*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
601

602
603
604
##############
# test targets
##############
605

606
607
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
608

609
610
%: %.mlw bin/why3.opt
	bin/why3.opt $*.mlw
611

612
613
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
614

615
616
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
617

618
%.type: %.mlw bin/why3ide.opt
619
	bin/why3.opt --type-only $*.mlw
620

621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
##############
# Why3server #
##############

SERVER_MODULES:= logging arraylist options queue readbuf request writebuf server_main
SERVER_C:= $(addprefix src/tools/, $(addsuffix .c, $(SERVER_MODULES)))
SERVER_H:= $(addprefix src/tools/, $(addsuffix .h, $(SERVER_MODULES)))
SERVER_O:= $(addprefix src/tools/, $(addsuffix .o, $(SERVER_MODULES)))

opt: bin/why3server$(EXE)

bin/why3server$(EXE): $(SERVER_O)
	gcc -o $@ $^

%.o: %.c %.h
	gcc -c -Wall -g -o $@ $<
%.o: %.c
	gcc -c -Wall -g -o $@ $<

src/tools/main.o:: src/tools/server-unix.c src/tools/server-win.c

install_no_local::
	cp -f bin/why3server$(EXE) $(BINDIR)/why3server$(EXE)

clean::
	 rm -f $(SERVER_O)

install_spark2014:
	mkdir -p $(BINDIR)
	mkdir -p $(DATADIR)/why3
	mkdir -p $(DATADIR)/why3/theories
	mkdir -p $(DATADIR)/why3/drivers
	mkdir -p $(DATADIR)/why3/modules
	mkdir -p $(DATADIR)/why3/libs
	cp -f theories/*.why $(DATADIR)/why3/theories
	cp -f modules/*.mlw $(DATADIR)/why3/modules
	cp -f drivers/*.drv drivers/*.gen drivers/*.aux $(DATADIR)/why3/drivers
	cp -f share/why3session.dtd $(DATADIR)/why3
	cp -f bin/why3server$(EXE) $(BINDIR)/why3server$(EXE)
	cp -f bin/gnatwhy3.@OCAMLBEST@ $(BINDIR)/gnatwhy3$(EXE)
	cp -f bin/why3realize.@OCAMLBEST@ $(BINDIR)/why3realize$(EXE)
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -rf lib/coq $(DATADIR)/why3/libs

666
667
668
669
##########
# gallery
##########

670
# we export exactly the programs that have a why3session.xml file
671
672
673

.PHONY: gallery

674
675
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
Andrei Paskevich's avatar
Andrei Paskevich committed
676
	@for x in examples/*/why3session.xml ; do \
677
678
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
679
	  why3 session html $$x; \
680
681
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
682
	  cp examples/$$f.mlw examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
683
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
Andrei Paskevich's avatar
Andrei Paskevich committed
684
	  cd examples/; \
685
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
686
	  cd ..; \
687
	done
688

689
690
691
692
693
.PHONY: gallery-subs

GALLERYSUBS=avl

gallery-subs::
694
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
695
696
697
698
699
700
701
702
703
704
705
	@for d in $(GALLERYSUBS) ; do \
	  echo "exporting examples/$$d"; \
	  rm -f $(GALLERYDIR)/$$d/$$d.zip; \
	  cd examples/$$d; \
	  why3 -L . doc --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
	  cd ..; \
	  zip -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
	  cd ..; \
	done


706
707
708
709
710
%-gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	x=$*/why3session.xml; \
	d=`dirname $$x`; \
	f=`basename $$d`; \
711
	why3 session html $$d; \
712
	rm $$d/*.bak; \
713
714
	echo "exporting $$f"; \
	mkdir -p $(GALLERYDIR)/$$f; \
715
716
	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; \
717
	cp examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
718
719
	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	cd examples/; \
720
	zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
721

MARCHE Claude's avatar
MARCHE Claude committed
722
723
724
725
726
727
728
729
########
# XML DTD validation
########

.PHONY: xml-validate

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

733
734
735
736
737
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
738
739
740
741
###############
# IDE
###############

742
743
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
744
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
745
746
747

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

Andrei Paskevich's avatar
Andrei Paskevich committed
748
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
749
750
751
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

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

755
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
756

757
758
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
759

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

763
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
764
	$(if $(QUIET),@echo 'Linking  $@' &&) \
765
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
MARCHE Claude's avatar
MARCHE Claude committed
766

767
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
768
	$(if $(QUIET),@echo 'Linking  $@' &&) \
769
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
MARCHE Claude's avatar
MARCHE Claude committed
770

771
src/ide/resetgc.o: src/ide/resetgc.c
772
773
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) \
	    $(OCAMLC) -c -ccopt "-Wall -o $@" $<
774

MARCHE Claude's avatar
MARCHE Claude committed
775
776
# depend and clean targets

777
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
Andrei Paskevich's avatar
Andrei Paskevich committed
778
779
include $(IDEDEP)
endif
MARCHE Claude's avatar
MARCHE Claude committed
780

Andrei Paskevich's avatar
Andrei Paskevich committed
781
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
782

Andrei Paskevich's avatar
Andrei Paskevich committed
783
CLEANDIRS += src/ide
MARCHE Claude's avatar
MARCHE Claude committed
784

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
785
786
787
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

788
install_no_local::
789
	cp -f bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
790

791
install_local:: bin/why3ide
792

793
endif
MARCHE Claude's avatar
d    
MARCHE Claude committed
794

795
796
797
798
###############
# Session
###############

Andrei Paskevich's avatar
Andrei Paskevich committed
799
800
801
SESSION_FILES = why3session_lib why3session_copy why3session_info \
		why3session_latex why3session_html why3session_rm \
		why3session_output why3session_run why3session_csv \
802
		why3session_main
803
804
805

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

Andrei Paskevich's avatar
Andrei Paskevich committed
806
SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
807
808
809
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
810
$(SESSIONDEP): DEPFLAGS += -I src/why3session
811
812
813
814
815
816
817
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

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

818
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
819
	$(if $(QUIET),@echo 'Linking  $@' &&) \
820
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
821

822
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
823
	$(if $(QUIET),@echo 'Linking  $@' &&) \
824
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
825
826
827

# depend and clean targets

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

Andrei Paskevich's avatar
Andrei Paskevich committed
832
depend: $(SESSIONDEP)
833

Andrei Paskevich's avatar
Andrei Paskevich committed
834
CLEANDIRS += src/why3session
835

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

839
install_no_local::
840
	cp -f bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
841

842
install_local:: bin/why3session
843

MARCHE Claude's avatar
MARCHE Claude committed
844

845
846
847
##############
# Coq plugin
##############
848

Andrei Paskevich's avatar
Andrei Paskevich committed
849
ifeq (@enable_coq_tactic@,yes)
850

851
COQPGENERATED = src/coq-tactic/why3tac.ml
852

853
COQP_FILES = why3tac
854

855
COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
856

857
858
859
COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
860

861
COQPTREES = kernel interp intf lib library parsing pretyping proofs printing tactics toplevel
862
COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
863

864
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
865
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
Andrei Paskevich's avatar
Andrei Paskevich committed
866
867
$(COQPCMO) $(COQPCMX): BFLAGS += -rectypes
$(COQPCMX): OFLAGS += -rectypes
868

869
$(COQPDEP): $(COQPGENERATED)
870

871
872
byte: src/coq-tactic/.why3-vo-byte
opt:  src/coq-tactic/.why3-vo-opt
873

874
875
876
877
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@)
878
lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cmo,  @MENHIRLIB@)
879

880
lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
881
	$(if $(QUIET),@echo 'Linking  $@' &&) \
882
	    $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
883

884
lib/coq-tactic/why3tac.cma: src/driver/vc_client.o lib/why3/why3.cma $(COQPCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
885
	$(if $(QUIET),@echo 'Linking  $@' &&) \
886
	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
887

888
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
889
	$(if $(QUIET),@echo 'Camlp    $<' &&) \
François Bobot's avatar
François Bobot committed
890
	    $(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
891

892
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
Andrei Paskevich's avatar
Andrei Paskevich committed
893
	$(if $(QUIET),@echo 'Coqc     $<' &&) \
894
	    WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
895
	    touch src/coq-tactic/.why3-vo-byte
896