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 \
François Bobot's avatar
François Bobot committed
114 115
	       src/driver/driver_lexer.ml src/coq_config.ml \
               src/session/xml.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116

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

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

122
LIB_PARSER = ptree denv typing parser lexer
123

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

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

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

François Bobot's avatar
François Bobot committed
142 143
LIB_SESSION = xml termcode session session_tools session_scheduler

144
LIBMODULES = src/config src/coq_config \
145 146 147 148 149
	      $(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)) \
François Bobot's avatar
François Bobot committed
150 151
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
	      $(addprefix src/session/, $(LIB_SESSION))
152

François Bobot's avatar
François Bobot committed
153
LIBDIRS = util core parser driver transform printer session
154
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
155

156
ifeq (@enable_hypothesis_selection@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
157 158 159
  LIB_TRANSFORM += hypothesis_selection
  INCLUDES += -I @OCAMLGRAPHLIB@
  EXTLIBS += graph
160 161
endif

162 163 164 165
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
166

167
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
168
$(LIBCMX): OFLAGS += -for-pack Why3
169

170
# build targets
171

172 173
byte: src/why3.cma
opt:  src/why3.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174

175
src/why3.cma: src/why3.cmo
176 177
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

178
src/why3.cmxa: src/why3.cmx
179 180
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

181
src/why3.cmo: $(LIBCMO)
182
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
183

184
src/why3.cmx: $(LIBCMX)
185 186 187
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
188

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190
include .depend.lib

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

depend: .depend.lib

196 197
# clean target

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

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
208
	rm -f src/why3.cm[aiox] src/why3.[ao] src/why3.cmxa
209
	rm -f .depend.lib
210

211 212 213
###############
# installation
###############
214

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

MARCHE Claude's avatar
MARCHE Claude committed
232 233
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
234
	cp -f src/why3.cm* $(OCAMLLIB)/why3
235
	cp -f META $(OCAMLLIB)/why3
236
	if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
237
	if test -f src/why3.o; then cp -f src/why3.o $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
238

239 240 241 242 243
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
244
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
245
install-lib: install_no_local_lib
246 247
endif

MARCHE Claude's avatar
MARCHE Claude committed
248 249
install-all: install install-lib

250 251 252 253 254 255 256
##################
# Why plugins
##################

PLUGGENERATED =

PLUG_PARSER = genequlin
257
PLUG_PRINTER = tptpfof
258 259
PLUG_TRANSFORM =

260
PLUGINS = genequlin tptpfof
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 323 324 325 326 327

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

328

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
329
##################
330
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331 332
##################

333 334
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335

336
bin/why3.opt: src/why3.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
337 338
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
339 340
	$(STRIP) $@

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

345 346 347
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

348 349
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
350

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
351
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
352
	rm -f src/main.cm[iox] src/main.annot src/main.o
353
	rm -f bin/why3.byte bin/why3.opt bin/why3
354

355
install_no_local::
356
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
357 358

install_local: bin/why3
359

360 361 362
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
363

364
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
365
	    pgm_module pgm_wp pgm_env pgm_typing pgm_ocaml pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
366

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

369 370 371 372 373
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

374
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
375 376

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

378 379
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
380

381
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
382 383
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
384 385
	$(STRIP) $@

386
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
387 388 389
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

390 391 392
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

393
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
394 395

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400 401 402
depend: .depend.programs

clean::
403 404
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
405
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
406
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407

408 409
# test target

410 411
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
412

413 414
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
415

416 417
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
418

419 420
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
421

422 423 424
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

425
install_no_local::
426
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml$(EXE)
427

428
install_local: bin/why3ml
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 460 461 462 463 464
########
# 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

465 466 467 468
##########
# gallery
##########

469
# we export exactly the programs that have a why3session.xml file
470 471 472

.PHONY: gallery

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

487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503
########
# 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

504 505
byte: bin/why3config.byte
opt:  bin/why3config.opt
506

507
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
508 509 510 511
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

512
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
513 514 515
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

516 517 518
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

519 520 521 522 523 524 525 526 527 528 529 530 531
# 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
532
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
533 534
	rm -f .depend.config

535 536
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
537
		--detect --conf_file why.conf
538

539
install_no_local::
540
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
541

542
install_local: bin/why3config
543

MARCHE Claude's avatar
MARCHE Claude committed
544 545 546 547
###############
# IDE
###############

548 549
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
550
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
551 552 553 554 555 556 557 558

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

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

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

561
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
562

563 564
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
565

566
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
567
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
568
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
569

570
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
571
	$(if $(QUIET), @echo 'Linking  $@' &&) \
572
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
573 574
	$(STRIP) $@

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

579 580 581
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
582 583 584 585
# depend and clean targets

include .depend.ide

François Bobot's avatar
François Bobot committed
586
.depend.ide:
587
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
588 589 590 591

depend: .depend.ide

clean::
592
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
593 594
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
595
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
596 597
	rm -f .depend.ide

598
install_no_local::
599
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE)
600 601

