Makefile.in 66 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
####################################################################
#                                                                  #
#  The Why3 Verification Platform   /   The Why3 Development Team  #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
#  Copyright 2010-2014   --   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
CAMLP5O   = @CAMLP5O@
MARCHE Claude's avatar
MARCHE Claude committed
51
FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
52

53
DEPFLAGS  = -slash -I lib/why3
54
ifeq (@OCAMLBEST@,opt)
Andrei Paskevich's avatar
Andrei Paskevich committed
55
DEPFLAGS += -native
56 57
endif

58
RUBBER = @RUBBER@
59
HEVEA = @HEVEA@
60
HACHA = @HACHA@
61
EMACS = @EMACS@
62

63
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
64
#PDFVIEWER = @PDFVIEWER@
65

66
INCLUDES =
67 68
OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
69 70 71

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

73
ifeq (@enable_profiling@,yes)
74 75 76
OFLAGS += -g -p
endif

77 78
# external libraries common to all binaries

79
EXTOBJS =
80
EXTLIBS = str unix nums dynlink
81 82 83

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
84

85 86
TARGET_EMACS = share/emacs/why3.elc

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87 88 89
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90

91 92 93 94
all: @OCAMLBEST@
plugins: plugins.@OCAMLBEST@
opt: plugins.opt
byte: plugins.byte
Francois Bobot's avatar
Francois Bobot committed
95

96 97 98 99 100
ifeq (@enable_local@,yes)
all: install_local
endif

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

103 104 105
##############
# Why3 library
##############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106

107
LIBGENERATED = src/util/config.ml \
108
	       src/util/rc.ml src/parser/lexer.ml \
109 110
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
111
	       src/driver/driver_lexer.ml src/session/xml.ml \
112
	       lib/ocaml/why3__BigInt_compat.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113

114
LIB_UTIL = config bigInt util opt lists strings extmap extset exthtbl weakhtbl \
115
	   hashcons stdlib exn_printer pp debug loc print_tree \
116
	   cmdline warning sysutil rc plugin bigInt number pqueue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
117

118 119
LIB_CORE = ident ty term pattern decl theory \
	   task pretty dterm env trans printer
120

121
LIB_PARSER = ptree glob parser typing lexer
122

123
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
124
	     whyconf autodetection
125

126
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
127
		eliminate_definition eliminate_algebraic \
128
		eliminate_inductive eliminate_let eliminate_if \
129 130 131 132
		libencoding discriminate encoding encoding_select \
		encoding_guards_full encoding_tags_full \
		encoding_guards encoding_tags encoding_twin \
		encoding_sort simplify_array filter_trigger \
133
		introduction abstraction close_epsilon lift_epsilon \
134
		eliminate_epsilon \
135
		eval_match instantiate_predicate smoke_detector
136

137
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
138
	      simplify gappa cvc3 yices mathematica
139

François Bobot's avatar
François Bobot committed
140 141
LIB_SESSION = xml termcode session session_tools session_scheduler

142
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
143
	    mlw_dexpr mlw_typing mlw_driver mlw_ocaml \
144
	    mlw_main mlw_interp
145 146

LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
147 148 149 150
	      $(addprefix src/core/, $(LIB_CORE)) \
	      $(addprefix src/parser/, $(LIB_PARSER)) \
	      $(addprefix src/driver/, $(LIB_DRIVER)) \
	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
François Bobot's avatar
François Bobot committed
151
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
152 153
	      $(addprefix src/session/, $(LIB_SESSION)) \
	      $(addprefix src/whyml/, $(LIB_WHYML))
154

155
LIBDIRS = util core parser driver transform printer session whyml
156
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
157

Andrei Paskevich's avatar
Andrei Paskevich committed
158
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
159 160
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
161

Andrei Paskevich's avatar
Andrei Paskevich committed
162
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
163
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
164
$(LIBCMX): OFLAGS += -for-pack Why3
165

