Makefile.in 37.9 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
3
#  Copyright (C) 2010-2011                                               #
4 5 6
#    François Bobot                                                      #
#    Jean-Christophe Filliâtre                                           #
#    Claude Marché                                                       #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
#    Andrei Paskevich                                                    #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8 9 10
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
11
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12 13 14 15 16 17 18 19
#  described in file LICENSE.                                            #
#                                                                        #
#  This software is distributed in the hope that it will be useful,      #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
#                                                                        #
##########################################################################

Andrei Paskevich's avatar
Andrei Paskevich committed
20
include Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

22 23 24 25 26 27
VERBOSEMAKE ?= @enable_verbose_make@

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

30
# install the binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31
DESTDIR =
32

33
prefix	    = @prefix@
34 35 36 37 38
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
39
DATADIR = $(DESTDIR)@datarootdir@
40
MANDIR  = $(DESTDIR)@mandir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
41

Andrei Paskevich's avatar
Andrei Paskevich committed
42
# OS specific stuff
43 44
EXE   = @EXE@
STRIP = @STRIP@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45 46

# other variables
47
CC        = @CC@
48 49 50 51 52 53 54 55 56
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
57 58
COQC      = @COQC@
COQDEP    = @COQDEP@
59 60
CAMLP5O   = @CAMLP5O@

