Makefile.in 66.3 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

239
240
241
242
243
# hide deprecated warnings for strings

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

244
# build targets
245

246
247
byte: lib/why3/why3.cma
opt:  lib/why3/why3.cmxa
248

249
lib/why3/why3.cma: lib/why3/why3.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
250
251
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
252

253
lib/why3/why3.cmxa: lib/why3/why3.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
254
255
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) -a $(OFLAGS) -o $@ $^
256

257
lib/why3/why3.cmo: $(LIBCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
258
259
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
260

261
lib/why3/why3.cmx: $(LIBCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
262
263
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
264

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

267
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
268
include $(LIBDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
269
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
270

271
depend: $(LIBDEP)
272

Andrei Paskevich's avatar
Andrei Paskevich committed
273
274
275
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
CLEANLIBS += lib/why3/why3session lib/why3/why3
GENERATED += $(LIBGENERATED)
276

277
278
279
###############
# installation
###############
280

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
281
282
clean_old_install::
	rm -rf $(LIBDIR)/why3
MARCHE Claude's avatar
MARCHE Claude committed
283
	rm -rf $(DATADIR)/why3
284
	rm -rf $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
285

286

287
ifeq ($(EMACS),no)
288
install_no_local:: clean_old_install
289
290
291
else
install_no_local:: clean_old_install $(TARGET_EMACS)
endif
292
	mkdir -p $(BINDIR)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
293
	mkdir -p $(LIBDIR)/why3
294
	mkdir -p $(TOOLDIR)
295
	mkdir -p $(DATADIR)/why3
296
	mkdir -p $(DATADIR)/why3/images
297
	mkdir -p $(DATADIR)/why3/vim
298
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
299
	mkdir -p $(DATADIR)/why3/theories
300
	mkdir -p $(DATADIR)/why3/modules/mach
MARCHE Claude's avatar
MARCHE Claude committed
301
	mkdir -p $(DATADIR)/why3/drivers
302
	mkdir -p $(DATADIR)/emacs/site-lisp/
MARCHE Claude's avatar
MARCHE Claude committed
303
	cp -f theories/*.why $(DATADIR)/why3/theories
304
	cp -f modules/*.mlw $(DATADIR)/why3/modules
305
	cp -f modules/mach/*.mlw $(DATADIR)/why3/modules/mach
Andrei Paskevich's avatar
Andrei Paskevich committed
306
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
MARCHE Claude's avatar
MARCHE Claude committed
307
	cp -f LICENSE $(DATADIR)/why3/
308
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
309
310
311
312
313
314
	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
315
	cp -f share/images/*.png $(DATADIR)/why3/images
316
	cp -f share/why3session.dtd $(DATADIR)/why3
317
	cp -f share/Makefile.config $(DATADIR)/why3
318
319
	cp -f share/vim/why3.vim $(DATADIR)/why3/vim/why3.vim
	cp -f share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
320

MARCHE Claude's avatar
MARCHE Claude committed
321
install_no_local_lib::
322
	mkdir -p $(OCAMLINSTALLLIB)/why3
323
	cp -f $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \
324
		lib/why3/META $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
325

326
327
ifeq (@enable_local@,yes)
install install-lib:
328
329
	@echo "Why3 is configured in local installation mode."
	@echo "To install Why3, run ./configure --disable-local ; make ; make install"
330
else
MARCHE Claude's avatar
MARCHE Claude committed
331
install: clean_old_install install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
332
install-lib: install_no_local_lib
333
334
endif

MARCHE Claude's avatar
MARCHE Claude committed
335
336
install-all: install install-lib

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
337
338
339
340
341
342
##################
# Uninstallation
##################

uninstall: clean_old_install

343
344
345
346
347
348
349
##################
# Why3 emacs mode
##################

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
350
351
352
353
354
355
356
357
358
359
360
361
362
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


363
##################
364
# Why3 plugins
365
366
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
367
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
368
369
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
		plugins/parser/dimacs.ml \
370

371
PLUG_PARSER = genequlin dimacs
372
PLUG_PRINTER =
373
PLUG_TRANSFORM =
374
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
375

376
PLUGINS = genequlin dimacs tptp
377

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

Andrei Paskevich's avatar
Andrei Paskevich committed
380
381
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
382

383
384
385
386
387
388
389
390
391
392
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

393
394
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
395
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
396
	      $(TPTPMODULES)
397

Andrei Paskevich's avatar
Andrei Paskevich committed
398
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
399
400
401
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
402
PLUGDIRS = parser printer transform tptp
403
404
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
405
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
406
407
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

408
409
$(PLUGDEP): $(PLUGGENERATED)

410
411
412
413
414
LIBPLUGCMO =  $(addsuffix .cmo,  $(addprefix lib/plugins/, $(PLUGINS)))
LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
415
416

lib/plugins/%.cmxs: plugins/parser/%.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
417
	$(if $(QUIET),@echo 'Linking  $@' &&) \
418
419
420
421
422
423
424
	    $(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
425
	$(if $(QUIET),@echo 'Linking  $@' &&) \
426
427
428
429
430
431
432
	    $(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
433
	$(if $(QUIET),@echo 'Linking  $@' &&) \
434
435
436
437
438
439
	    $(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
440
lib/plugins/tptp.cmxs: $(TPTPCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
441
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
442
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
443

Andrei Paskevich's avatar
Andrei Paskevich committed
444
lib/plugins/tptp.cmo: $(TPTPCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
445
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
446
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
447

Andrei Paskevich's avatar
Andrei Paskevich committed
448
449
# depend and clean targets

450
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
Andrei Paskevich's avatar
Andrei Paskevich committed
451
452
453
include $(PLUGDEP)
endif

454
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
455

Andrei Paskevich's avatar
Andrei Paskevich committed
456
457
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
GENERATED += $(PLUGGENERATED)
458
459
460

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

463
464
465
466
###############
# Why3 commands
###############

Andrei Paskevich's avatar
Andrei Paskevich committed
467
468
469
470
471
TOOLSGENERATED = src/tools/why3wc.ml

TOOLS_BIN = why3config why3execute why3extract why3prove \
	    why3realize why3replay why3wc

Andrei Paskevich's avatar
Andrei Paskevich committed
472
TOOLS_FILES = main $(TOOLS_BIN)
473
474
475
476
477
478
479
480
481
482

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
483
484
$(TOOLSDEP): $(TOOLSGENERATED)

485
486
487
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt:  bin/why3.opt  $(TOOLS_BIN:%=bin/%.opt)

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

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

496
497
498
499
500
501
502
503
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
504
bin/why3execute.opt: lib/why3/why3.cmxa src/tools/why3execute.cmx
505
506
507
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

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

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

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

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

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

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

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

536
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/why3replay.cmx
537
538
539
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

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

Andrei Paskevich's avatar
Andrei Paskevich committed
544
545
546
547
548
549
550
551
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
552
clean_old_install::
553
	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
554
	rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
555

556
install_no_local::
557
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
558
	cp -f bin/why3server$(EXE) $(BINDIR)/why3$(EXE)
559
	cp -f bin/why3config.@OCAMLBEST@  $(TOOLDIR)/why3config$(EXE)
560
561
562
	cp -f bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE)
	cp -f bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE)
	cp -f bin/why3prove.@OCAMLBEST@   $(TOOLDIR)/why3prove$(EXE)
563
	cp -f bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
564
	cp -f bin/why3replay.@OCAMLBEST@  $(TOOLDIR)/why3replay$(EXE)
Andrei Paskevich's avatar
Andrei Paskevich committed
565
	cp -f bin/why3wc.@OCAMLBEST@      $(TOOLDIR)/why3wc$(EXE)
566
567

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

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

572
573
574
575
576
577
578
579
580
581
582
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

583
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
584
include $(TOOLSDEP)
585
586
endif

587
depend: $(TOOLSDEP)
588

Andrei Paskevich's avatar
Andrei Paskevich committed
589
590
591
CLEANDIRS += src/tools
GENERATED += $(TOOLSGENERATED)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
592
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
593
	rm -f bin/why3*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
594

595
596
597
##############
# test targets
##############
598

599
600
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
601

602
603
%: %.mlw bin/why3.opt
	bin/why3.opt $*.mlw
604

605
606
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
607

608
609
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
610

611
%.type: %.mlw bin/why3ide.opt
612
	bin/why3.opt --type-only $*.mlw
613

614
615
616
617
618
619
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
##############
# 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

659
660
661
662
##########
# gallery
##########

663
# we export exactly the programs that have a why3session.xml file
664
665
666

.PHONY: gallery

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

682
683
684
685
686
.PHONY: gallery-subs

GALLERYSUBS=avl

gallery-subs::
687
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
688
689
690
691
692
693
694
695
696
697
698
	@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


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

MARCHE Claude's avatar
MARCHE Claude committed
715
716
717
718
719
720
721
722
########
# XML DTD validation
########

.PHONY: xml-validate

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

726
727
728
729
730
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
731
732
733
734
###############
# IDE
###############

735
736
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
737
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
738
739
740

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

Andrei Paskevich's avatar
Andrei Paskevich committed
741
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
742
743
744
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

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

748
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
749

750
751
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
752

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

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

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

764
src/ide/resetgc.o: src/ide/resetgc.c
765
766
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) \
	    $(OCAMLC) -c -ccopt "-Wall -o $@" $<
767

MARCHE Claude's avatar
MARCHE Claude committed
768
769
# depend and clean targets

770
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
Andrei Paskevich's avatar
Andrei Paskevich committed
771
772
include $(IDEDEP)
endif
MARCHE Claude's avatar
MARCHE Claude committed
773

Andrei Paskevich's avatar
Andrei Paskevich committed
774
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
775

Andrei Paskevich's avatar
Andrei Paskevich committed
776
CLEANDIRS += src/ide
MARCHE Claude's avatar
MARCHE Claude committed
777

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
778
779
780
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

781
install_no_local::
782
	cp -f bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
783

784
install_local:: bin/why3ide
785

786
endif
MARCHE Claude's avatar
d    
MARCHE Claude committed
787

788
789
790
791
###############
# Session
###############

Andrei Paskevich's avatar
Andrei Paskevich committed
792
793
794
SESSION_FILES = why3session_lib why3session_copy why3session_info \
		why3session_latex why3session_html why3session_rm \
		why3session_output why3session_run why3session_csv \
795
		why3session_main
796
797
798

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

Andrei Paskevich's avatar
Andrei Paskevich committed
799
SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
800
801
802
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
803
$(SESSIONDEP): DEPFLAGS += -I src/why3session
804
805
806
807
808
809
810
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

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

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

815
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
816
	$(if $(QUIET),@echo 'Linking  $@' &&) \
817
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
818
819
820

# depend and clean targets

821
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
Andrei Paskevich's avatar
Andrei Paskevich committed
822
823
include $(SESSIONDEP)
endif
824

Andrei Paskevich's avatar
Andrei Paskevich committed
825
depend: $(SESSIONDEP)
826

Andrei Paskevich's avatar
Andrei Paskevich committed
827
CLEANDIRS += src/why3session
828

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
829
830
831
clean_old_install::
	rm -f $(BINDIR)/why3session$(EXE)

832
install_no_local::
833
	cp -f bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
834

835
install_local:: bin/why3session
836

MARCHE Claude's avatar
MARCHE Claude committed
837

838
839
840
##############
# Coq plugin
##############
841

Andrei Paskevich's avatar
Andrei Paskevich committed
842
ifeq (@enable_coq_tactic@,yes)
843

844
COQPGENERATED = src/coq-tactic/why3tac.ml
845

846
COQP_FILES = why3tac
847

848
COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
849

850
851
852
COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
853

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

857
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
858
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
Andrei Paskevich's avatar
Andrei Paskevich committed
859
860
$(COQPCMO) $(COQPCMX): BFLAGS += -rectypes
$(COQPCMX): OFLAGS += -rectypes
861

862
$(COQPDEP): $(COQPGENERATED)
863

864
865
byte: src/coq-tactic/.why3-vo-byte
opt:  src/coq-tactic/.why3-vo-opt
866

867
868
869
870
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@)
871
lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cmo,  @MENHIRLIB@)
872

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

877
lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
878
	$(if $(QUIET),@echo 'Linking  $@' &&) \
879
	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
880

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

885
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
886
	$(if $(QUIET),@echo 'Coqc     $<' &&) \
887
	    WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
888
	    touch src/coq-tactic/.why3-vo-byte
889

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