166 167
$(LIBDEP): $(LIBGENERATED)

168 169 170 171
# Zarith

ifeq (@enable_zarith@,yes)

172
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
173
	cp lib/ocaml/why3__BigInt_zarith.ml $@
174 175 176

else

177
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
178
	cp lib/ocaml/why3__BigInt_num.ml $@
179 180 181

endif

182
clean::
183
	rm -f lib/ocaml/why3__BigInt_compat.ml
184

185
# build targets
186

187 188
byte: lib/why3/why3.cma
opt:  lib/why3/why3.cmxa
189

190
lib/why3/why3.cma: lib/why3/why3.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
191 192
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
193

194
lib/why3/why3.cmxa: lib/why3/why3.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
195 196
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) -a $(OFLAGS) -o $@ $^
197

198
lib/why3/why3.cmo: $(LIBCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
199 200
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
201

202
lib/why3/why3.cmx: $(LIBCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
203 204
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
205

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

Andrei Paskevich's avatar
Andrei Paskevich committed
208 209 210
ifneq "$(MAKECMDGOALS)" "clean"
include $(LIBDEP)
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
211

212
depend: $(LIBDEP)
213

Andrei Paskevich's avatar
Andrei Paskevich committed
214
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
215 216
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
217 218
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
219
	   $(addsuffix /*.dep, $(LIBSDIRS)) \
220 221 222 223 224
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
225
	rm -f lib/why3/why3.cm* lib/why3/why3.[ao]
226

227 228 229
###############
# installation
###############
230

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
231 232
clean_old_install::
	rm -rf $(LIBDIR)/why3
MARCHE Claude's avatar
MARCHE Claude committed
233
	rm -rf $(DATADIR)/why3
234
	rm -rf $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
235

236

237
ifeq ($(EMACS),no)
238
install_no_local:: clean_old_install
239 240 241
else
install_no_local:: clean_old_install $(TARGET_EMACS)
endif
242
	mkdir -p $(BINDIR)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
243
	mkdir -p $(LIBDIR)/why3
244
	mkdir -p $(TOOLDIR)
245
	mkdir -p $(DATADIR)/why3
246
	mkdir -p $(DATADIR)/why3/images
247 248
	mkdir -p $(DATADIR)/why3/images/boomy
	mkdir -p $(DATADIR)/why3/images/fatcow
MARCHE Claude's avatar
MARCHE Claude committed
249
	mkdir -p $(DATADIR)/why3/emacs
250
	mkdir -p $(DATADIR)/why3/vim
251
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
252
	mkdir -p $(DATADIR)/why3/theories
253
	mkdir -p $(DATADIR)/why3/modules/mach
MARCHE Claude's avatar
MARCHE Claude committed
254
	mkdir -p $(DATADIR)/why3/drivers
255
	mkdir -p $(DATADIR)/emacs/site-lisp/
MARCHE Claude's avatar
MARCHE Claude committed
256
	cp -f theories/*.why $(DATADIR)/why3/theories
257
	cp -f modules/*.mlw $(DATADIR)/why3/modules
258
	cp -f modules/mach/*.mlw $(DATADIR)/why3/modules/mach
Andrei Paskevich's avatar
Andrei Paskevich committed
259
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
260
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
261
	cp -f share/images/icons.rc $(DATADIR)/why3/images
262
	cp -f share/images/*.png $(DATADIR)/why3/images
263 264
	cp -f share/images/boomy/*.png $(DATADIR)/why3/images/boomy
	cp -f share/images/fatcow/*.png $(DATADIR)/why3/images/fatcow
265
	cp -f share/why3session.dtd $(DATADIR)/why3
266
	cp -rf share/javascript $(DATADIR)/why3/javascript
267 268
	cp -f share/vim/why3.vim $(DATADIR)/why3/vim/why3.vim
	cp -f share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
269

MARCHE Claude's avatar
MARCHE Claude committed
270
install_no_local_lib::
271
	mkdir -p $(OCAMLINSTALLLIB)/why3
Andrei Paskevich's avatar
Andrei Paskevich committed
272
	cp -f lib/why3/why3.cm* lib/why3/why3.[ao] \
273
		lib/why3/META $(OCAMLINSTALLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
274

275 276
ifeq (@enable_local@,yes)
install install-lib:
277 278
	@echo "Why3 is configured in local installation mode."
	@echo "To install Why3, run ./configure --disable-local ; make ; make install"
279
else
MARCHE Claude's avatar
MARCHE Claude committed
280
install: clean_old_install install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
281
install-lib: install_no_local_lib
282 283
endif

MARCHE Claude's avatar
MARCHE Claude committed
284 285
install-all: install install-lib

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
286 287 288 289 290 291
##################
# Uninstallation
##################

uninstall: clean_old_install

292 293 294 295 296 297 298
##################
# Why3 emacs mode
##################

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
299 300 301 302 303 304 305 306 307 308 309 310 311
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


312
##################
313
# Why3 plugins
314 315
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
316
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
317 318
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
		plugins/parser/dimacs.ml \
319

320
PLUG_PARSER = genequlin dimacs
321
PLUG_PRINTER =
322
PLUG_TRANSFORM =
323
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
324

325
PLUGINS = genequlin dimacs tptp
326

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

Andrei Paskevich's avatar
Andrei Paskevich committed
329 330
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
331

332 333 334 335 336 337 338 339 340 341
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

342 343
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
344
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
345
	      $(TPTPMODULES)
346

Andrei Paskevich's avatar
Andrei Paskevich committed
347
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
348 349 350
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
351
PLUGDIRS = parser printer transform tptp
352 353
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
354
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
355 356
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

357 358
$(PLUGDEP): $(PLUGGENERATED)

359 360 361 362 363
LIBPLUGCMO =  $(addsuffix .cmo,  $(addprefix lib/plugins/, $(PLUGINS)))
LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
364 365

lib/plugins/%.cmxs: plugins/parser/%.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
366
	$(if $(QUIET),@echo 'Linking  $@' &&) \
367 368 369 370 371 372 373
	    $(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
374
	$(if $(QUIET),@echo 'Linking  $@' &&) \
375 376 377 378 379 380 381
	    $(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
382
	$(if $(QUIET),@echo 'Linking  $@' &&) \
383 384 385 386 387 388
	    $(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
389
lib/plugins/tptp.cmxs: $(TPTPCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
390
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
391
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
392

Andrei Paskevich's avatar
Andrei Paskevich committed
393
lib/plugins/tptp.cmo: $(TPTPCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
394
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
395
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
396 397 398 399 400 401

PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
	    $(addsuffix /*.annot, $(PLUGSDIRS)) \
	    $(addsuffix /*.output, $(PLUGSDIRS)) \
	    $(addsuffix /*.automaton, $(PLUGSDIRS)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
402
	    $(addsuffix /*.dep, $(PLUGSDIRS)) \
403 404 405
	    $(addsuffix /*.o, $(PLUGSDIRS)) \
	    $(addsuffix /*~, $(PLUGSDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
406 407 408 409 410 411
# depend and clean targets

ifneq "$(MAKECMDGOALS)" "clean"
include $(PLUGDEP)
endif

412
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
413

414 415 416 417 418 419
clean::
	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
	rm -f lib/plugins/*

install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
420
	cp -f $(foreach f,$(LIBPLUGCMO) $(LIBPLUGCMXS),$(wildcard $(f))) $(LIBDIR)/why3/plugins
421

422 423 424
######
# Why3
######
425

426 427
src/tools/main.cmo: lib/why3/why3.cma
src/tools/main.cmx: lib/why3/why3.cmxa
428

429 430
src/tools/why3contraption.cmo: lib/why3/why3.cma
src/tools/why3contraption.cmx: lib/why3/why3.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
431

432 433
byte: bin/why3.byte bin/why3contraption.byte
opt:  bin/why3.opt  bin/why3contraption.opt
434 435

bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
436
	$(if $(QUIET),@echo 'Linking  $@' &&) \
437
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438

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

443 444
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
445

446 447 448 449 450 451 452 453 454 455 456
bin/why3contraption.opt: lib/why3/why3.cmxa src/tools/why3contraption.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

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

bin/why3contraption: bin/why3contraption.@OCAMLBEST@
	ln -sf why3contraption.@OCAMLBEST@ $@

457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498
clean_old_install::
	rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE)

install_no_local::
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
	cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE)

install_local: bin/why3 bin/why3contraption bin/why3prove

ifneq "$(MAKECMDGOALS)" "clean"
include src/tools/main.dep
include src/tools/why3contraption.dep
include src/tools/why3prove.dep
endif

depend: src/tools/main.dep src/tools/why3contraption.dep

clean::
	rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
	rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep
	rm -f bin/why3.byte bin/why3.opt bin/why3
	rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption

###############
# Why3 commands
###############

TOOLS_FILES = args why3prove

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

byte: bin/why3prove.byte
opt:  bin/why3prove.opt

bin/why3prove.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3prove.cmx
499 500 501
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

502
bin/why3prove.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3prove.cmo
503 504 505 506 507 508
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

bin/why3prove: bin/why3prove.@OCAMLBEST@
	ln -sf why3prove.@OCAMLBEST@ $@

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
509
clean_old_install::
510
	rm -f $(TOOLDIR)/why3prove$(EXE)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
511

512
install_no_local::
513
	cp -f bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
514

515
install_local: bin/why3prove
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
516

517
ifneq "$(MAKECMDGOALS)" "clean"
518
include $(TOOLSDEP)
519 520
endif

521
depend: $(TOOLSDEP)
522

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
523
clean::
524
	rm -f src/tools/args.cm[iox] src/tools/args.annot src/tools/args.o src/tools/args.dep
525 526
	rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
	rm -f bin/why3prove.byte bin/why3prove.opt bin/why3prove
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
527

528 529 530
##############
# test targets
##############
531

532 533
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
534

535 536
%: %.mlw bin/why3.opt
	bin/why3.opt $*.mlw
537

538 539
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
540

541 542
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
543

544
%.type: %.mlw bin/why3ide.opt
545
	bin/why3.opt --type-only $*.mlw
546

547 548 549 550
##########
# gallery
##########

551
# we export exactly the programs that have a why3session.xml file
552 553 554

.PHONY: gallery

555 556
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
Andrei Paskevich's avatar
Andrei Paskevich committed
557
	@for x in examples/*/why3session.xml ; do \
558 559
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
560
	  why3session html $$x; \
561 562
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
563
	  cp examples/$$f.mlw examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
564
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
Andrei Paskevich's avatar
Andrei Paskevich committed
565
	  cd examples/; \
566
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
567
	  cd ..; \
568
	done
569

570 571 572 573 574 575 576 577
%-gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	x=$*/why3session.xml; \
	d=`dirname $$x`; \
	f=`basename $$d`; \
	why3session html $$x; \
	echo "exporting $$f"; \
	mkdir -p $(GALLERYDIR)/$$f; \
578 579
	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; \
580
	cp examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
581 582
	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	cd examples/; \
583
	zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
584

MARCHE Claude's avatar
MARCHE Claude committed
585 586 587 588 589 590 591 592
########
# XML DTD validation
########

.PHONY: xml-validate

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

596 597 598 599 600
xml-validate-local:
	@for x in `find examples/ -name why3session.xml`; do \
	  xmllint --noout --dtdvalid share/why3session.dtd $$x 2>&1 | head -1; \
	done

601 602 603 604
########
# Config
########

605
CONFIG_FILES = why3config
606

607
CONFIGMODULES = $(addprefix src/why3config/, $(CONFIG_FILES))
608

Andrei Paskevich's avatar
Andrei Paskevich committed
609
CONFIGDEP = $(addsuffix .dep, $(CONFIGMODULES))
610 611 612 613 614
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

# build targets

615 616
byte: bin/why3config.byte
opt:  bin/why3config.opt
617

618
bin/why3config.opt: lib/why3/why3.cmxa $(CONFIGCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
619
	$(if $(QUIET),@echo 'Linking  $@' &&) \
620
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
621

622
bin/why3config.byte: lib/why3/why3.cma $(CONFIGCMO)
623
	$(if $(QUIET),@echo 'Linking  $@' &&) \
624
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
625

626 627 628
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

629 630
# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
631 632 633
ifneq "$(MAKECMDGOALS)" "clean"
include $(CONFIGDEP)
endif
634

Andrei Paskevich's avatar
Andrei Paskevich committed
635
depend: $(CONFIGDEP)
636 637

clean::
638 639 640
	rm -f src/why3config/*.cm[iox] src/why3config/*.o
	rm -f src/why3config/*.annot src/why3config/*.dep src/why3config/*~
	rm -f src/why3config/*.output src/why3config/*.automaton
641
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
642

643 644
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
645
		--detect --conf_file why3.conf
646

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
647 648 649
clean_old_install::
	rm -f $(BINDIR)/why3config$(EXE)

650
install_no_local::
651
	cp -f bin/why3config.@OCAMLBEST@ $(TOOLDIR)/why3config$(EXE)
652

653
install_local: bin/why3config
654

MARCHE Claude's avatar
MARCHE Claude committed
655 656 657 658
###############
# IDE
###############

659 660
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
661
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
662 663 664

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

Andrei Paskevich's avatar
Andrei Paskevich committed
665
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
666 667 668
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

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

672
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
673

674 675
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
676

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

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

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

688 689 690
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

691
src/ide/resetgc.o: src/ide/resetgc.c
692
	$(OCAMLC) -c -ccopt "-Wall -o $@" $<
693

MARCHE Claude's avatar
MARCHE Claude committed
694 695
# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
696 697 698
ifneq "$(MAKECMDGOALS)" "clean"
include $(IDEDEP)
endif
MARCHE Claude's avatar
MARCHE Claude committed
699

Andrei Paskevich's avatar
Andrei Paskevich committed
700
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
701 702

clean::
703
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
704
	rm -f src/ide/*.cm[iox] src/ide/*.o
Andrei Paskevich's avatar
Andrei Paskevich committed
705
	rm -f src/ide/*.annot src/ide/*.dep src/ide/*~
706
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
707

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
708 709 710
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

711
install_no_local::
712
	cp -f bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
713 714

install_local: bin/why3ide
715

716
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
717

718

MARCHE Claude's avatar
MARCHE Claude committed
719 720 721 722
###############
# Replayer
###############

François Bobot's avatar
François Bobot committed
723
REPLAYER_FILES = replay
MARCHE Claude's avatar
MARCHE Claude committed
724

725
REPLAYERMODULES = $(addprefix src/why3replayer/, $(REPLAYER_FILES))
MARCHE Claude's avatar
MARCHE Claude committed
726

Andrei Paskevich's avatar
Andrei Paskevich committed
727
REPLAYERDEP = $(addsuffix .dep, $(REPLAYERMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
728 729 730
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))

731 732
$(REPLAYERDEP): DEPFLAGS += -I src/why3replayer
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/why3replayer
MARCHE Claude's avatar
MARCHE Claude committed
733 734 735 736 737 738

# build targets

byte: bin/why3replayer.byte
opt:  bin/why3replayer.opt

739
bin/why3replayer.opt: lib/why3/why3.cmxa $(REPLAYERCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
740
	$(if $(QUIET),@echo 'Linking  $@' &&) \
741
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
MARCHE Claude's avatar
MARCHE Claude committed
742

743
bin/why3replayer.byte: lib/why3/why3.cma $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
744
	$(if $(QUIET),@echo 'Linking  $@' &&) \
745
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
MARCHE Claude's avatar
MARCHE Claude committed
746 747 748 749 750 751

bin/why3replayer: bin/why3replayer.@OCAMLBEST@
	ln -sf why3replayer.@OCAMLBEST@ $@

# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
752 753 754
ifneq "$(MAKECMDGOALS)" "clean"
include $(REPLAYERDEP)
endif
MARCHE Claude's avatar
MARCHE Claude committed
755

Andrei Paskevich's avatar
Andrei Paskevich committed
756
depend: $(REPLAYERDEP)
MARCHE Claude's avatar
MARCHE Claude committed
757 758

clean::
759 760
	rm -f src/why3replayer/*.cm[iox] src/why3replayer/*.o
	rm -f src/why3replayer/*.annot src/why3replayer/*.dep src/why3replayer/*~
MARCHE Claude's avatar
MARCHE Claude committed
761 762
	rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
763 764 765
clean_old_install::
	rm -f $(BINDIR)/why3replayer$(EXE)

MARCHE Claude's avatar
MARCHE Claude committed
766
install_no_local::
767
	cp -f bin/why3replayer.@OCAMLBEST@ $(TOOLDIR)/why3replayer$(EXE)
MARCHE Claude's avatar
MARCHE Claude committed
768 769 770

install_local: bin/why3replayer

771 772 773 774 775

###############
# Session
###############

776 777
SESSION_FILES = why3session_lib why3session_copy why3session_info	\
		why3session_latex why3session_html why3session_rm	\
778 779
		why3session_output why3session_run why3session_csv	\
		why3session
780 781 782

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

Andrei Paskevich's avatar
Andrei Paskevich committed
783
SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
784 785 786
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
787
$(SESSIONDEP): DEPFLAGS += -I src/why3session
788 789 790 791 792 793 794
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

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

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

799
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
800
	$(if $(QUIET),@echo 'Linking  $@' &&) \
801
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
802 803 804 805 806 807

bin/why3session: bin/why3session.@OCAMLBEST@
	ln -sf why3session.@OCAMLBEST@ $@

# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
808 809 810
ifneq "$(MAKECMDGOALS)" "clean"
include $(SESSIONDEP)
endif
811

Andrei Paskevich's avatar
Andrei Paskevich committed
812
depend: $(SESSIONDEP)
813 814

clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
815 816
	rm -f src/why3session/*.cm[iox] src/why3session/*.o
	rm -f src/why3session/*.annot src/why3session/*.dep src/why3session/*~
817 818
	rm -f bin/why3session.byte bin/why3session.opt bin/why3session

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
819 820 821
clean_old_install::
	rm -f $(BINDIR)/why3session$(EXE)

822
install_no_local::
823
	cp -f bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
824 825 826

install_local: bin/why3session

MARCHE Claude's avatar
MARCHE Claude committed
827

828
###############
829
# Bench
830 831
###############

832 833
ifeq (@enable_bench@,yes)

834
BENCH_FILES = worker db bench benchrc benchdb why3bench
835

836
BENCHMODULES := $(addprefix src/why3bench/, $(BENCH_FILES))
837

Andrei Paskevich's avatar
Andrei Paskevich committed
838
BENCHDEP = $(addsuffix .dep, $(BENCHMODULES))
839 840 841
BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))

842 843
$(BENCHDEP): DEPFLAGS += -I src/why3bench
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/why3bench -I @SQLITE3LIB@
844 845 846

# build targets

847 848
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
849

Andrei Paskevich's avatar
Andrei Paskevich committed
850
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
851
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
852

853
bin/why3bench.opt: lib/why3/why3.cmxa $(BENCHCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
854
	$(if $(QUIET),@echo 'Linking  $@' &&) \
855
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
856