61
ifeq (@enable_menhirlib@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
62 63
  MENHIR    = @MENHIR@ --table
  MENHIRINC = -I @MENHIRLIB@
64 65
  MENHIRLIB = menhirLib
else
Andrei Paskevich's avatar
Andrei Paskevich committed
66
  MENHIR    = @MENHIR@
67 68 69 70
  MENHIRINC =
  MENHIRLIB =
endif

71 72
RUBBER = @RUBBER@

73
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
74
#PDFVIEWER = @PDFVIEWER@
75

76 77
BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aer-29 -dtypes    -I src $(INCLUDES)
78

79
ifeq (@enable_profiling@,yes)
80 81 82 83
OFLAGS += -g -p
STRIP = true
endif

84 85
# external libraries common to all binaries

86
EXTOBJS =
Andrei Paskevich's avatar
Andrei Paskevich committed
87
EXTLIBS = str unix nums dynlink
88 89 90

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
91

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92 93 94
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95

96
all: @OCAMLBEST@ plugins
Francois Bobot's avatar
Francois Bobot committed
97

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

102 103
plugins: plugins.@OCAMLBEST@

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
#############
108
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
110

111
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
112 113
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
114
	       src/driver/driver_lexer.ml src/coq_config.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
115

116
LIB_UTIL = stdlib exn_printer pp debug loc print_tree print_number \
117
	   cmdline hashweak hashcons util sysutil rc plugin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
118

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

121
LIB_PARSER = ptree denv typing parser lexer
122

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

126
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
127
		inlining split_goal \
128
		eliminate_definition eliminate_algebraic \
129
		eliminate_inductive eliminate_let eliminate_if \
130 131
		libencoding discriminate protect_enumeration \
		encoding encoding_select \
132
		encoding_decorate encoding_twin \
François Bobot's avatar
François Bobot committed
133
		encoding_explicit encoding_guard encoding_sort \
134
		encoding_instantiate simplify_array filter_trigger \
135
		introduction abstraction close_epsilon lift_epsilon \
136
		eval_match instantiate_predicate smoke_detector
137

138
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
139
	      cvc3 yices
140

141
LIBMODULES = src/config src/coq_config \
142 143 144 145 146
	      $(addprefix src/util/, $(LIB_UTIL)) \
	      $(addprefix src/core/, $(LIB_CORE)) \
	      $(addprefix src/parser/, $(LIB_PARSER)) \
	      $(addprefix src/driver/, $(LIB_DRIVER)) \
	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
147
	      $(addprefix src/printer/, $(LIB_PRINTER))
148

149
LIBDIRS = util core parser driver transform printer
150
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
151

152
ifeq (@enable_hypothesis_selection@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
153 154 155
  LIB_TRANSFORM += hypothesis_selection
  INCLUDES += -I @OCAMLGRAPHLIB@
  EXTLIBS += graph
156 157
endif

158 159 160 161
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
162

163
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
164
$(LIBCMX): OFLAGS += -for-pack Why3
165

166
# build targets
167

168 169
byte: src/why3.cma
opt:  src/why3.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
170

171
src/why3.cma: src/why3.cmo
172 173
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

174
src/why3.cmxa: src/why3.cmx
175 176
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

177
src/why3.cmo: $(LIBCMO)
178
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
179

180
src/why3.cmx: $(LIBCMX)
181 182 183
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
184

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
185 186
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
187
.depend.lib: src/config.ml $(LIBGENERATED)
188
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190 191

depend: .depend.lib

192 193
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
194
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
195 196
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
197 198
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
199 200 201 202 203
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
204
	rm -f src/why3.cm[aiox] src/why3.[ao] src/why3.cmxa
205
	rm -f .depend.lib
206

207 208 209
###############
# installation
###############
210

211
install_no_local::
212 213
	mkdir -p $(BINDIR)
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
214
	mkdir -p $(DATADIR)/why3/emacs
215
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
216
	mkdir -p $(DATADIR)/why3/theories
217
	mkdir -p $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
218 219
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
220
	cp -f modules/*.mlw $(DATADIR)/why3/modules
Andrei Paskevich's avatar
Andrei Paskevich committed
221
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
222 223
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
224
	cp -rf share/javascript $(DATADIR)/why3/javascript
MARCHE Claude's avatar
MARCHE Claude committed
225
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
226 227
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

MARCHE Claude's avatar
MARCHE Claude committed
228 229
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
230
	cp -f src/why3.cm* $(OCAMLLIB)/why3
231
	cp -f META $(OCAMLLIB)/why3
232
	if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
233

234 235 236 237 238
ifeq (@enable_local@,yes)
install install-lib:
	@echo "Why is configured in local installation mode."
	@echo "To install Why, run ./configure --disable-local ; make ; make install"
else
239
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
240
install-lib: install_no_local_lib
241 242
endif

MARCHE Claude's avatar
MARCHE Claude committed
243 244
install-all: install install-lib

245 246 247 248 249 250 251
##################
# Why plugins
##################

PLUGGENERATED =

PLUG_PARSER = genequlin
252
PLUG_PRINTER = tptpfof
253 254
PLUG_TRANSFORM =

255
PLUGINS = genequlin tptpfof
256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322

PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGMLI = $(addsuffix .mli, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

PLUGDIRS = parser printer transform
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

plugins.byte: $(addsuffix .cmo, $(addprefix lib/plugins/, $(PLUGINS)))
plugins.opt : $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

lib/plugins/%.cmxs: plugins/parser/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

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

lib/plugins/%.cmxs: plugins/printer/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

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

lib/plugins/%.cmxs: plugins/transform/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

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

include .depend.plugins

.depend.plugins: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I plugins $(PLUGINCLUDES) \
		$(PLUGML) $(PLUGMLI) > $@

depend: .depend.plugins

PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
	    $(addsuffix /*.annot, $(PLUGSDIRS)) \
	    $(addsuffix /*.output, $(PLUGSDIRS)) \
	    $(addsuffix /*.automaton, $(PLUGSDIRS)) \
	    $(addsuffix /*.o, $(PLUGSDIRS)) \
	    $(addsuffix /*~, $(PLUGSDIRS))

clean::
	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
	rm -f lib/plugins/*
	rm -f .depend.plugins

install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
	cp -f lib/plugins/* $(LIBDIR)/why3/plugins

323

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324
##################
325
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326 327
##################

328 329
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330

331
bin/why3.opt: src/why3.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
332 333
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334 335
	$(STRIP) $@

336
bin/why3.byte: src/why3.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
337 338
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
339

340 341 342
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

343 344
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
345

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
347
	rm -f src/main.cm[iox] src/main.annot src/main.o
348
	rm -f bin/why3.byte bin/why3.opt bin/why3
349

350
install_no_local::
351
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
352 353

install_local: bin/why3
354

355 356 357
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
358

359
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
360
	    pgm_module pgm_wp pgm_env pgm_typing pgm_ocaml pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
361

362
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
363

364 365 366 367 368
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

369
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
370 371

# build targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
372

373 374
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
375

376
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
377 378
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
379 380
	$(STRIP) $@

381
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
382 383 384
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

385 386 387
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

388
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389 390

include .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391

392
.depend.programs:
393
	$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
394

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
395 396 397
depend: .depend.programs

clean::
398 399
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
400
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
401
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402

403 404
# test target

405 406
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
407

408 409
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
410

411 412
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
413

414 415
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
416

417 418 419
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

420
install_no_local::
421
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml$(EXE)
422

423
install_local: bin/why3ml
424

425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459
########
# Whyml (new API)
########

MLW_FILES = mlw_ty

MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))

MLWML  = $(addsuffix .ml,  $(MLWMODULES))
MLWMLI = $(addsuffix .mli, $(MLWMODULES))
MLWCMO = $(addsuffix .cmo, $(MLWMODULES))
MLWCMX = $(addsuffix .cmx, $(MLWMODULES))

$(MLWCMO) $(MLWCMX): INCLUDES += -I src/whyml

# build targets

byte: $(MLWCMX)
opt:  $(MLWCMO)

# depend and clean targets

include .depend.whyml

.depend.whyml:
	$(OCAMLDEP) -slash -I src -I src/whyml $(MLWML) $(MLWMLI) > $@

depend: .depend.whyml

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

460 461 462 463
##########
# gallery
##########

464
# we export exactly the programs that have a why3session.xml file
465 466 467

.PHONY: gallery

468 469
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
470 471 472
	@for x in `find examples/programs/ -name why3session.xml`; do \
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
473 474 475
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
476 477 478 479
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	  cd examples/programs/; \
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
	  cd ../..; \
480
	done
481

482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498
########
# Config
########

CONFIG_FILES = whyconfig

CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))

CONFIGML  = $(addsuffix .ml,  $(CONFIGMODULES))
CONFIGMLI = $(addsuffix .mli, $(CONFIGMODULES))
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

$(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs

# build targets

499 500
byte: bin/why3config.byte
opt:  bin/why3config.opt
501

502
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
503 504 505 506
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

507
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
508 509 510
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

511 512 513
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

514 515 516 517 518 519 520 521 522 523 524 525 526
# depend and clean targets

include .depend.config

.depend.config: $(CONFIGGENERATED)
	$(OCAMLDEP) -slash -I src -I src/config $(CONFIGML) $(CONFIGMLI) > $@

depend: .depend.config

clean::
	rm -f src/config/*.cm[iox] src/config/*.o
	rm -f src/config/*.annot src/config/*~
	rm -f src/config/*.output src/config/*.automaton
527
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
528 529
	rm -f .depend.config

530 531
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
532
		--detect --conf_file why.conf
533

534
install_no_local::
535
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
536

537
install_local: bin/why3config
538

MARCHE Claude's avatar
MARCHE Claude committed
539 540 541 542
###############
# IDE
###############

543 544
ifeq (@enable_ide@,yes)

545
IDE_FILES = xml termcode session gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
546 547 548 549 550 551 552 553

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

IDEML  = $(addsuffix .ml,  $(IDEMODULES))
IDEMLI = $(addsuffix .mli, $(IDEMODULES))
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

554
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
555

556
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
557

558 559
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
560

561
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
562
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
563
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
564

565
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
566
	$(if $(QUIET), @echo 'Linking  $@' &&) \
567
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
568 569
	$(STRIP) $@

570
bin/why3ide.byte: src/why3.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
571
	$(if $(QUIET),@echo 'Linking  $@' &&) \
572
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
573

574 575 576
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
577 578 579 580
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
581
.depend.ide: src/ide/xml.ml
582
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
583 584 585 586

depend: .depend.ide

clean::
587
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
588 589
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
590
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
591 592
	rm -f .depend.ide

593
install_no_local::
594
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE)
595 596

install_local: bin/why3ide
597

598
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
599

600

MARCHE Claude's avatar
MARCHE Claude committed
601 602 603 604
###############
# Replayer
###############

MARCHE Claude's avatar
MARCHE Claude committed
605
REPLAYER_FILES = xml termcode session replay
MARCHE Claude's avatar
MARCHE Claude committed
606 607 608 609 610 611 612 613

REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES))

REPLAYERML  = $(addsuffix .ml,  $(REPLAYERMODULES))
REPLAYERMLI = $(addsuffix .mli, $(REPLAYERMODULES))
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
614
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
615 616 617 618 619 620

# build targets

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

621
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
622 623 624 625
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

626
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

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

# depend and clean targets

include .depend.replayer

.depend.replayer: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@

depend: .depend.replayer

clean::
643
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
644 645 646 647 648 649
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
	rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
	rm -f .depend.replayer

install_no_local::
650
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
MARCHE Claude's avatar
MARCHE Claude committed
651 652 653

install_local: bin/why3replayer

654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703
###############
# Stats
###############

STATS_FILES = xml termcode session session_ro stats

STATSMODULES = $(addprefix src/ide/, $(STATS_FILES))

STATSML  = $(addsuffix .ml,  $(STATSMODULES))
STATSMLI = $(addsuffix .mli, $(STATSMODULES))
STATSCMO = $(addsuffix .cmo, $(STATSMODULES))
STATSCMX = $(addsuffix .cmx, $(STATSMODULES))

$(STATSCMO) $(STATSCMX): INCLUDES += -I src/ide

# build targets

byte: bin/why3stats.byte
opt:  bin/why3stats.opt

bin/why3stats.opt: src/why3.cmxa $(PGMCMX) $(STATSCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why3stats.byte: src/why3.cma $(PGMCMO) $(STATSCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

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

# depend and clean targets

include .depend.stats

.depend.stats: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(STATSML) $(STATSMLI) > $@

depend: .depend.stats

clean::
	rm -f bin/why3stats.byte bin/why3stats.opt bin/why3stats
	rm -f .depend.stats

install_no_local::
	cp -f bin/why3stats.@OCAMLBEST@ $(BINDIR)/why3stats

install_local: bin/why3stats

704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753
###############
# Html
###############

HTML_FILES = xml termcode session session_ro html_session

HTMLMODULES = $(addprefix src/ide/, $(HTML_FILES))

HTMLML  = $(addsuffix .ml,  $(HTMLMODULES))
HTMLMLI = $(addsuffix .mli, $(HTMLMODULES))
HTMLCMO = $(addsuffix .cmo, $(HTMLMODULES))
HTMLCMX = $(addsuffix .cmx, $(HTMLMODULES))

$(HTMLCMO) $(HTMLCMX): INCLUDES += -I src/ide

# build targets

byte: bin/why3html.byte
opt:  bin/why3html.opt

bin/why3html.opt: src/why3.cmxa $(PGMCMX) $(HTMLCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why3html.byte: src/why3.cma $(PGMCMO) $(HTMLCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

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

# depend and clean targets

include .depend.html

.depend.html: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(HTMLML) $(HTMLMLI) > $@

depend: .depend.html

clean::
	rm -f bin/why3html.byte bin/why3html.opt bin/why3html
	rm -f .depend.html

install_no_local::
	cp -f bin/why3html.@OCAMLBEST@ $(BINDIR)/why3html

install_local: bin/why3html

MARCHE Claude's avatar
MARCHE Claude committed
754

755
###############
756
# Bench
757 758
###############

759 760
ifeq (@enable_bench@,yes)

761
BENCH_FILES = worker db bench benchrc benchdb whybench
762 763 764 765 766 767 768 769

BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))

BENCHML  = $(addsuffix .ml,  $(BENCHMODULES))
BENCHMLI = $(addsuffix .mli, $(BENCHMODULES))
BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))

770
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/bench -I @SQLITE3LIB@
771 772 773

# build targets

774 775
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
776

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

780
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
781 782 783 784
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

785
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
786 787 788
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

789 790 791
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

792 793 794 795 796 797 798 799 800 801 802 803
# depend and clean targets

include .depend.bench

.depend.bench:
	$(OCAMLDEP) -slash -I src -I src/bench -I src/ide $(BENCHML) $(BENCHMLI) > $@

depend: .depend.bench

clean::
	rm -f src/bench/*.cm[iox] src/bench/*.o
	rm -f src/bench/*.annot src/bench/*~
804
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
805 806 807
	rm -f .depend.bench

install_no_local::
808
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
809 810

install_local: bin/why3bench
811

812 813
endif

814 815 816
##############
# Coq plugin
##############
817

818
ifeq (@enable_coq_plugin@,yes)
819

820 821 822 823 824 825 826 827 828 829 830 831 832
COQGENERATED = src/coq-plugin/g_whytac.ml

COQ_FILES = whytac g_whytac

COQMODULES = $(addprefix src/coq-plugin/, $(COQ_FILES))

COQML  = $(addsuffix .ml,  $(COQMODULES))
COQCMO = $(addsuffix .cmo, $(COQMODULES))
COQCMX = $(addsuffix .cmx, $(COQMODULES))

COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
COQINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQTREES))

833
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
834

835 836
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
837

838 839
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
840

841
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
842 843
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

844
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
845 846
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

847 848 849 850
src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
	$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@

# depend and clean targets
Andrei Paskevich's avatar
Andrei Paskevich committed
851

852
include .depend.coq-plugin
853

854
.depend.coq-plugin: $(COQGENERATED)
855 856
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

857
depend: .depend.coq-plugin
858 859 860 861 862 863

clean::
	rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
	rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
	rm -f src/coq-plugin/*.annot src/coq-plugin/*~
	rm -f $(COQGENERATED)
864 865 866 867 868 869 870 871 872 873
	rm -f .depend.coq-plugin

endif

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

ifeq (@enable_coq_libs@,yes)

874
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
875 876
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))

877
COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
878 879
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))

880 881 882 883 884
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding Single Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
885 886

COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
887 888 889 890 891 892 893

COQV  = $(addsuffix .v,  $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))

%.vo: %.v
	$(COQC) -R lib/coq Why3 $<

894 895 896 897 898 899 900 901 902
src/coq_config.ml:
	echo "let realized_theories = [" > $@
	for f in $(COQLIBS_INT_FILES); do echo '  ["int"; "'"$$f"'"];'; done >> $@
	for f in $(COQLIBS_REAL_FILES); do echo '  ["real"; "'"$$f"'"];'; done >> $@
ifeq (@enable_coq_fp_libs@,yes)
	for f in $(COQLIBS_FP_FILES); do echo '  ["floating_point"; "'"$$f"'"];'; done >> $@
endif
	echo "]" >> $@

903 904 905 906
all: $(COQVO)

install_no_local::
	mkdir -p $(LIBDIR)/why3/coq
907 908
	mkdir -p $(LIBDIR)/why3/coq/int
	cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
909
	mkdir -p $(LIBDIR)/why3/coq/real
910
	cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
911 912
ifeq (@enable_coq_fp_libs@,yes)
	mkdir -p $(LIBDIR)/why3/coq/floating_point
913
	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
914
endif
915 916 917 918 919 920 921 922 923 924 925

install_local: $(COQVO)

include .depend.coq-libs

.depend.coq-libs:
	$(COQDEP) -slash -R lib/coq Why3 $(COQV) > $@

depend: .depend.coq-libs

clean::
926
	rm -f $(COQVO) $(addsuffix .glob, $(COQLIBS_FILES))
927
	rm -f .depend.coq-libs
928

929 930 931 932 933
else

src/coq_config.ml:
	echo "let realized_theories = []" > $@

934
endif
935

936 937 938
########
# Tptp2why
########
939

940
ifeq (@enable_whytptp@,yes)
941

942 943
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
944

François Bobot's avatar
François Bobot committed
945
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
946

947
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
948 949 950 951 952 953

TPTPML  = $(addsuffix .ml,  $(TPTPMODULES))
TPTPMLI = $(addsuffix .mli, $(TPTPMODULES))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))

954 955
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
956 957 958

# build targets

Andrei Paskevich's avatar
Andrei Paskevich committed
959 960
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt  opt : lib/plugins/whytptp.cmxs
961

Andrei Paskevich's avatar
Andrei Paskevich committed
962 963
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
964

Andrei Paskevich's avatar
Andrei Paskevich committed
965
lib/plugins/whytptp.cmxs: $(TPTPCMX)
966
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
967
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
968

Andrei Paskevich's avatar
Andrei Paskevich committed
969
lib/plugins/whytptp.cmo: $(TPTPCMO)
970
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
971 972
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
973
install_no_local::
Andrei Paskevich's avatar
Andrei Paskevich committed
974
	cp -f lib/plugins/whytptp.cm* $(LIBDIR)/why3/plugins/
François Bobot's avatar
François Bobot committed
975

976 977 978 979 980 981 982 983 984 985 986
# depend and clean targets

include .depend.tptp2why

.depend.tptp2why: $(TPTPGENERATED)
	$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@

depend: .depend.tptp2why

clean::
	rm -f $(TPTPGENERATED)
987
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
988
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
989
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
Andrei Paskevich's avatar
Andrei Paskevich committed
990
	rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
991 992
	rm -f .depend.tptp2why

993
endif
994

995 996 997 998
#######
# tools
#######

999
TOOLS = bin/why3-cpulimit$(EXE)
1000 1001 1002

byte opt: $(TOOLS)

1003
bin/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
1004
	$(CC) -Wall -o $@ $^
1005 1006

clean::
1007
	rm -f bin/why3-cpulimit$(EXE) src/tools/*~
1008

1009
install_no_local::
1010
	cp -f bin/why3-cpulimit$(EXE) $(BINDIR)/why3-cpulimit$(EXE)
1011

1012 1013 1014 1015
#########
# why3doc
#########

1016 1017
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032

WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))

WHY3DOCML  = $(addsuffix .ml,  $(WHY3DOCMODULES))
WHY3DOCMLI = $(addsuffix .mli, $(WHY3DOCMODULES))
WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))

$(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc

# build targets

byte: bin/why3doc.byte
opt:  bin/why3doc.opt

1033
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
1034 1035 1036 1037
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

1038
bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
1039 1040 1041
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

1042 1043 1044
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

1045
install_no_local::
1046
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc$(EXE)