Makefile.in 71.5 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 = @ZIPINCLUDE@
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 @ZIPLIB@
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 112 113
	       src/driver/driver_lexer.ml \
               src/session/compress.ml src/session/xml.ml \
	       lib/ocaml/why3__BigInt_compat.ml 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114

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

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

123
LIB_PARSER = ptree glob parser typing lexer
124

125
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
126
	     whyconf autodetection
127

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

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

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
	      $(addprefix src/whyml/, $(LIB_WHYML))
153

154 155 156 157 158
LIB_SESSION = compress xml termcode session session_tools session_scheduler

LIBSESSIONMODULES = $(addprefix src/session/, $(LIB_SESSION)) 
	      
LIBDIRS = util core parser driver transform printer whyml
159
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
160

161 162 163
LIBSESSIONDIRS = session 
LIBSESSIONINCLUDES = $(addprefix -I src/, $(LIBSESSIONDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
164
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
165 166
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
167

168 169 170 171
LIBSESSIONDEP = $(addsuffix .dep, $(LIBSESSIONMODULES))
LIBSESSIONCMO = $(addsuffix .cmo, $(LIBSESSIONMODULES))
LIBSESSIONCMX = $(addsuffix .cmx, $(LIBSESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
172
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
173
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
174
$(LIBCMX): OFLAGS += -for-pack Why3
175

176 177 178 179
$(LIBSESSIONDEP): DEPFLAGS += $(LIBSESSIONINCLUDES)
$(LIBSESSIONCMO) $(LIBSESSIONCMX): INCLUDES += $(LIBSESSIONINCLUDES)
$(LIBSESSIONCMX): OFLAGS += -for-pack Why3session

180
$(LIBDEP): $(LIBGENERATED)
181
$(LIBSESSIONDEP): $(LIBGENERATED)
182

183 184 185 186
# Zarith

ifeq (@enable_zarith@,yes)

187
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
188
	cp lib/ocaml/why3__BigInt_zarith.ml $@
189 190 191

else

192
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
193
	cp lib/ocaml/why3__BigInt_num.ml $@
194 195 196

endif

197
clean::
198
	rm -f lib/ocaml/why3__BigInt_compat.ml
199

200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
# 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

clean::
	rm -f src/session/compress.ml

217
# build targets
218

219 220
byte: lib/why3/why3.cma
opt:  lib/why3/why3.cmxa
221

222
lib/why3/why3.cma: lib/why3/why3.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
223 224
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
225

226
lib/why3/why3.cmxa: lib/why3/why3.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
227 228
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) -a $(OFLAGS) -o $@ $^
229

230
lib/why3/why3.cmo: $(LIBCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
231 232
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
233

234
lib/why3/why3.cmx: $(LIBCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
235 236
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
237

238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256
byte: lib/why3/why3session.cma
opt:  lib/why3/why3session.cmxa

lib/why3/why3session.cma: lib/why3/why3session.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) -a $(BFLAGS) -o $@ $^

lib/why3/why3session.cmxa: lib/why3/why3session.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) -a $(OFLAGS) -o $@ $^

lib/why3/why3session.cmo: $(LIBSESSIONCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

lib/why3/why3session.cmx: $(LIBSESSIONCMX)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

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

Andrei Paskevich's avatar
Andrei Paskevich committed
259
ifneq "$(MAKECMDGOALS)" "clean"
260
include $(LIBDEP) $(LIBSESSIONDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
261
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
262

263
depend: $(LIBDEP) $(LIBSESSIONDEP)
264

Andrei Paskevich's avatar
Andrei Paskevich committed
265
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
266 267
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
268 269
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
270
	   $(addsuffix /*.dep, $(LIBSDIRS)) \
271 272 273 274 275
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

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

278 279 280
###############
# installation
###############
281

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

287

288
ifeq ($(EMACS),no)
289
install_no_local:: clean_old_install
290 291 292
else
install_no_local:: clean_old_install $(TARGET_EMACS)
endif
293
	mkdir -p $(BINDIR)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
294
	mkdir -p $(LIBDIR)/why3
295
	mkdir -p $(TOOLDIR)
296
	mkdir -p $(DATADIR)/why3
297
	mkdir -p $(DATADIR)/why3/images
298 299
	mkdir -p $(DATADIR)/why3/images/boomy
	mkdir -p $(DATADIR)/why3/images/fatcow
MARCHE Claude's avatar
MARCHE Claude committed
300
	mkdir -p $(DATADIR)/why3/emacs
301
	mkdir -p $(DATADIR)/why3/vim
302
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
303
	mkdir -p $(DATADIR)/why3/theories
304
	mkdir -p $(DATADIR)/why3/modules/mach
MARCHE Claude's avatar
MARCHE Claude committed
305
	mkdir -p $(DATADIR)/why3/drivers
306
	mkdir -p $(DATADIR)/emacs/site-lisp/
MARCHE Claude's avatar
MARCHE Claude committed
307
	cp -f theories/*.why $(DATADIR)/why3/theories
308
	cp -f modules/*.mlw $(DATADIR)/why3/modules
309
	cp -f modules/mach/*.mlw $(DATADIR)/why3/modules/mach
Andrei Paskevich's avatar
Andrei Paskevich committed
310
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
311
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
312
	cp -f share/images/icons.rc $(DATADIR)/why3/images
313
	cp -f share/images/*.png $(DATADIR)/why3/images
314 315
	cp -f share/images/boomy/*.png $(DATADIR)/why3/images/boomy
	cp -f share/images/fatcow/*.png $(DATADIR)/why3/images/fatcow
316
	cp -f share/why3session.dtd $(DATADIR)/why3
317
	cp -rf share/javascript $(DATADIR)/why3/javascript
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
Andrei Paskevich's avatar
Andrei Paskevich committed
323
	cp -f lib/why3/why3.cm* lib/why3/why3.[ao] \
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 448 449 450 451 452

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
453
	    $(addsuffix /*.dep, $(PLUGSDIRS)) \
454 455 456
	    $(addsuffix /*.o, $(PLUGSDIRS)) \
	    $(addsuffix /*~, $(PLUGSDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
457 458 459 460 461 462
# depend and clean targets

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

463
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
464

465 466 467 468 469 470
clean::
	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
	rm -f lib/plugins/*

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

473 474 475
######
# Why3
######
476

477 478
src/tools/main.cmo: lib/why3/why3.cma
src/tools/main.cmx: lib/why3/why3.cmxa
479

480 481
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
482

483 484
byte: bin/why3.byte bin/why3contraption.byte
opt:  bin/why3.opt  bin/why3contraption.opt
485 486

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

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

494 495
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
496

497 498 499 500 501 502 503 504 505 506 507
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@ $@

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
508
clean_old_install::
509
	rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE)
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
510

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

Guillaume Melquiond's avatar
Guillaume Melquiond committed
515
install_local:: bin/why3 bin/why3contraption
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
516

517
ifneq "$(MAKECMDGOALS)" "clean"
518 519 520
include src/tools/main.dep
include src/tools/why3contraption.dep
include src/tools/why3prove.dep
521 522
endif

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525
clean::
526 527
	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
528
	rm -f bin/why3.byte bin/why3.opt bin/why3
529 530 531 532 533 534
	rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption

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

535
TOOLS_BIN = why3execute why3extract why3prove why3realize why3replay
536
TOOLS_FILES = args $(TOOLS_BIN)
537 538 539 540 541 542 543 544 545 546

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

547 548 549 550 551 552 553 554 555 556 557 558 559
byte: $(TOOLS_BIN:%=bin/%.byte)
opt:  $(TOOLS_BIN:%=bin/%.opt)

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

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

bin/why3execute: bin/why3execute.@OCAMLBEST@
	ln -sf why3execute.@OCAMLBEST@ $@
560 561 562 563 564 565 566 567 568 569 570

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

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

bin/why3extract: bin/why3extract.@OCAMLBEST@
	ln -sf why3extract.@OCAMLBEST@ $@
571 572

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

576
bin/why3prove.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3prove.cmo
577 578 579 580 581 582
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

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

583 584 585 586 587 588 589 590 591 592 593
bin/why3realize.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3realize.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

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

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

594 595 596 597 598 599 600 601 602 603 604
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3replay.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

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

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

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
605
clean_old_install::
606
	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE))
Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
607

608
install_no_local::
609 610 611
	cp -f bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE)
	cp -f bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE)
	cp -f bin/why3prove.@OCAMLBEST@   $(TOOLDIR)/why3prove$(EXE)
612
	cp -f bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
613
	cp -f bin/why3replay.@OCAMLBEST@ $(TOOLDIR)/why3replay$(EXE)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
614

Guillaume Melquiond's avatar
Guillaume Melquiond committed
615
install_local:: $(addprefix bin/,$(TOOLS_BIN))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
616

617
ifneq "$(MAKECMDGOALS)" "clean"
618
include $(TOOLSDEP)
619 620
endif

621
depend: $(TOOLSDEP)
622

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
623
clean::
624
	rm -f src/tools/args.cm[iox] src/tools/args.annot src/tools/args.o src/tools/args.dep
625
	rm -f src/tools/why3execute.cm[iox] src/tools/why3execute.annot src/tools/why3execute.o src/tools/why3execute.dep
626
	rm -f src/tools/why3extract.cm[iox] src/tools/why3extract.annot src/tools/why3extract.o src/tools/why3extract.dep
627
	rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
628
	rm -f src/tools/why3realize.cm[iox] src/tools/why3realize.annot src/tools/why3realize.o src/tools/why3realize.dep
629
	rm -f src/tools/why3replay.cm[iox] src/tools/why3replay.annot src/tools/why3replay.o src/tools/why3replay.dep
630
	rm -f bin/why3execute.byte bin/why3execute.opt bin/why3execute
631
	rm -f bin/why3extract.byte bin/why3extract.opt bin/why3extract
632
	rm -f bin/why3prove.byte bin/why3prove.opt bin/why3prove
633
	rm -f bin/why3realize.byte bin/why3realize.opt bin/why3realize
634
	rm -f bin/why3replay.byte bin/why3replay.opt bin/why3replay
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
635

636 637 638
##############
# test targets
##############
639

640 641
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
642

643 644
%: %.mlw bin/why3.opt
	bin/why3.opt $*.mlw
645

646 647
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
648

649 650
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
651

652
%.type: %.mlw bin/why3ide.opt
653
	bin/why3.opt --type-only $*.mlw
654

655 656 657 658
##########
# gallery
##########

659
# we export exactly the programs that have a why3session.xml file
660 661 662

.PHONY: gallery

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

678 679 680 681 682 683 684 685
%-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; \
686 687
	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; \
688
	cp examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
689 690
	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	cd examples/; \
691
	zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
692

MARCHE Claude's avatar
MARCHE Claude committed
693 694 695 696 697 698 699 700
########
# XML DTD validation
########

.PHONY: xml-validate

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

704 705 706 707 708
xml-validate-local:
	@for x in `find examples/ -name why3session.xml`; do \
	  xmllint --noout --dtdvalid share/why3session.dtd $$x 2>&1 | head -1; \
	done

709 710 711 712
########
# Config
########

713
CONFIG_FILES = why3config
714

715
CONFIGMODULES = $(addprefix src/why3config/, $(CONFIG_FILES))
716

Andrei Paskevich's avatar
Andrei Paskevich committed
717
CONFIGDEP = $(addsuffix .dep, $(CONFIGMODULES))
718 719 720 721 722
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

# build targets

723 724
byte: bin/why3config.byte
opt:  bin/why3config.opt
725

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

730
bin/why3config.byte: lib/why3/why3.cma $(CONFIGCMO)
731
	$(if $(QUIET),@echo 'Linking  $@' &&) \
732
	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
733

734 735 736
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

737 738
# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
739 740 741
ifneq "$(MAKECMDGOALS)" "clean"
include $(CONFIGDEP)
endif
742

Andrei Paskevich's avatar
Andrei Paskevich committed
743
depend: $(CONFIGDEP)
744 745

clean::
746 747 748
	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
749
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
750

751 752
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
753
		--detect --conf_file why3.conf
754

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
755 756 757
clean_old_install::
	rm -f $(BINDIR)/why3config$(EXE)

758
install_no_local::
759
	cp -f bin/why3config.@OCAMLBEST@ $(TOOLDIR)/why3config$(EXE)
760

761
install_local:: bin/why3config
762

MARCHE Claude's avatar
MARCHE Claude committed
763 764 765 766
###############
# IDE
###############

767 768
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
769
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
770 771 772

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

Andrei Paskevich's avatar
Andrei Paskevich committed
773
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
774 775 776
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

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

780
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
781

782 783
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
784

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

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

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

796 797 798
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

799
src/ide/resetgc.o: src/ide/resetgc.c
800
	$(OCAMLC) -c -ccopt "-Wall -o $@" $<
801

MARCHE Claude's avatar
MARCHE Claude committed
802 803
# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
804 805 806
ifneq "$(MAKECMDGOALS)" "clean"
include $(IDEDEP)
endif
MARCHE Claude's avatar
MARCHE Claude committed
807

Andrei Paskevich's avatar
Andrei Paskevich committed
808
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
809 810

clean::
811
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
812
	rm -f src/ide/*.cm[iox] src/ide/*.o
Andrei Paskevich's avatar
Andrei Paskevich committed
813
	rm -f src/ide/*.annot src/ide/*.dep src/ide/*~
814
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
815

Jacques-Pascal Deplaix's avatar
Jacques-Pascal Deplaix committed
816 817 818
clean_old_install::
	rm -f $(BINDIR)/why3ide$(EXE)

819
install_no_local::
820
	cp -f bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
821

822
install_local:: bin/why3ide
823

824
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
825

826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882
# <<<<<<< HEAD
# =======

# ###############
# # Replayer
# ###############

# REPLAYER_FILES = replay

# REPLAYERMODULES = $(addprefix src/why3replayer/, $(REPLAYER_FILES))

# REPLAYERDEP = $(addsuffix .dep, $(REPLAYERMODULES))
# REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
# REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))

# $(REPLAYERDEP): DEPFLAGS += -I src/why3replayer
# $(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/why3replayer

# # build targets

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

# bin/why3replayer.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa $(REPLAYERCMX)
# 	$(if $(QUIET),@echo 'Linking  $@' &&) \
# 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^

# bin/why3replayer.byte: lib/why3/why3.cma lib/why3/why3session.cma $(REPLAYERCMO)
# 	$(if $(QUIET),@echo 'Linking  $@' &&) \
# 	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^

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

# # depend and clean targets

# ifneq "$(MAKECMDGOALS)" "clean"
# include $(REPLAYERDEP)
# endif

# depend: $(REPLAYERDEP)

# clean::
# 	rm -f src/why3replayer/*.cm[iox] src/why3replayer/*.o
# 	rm -f src/why3replayer/*.annot src/why3replayer/*.dep src/why3replayer/*~
# 	rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer

# clean_old_install::
# 	rm -f $(BINDIR)/why3replayer$(EXE)

# install_no_local::
# 	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)

# i