install_local: bin/why3ide
602

603
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
604

605

MARCHE Claude's avatar
MARCHE Claude committed
606 607 608 609
###############
# Replayer
###############

François Bobot's avatar
François Bobot committed
610
REPLAYER_FILES = replay
MARCHE Claude's avatar
MARCHE Claude committed
611 612 613 614 615 616 617 618

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
619
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
620 621 622 623 624 625

# build targets

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

626
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
627 628 629 630
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

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

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

# depend and clean targets

include .depend.replayer

François Bobot's avatar
François Bobot committed
642
.depend.replayer:
MARCHE Claude's avatar
MARCHE Claude committed
643 644 645 646 647 648 649 650 651 652 653
	$(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@

depend: .depend.replayer

clean::
	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::
654
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
MARCHE Claude's avatar
MARCHE Claude committed
655 656 657

install_local: bin/why3replayer

658 659 660 661
###############
# Stats
###############

François Bobot's avatar
François Bobot committed
662
STATS_FILES = stats
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

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

François Bobot's avatar
François Bobot committed
694
.depend.stats:
695 696 697 698 699 700 701 702 703 704 705 706 707
	$(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

708 709 710 711
###############
# Html
###############

François Bobot's avatar
François Bobot committed
712
HTML_FILES = html_session
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

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

François Bobot's avatar
François Bobot committed
744
.depend.html:
745 746 747 748 749 750 751 752 753 754 755 756 757
	$(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
758

759
###############
760
# Bench
761 762
###############

763 764
ifeq (@enable_bench@,yes)

765
BENCH_FILES = worker db bench benchrc benchdb whybench
766 767 768 769 770 771 772 773

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

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

774
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/bench -I @SQLITE3LIB@
775 776 777

# build targets

778 779
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
780

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

784
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
785 786 787 788
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

789
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
790 791 792
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

793 794 795
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

796 797 798 799 800 801 802 803 804 805 806 807
# 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/*~
808
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
809 810 811
	rm -f .depend.bench

install_no_local::
812
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
813 814

install_local: bin/why3bench
815

816 817
endif

818 819 820
##############
# Coq plugin
##############
821

822
ifeq (@enable_coq_plugin@,yes)
823

824 825 826 827 828 829 830 831 832 833 834 835 836
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))

837
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
838

839 840
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
841

842 843
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
844

845
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
846 847
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

848
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
849 850
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

851 852 853 854
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
855

856
include .depend.coq-plugin
857

858
.depend.coq-plugin: $(COQGENERATED)
859 860
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

861
depend: .depend.coq-plugin
862 863 864 865 866 867

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)
868 869 870 871 872 873 874 875 876 877
	rm -f .depend.coq-plugin

endif

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

ifeq (@enable_coq_libs@,yes)

878
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
879 880
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))

881
COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
882 883
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))

884 885 886 887 888
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
889 890

COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
891 892 893 894 895 896 897

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

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

898 899 900 901 902 903 904 905 906
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 "]" >> $@

907 908 909 910
all: $(COQVO)

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

install_local: $(COQVO)

include .depend.coq-libs

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

depend: .depend.coq-libs

clean::
930
	rm -f $(COQVO) $(addsuffix .glob, $(COQLIBS_FILES))
931
	rm -f .depend.coq-libs
932

933 934 935 936 937
else

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

938
endif
939

940 941 942
########
# Tptp2why
########
943

944
ifeq (@enable_whytptp@,yes)
945

946 947
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
948

François Bobot's avatar
François Bobot committed
949
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
950

951
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
952 953 954 955 956 957

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

958 959
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
960 961 962

# build targets

Andrei Paskevich's avatar
Andrei Paskevich committed
963 964
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt  opt : lib/plugins/whytptp.cmxs
965

Andrei Paskevich's avatar
Andrei Paskevich committed
966 967
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
968

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

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

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

980 981 982 983 984 985 986 987 988 989 990
# 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)
991
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
992
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
993
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
Andrei Paskevich's avatar
Andrei Paskevich committed
994
	rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
995 996
	rm -f .depend.tptp2why

997
endif
998

999 1000 1001 1002
#######
# tools
#######

1003
TOOLS = bin/why3-cpulimit$(EXE)
1004 1005 1006

byte opt: $(TOOLS)

1007
bin/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
1008
	$(CC) -Wall -o $@ $^
1009 1010

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

1013
install_no_local::
1014
	cp -f bin/why3-cpulimit$(EXE) $(BINDIR)/why3-cpulimit$(EXE)
1015

1016 1017 1018 1019
#########
# why3doc
#########

1020 1021
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036

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

1037
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
1038 1039 1040 1041
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@