Makefile.in 38.3 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
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
56 57
COQC      = @COQC@
COQDEP    = @COQDEP@
58 59
CAMLP5O   = @CAMLP5O@

60 61
ifeq (@OCAMLBEST@,opt)
OCAMLDEP  = @OCAMLDEP@ -native
62
else
63
OCAMLDEP  = @OCAMLDEP@
64 65
endif

66 67
RUBBER = @RUBBER@

68
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
69
#PDFVIEWER = @PDFVIEWER@
70

71 72
BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aer-29 -dtypes    -I src $(INCLUDES)
73

74
ifeq (@enable_profiling@,yes)
75 76 77 78
OFLAGS += -g -p
STRIP = true
endif

79 80
# external libraries common to all binaries

81
EXTOBJS =
Andrei Paskevich's avatar
Andrei Paskevich committed
82
EXTLIBS = str unix nums dynlink
83 84 85

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
86

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
all: @OCAMLBEST@ plugins
Francois Bobot's avatar
Francois Bobot committed
92

93 94 95 96
ifeq (@enable_local@,yes)
all: install_local
endif

97 98
plugins: plugins.@OCAMLBEST@

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102
#############
103
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105

106
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
107 108
	       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
109 110
	       src/driver/driver_lexer.ml src/coq_config.ml \
               src/session/xml.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
111

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

115
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
116

117
LIB_PARSER = ptree denv typing parser lexer
118

119
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
120
	     whyconf autodetection
121

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

134
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs simplify gappa \
135
	      cvc3 yices
136

François Bobot's avatar
François Bobot committed
137 138
LIB_SESSION = xml termcode session session_tools session_scheduler

139
LIBMODULES = src/config src/coq_config \
140 141 142 143 144
	      $(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
145 146
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
	      $(addprefix src/session/, $(LIB_SESSION))
147

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

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

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

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

165
# build targets
166

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

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

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

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

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

# depend target
183

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

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

depend: .depend.lib

191 192
# clean target

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

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

206 207 208
###############
# installation
###############
209

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

MARCHE Claude's avatar
MARCHE Claude committed
227 228
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
229
	cp -f src/why3.cm* $(OCAMLLIB)/why3
230
	cp -f META $(OCAMLLIB)/why3
231
	if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
232
	if test -f src/why3.o; then cp -f src/why3.o $(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
##################
# Why plugins
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
249 250
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli
251 252

PLUG_PARSER = genequlin
253
PLUG_PRINTER = tptpfof
254
PLUG_TRANSFORM =
Andrei Paskevich's avatar
Andrei Paskevich committed
255
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer
256

Andrei Paskevich's avatar
Andrei Paskevich committed
257 258
PLUGINS = genequlin tptpfof tptp

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

Andrei Paskevich's avatar
Andrei Paskevich committed
261 262
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
263 264 265

PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
266
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
267
	      $(TPTPMODULES)
268 269 270 271 272 273

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

Andrei Paskevich's avatar
Andrei Paskevich committed
274
PLUGDIRS = parser printer transform tptp
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
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 $@ $<

Andrei Paskevich's avatar
Andrei Paskevich committed
306
lib/plugins/tptp.cmxs: $(TPTPCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
307
	$(if $(QUIET), @echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
308
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
Andrei Paskevich's avatar
Andrei Paskevich committed
309

Andrei Paskevich's avatar
Andrei Paskevich committed
310
lib/plugins/tptp.cmo: $(TPTPCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
311
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
312
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
Andrei Paskevich's avatar
Andrei Paskevich committed
313

314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
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

339

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340
##################
341
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342 343
##################

344 345
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346

347
bin/why3.opt: src/why3.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
348 349
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350 351
	$(STRIP) $@

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

356 357 358
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

359 360
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
361

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
362
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
363
	rm -f src/main.cm[iox] src/main.annot src/main.o
364
	rm -f bin/why3.byte bin/why3.opt bin/why3
365

366
install_no_local::
367
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
368 369

install_local: bin/why3
370

371 372 373
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
374

375
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
376
	    pgm_module pgm_wp pgm_env pgm_typing pgm_ocaml pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
377

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

380 381 382 383 384
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

385
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
386 387

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

389 390
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391

392
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
393 394
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
395 396
	$(STRIP) $@

397
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
398 399 400
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

401 402 403
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

404
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
405 406

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411 412 413
depend: .depend.programs

clean::
414 415
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
416
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
417
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
418

419 420
# test target

421 422
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
423

424 425
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
426

427 428
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
429

430 431
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
432

433 434 435
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

436
install_no_local::
437
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml$(EXE)
438

439
install_local: bin/why3ml
440

441 442 443 444
########
# Whyml (new API)
########

445
MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module
446 447 448 449 450 451 452 453 454 455 456 457

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

458 459
byte: $(MLWCMO)
opt:  $(MLWCMX)
460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475

# 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

476 477 478 479
##########
# gallery
##########

480
# we export exactly the programs that have a why3session.xml file
481 482 483

.PHONY: gallery

484 485
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
486 487 488
	@for x in `find examples/programs/ -name why3session.xml`; do \
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
489 490 491
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
492 493 494 495
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	  cd examples/programs/; \
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
	  cd ../..; \
496
	done
497

498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514
########
# 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

515 516
byte: bin/why3config.byte
opt:  bin/why3config.opt
517

518
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
519 520 521 522
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

523
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
524 525 526
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

527 528 529
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

530 531 532 533 534 535 536 537 538 539 540 541 542
# 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
543
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
544 545
	rm -f .depend.config

546 547
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
548
		--detect --conf_file why.conf
549

550
install_no_local::
551
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
552

553
install_local: bin/why3config
554

MARCHE Claude's avatar
MARCHE Claude committed
555 556 557 558
###############
# IDE
###############

559 560
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
561
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
562 563 564 565 566 567 568 569

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

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

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

572
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
573

574 575
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
576

577
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
578
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
579
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
580

581
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
582
	$(if $(QUIET), @echo 'Linking  $@' &&) \
583
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
584 585
	$(STRIP) $@

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

590 591 592
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
593 594 595 596
# depend and clean targets

include .depend.ide

François Bobot's avatar
François Bobot committed
597
.depend.ide:
598
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
599 600 601 602

depend: .depend.ide

clean::
603
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
604 605
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
606
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
607 608
	rm -f .depend.ide

609
install_no_local::
610
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE)
611 612

install_local: bin/why3ide
613

614
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
615

616

MARCHE Claude's avatar
MARCHE Claude committed
617 618 619 620
###############
# Replayer
###############

François Bobot's avatar
François Bobot committed
621
REPLAYER_FILES = replay
MARCHE Claude's avatar
MARCHE Claude committed
622 623 624 625 626 627 628 629

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
630
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
631 632 633 634 635 636

# build targets

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

637
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
638 639 640 641
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

642
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
643 644 645 646 647 648 649 650 651 652
	$(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
653
.depend.replayer:
MARCHE Claude's avatar
MARCHE Claude committed
654 655 656 657 658 659 660 661 662 663 664
	$(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::
665
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
MARCHE Claude's avatar
MARCHE Claude committed
666 667 668

install_local: bin/why3replayer

669 670 671 672 673 674

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

SESSION_FILES = why3session_lib why3session_mod why3session_copy \
675
		why3session_info why3session_rm why3session
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 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722

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

SESSIONML  = $(addsuffix .ml,  $(SESSIONMODULES))
SESSIONMLI = $(addsuffix .mli, $(SESSIONMODULES))
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

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

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

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

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

# depend and clean targets

include .depend.session

.depend.session:
	$(OCAMLDEP) -slash -I src -I src/why3session $(SESSIONML) $(SESSIONMLI) > $@

depend: .depend.session

clean::
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
	rm -f bin/why3session.byte bin/why3session.opt bin/why3session
	rm -f .depend.session

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

install_local: bin/why3session

723 724 725 726
###############
# Stats
###############

François Bobot's avatar
François Bobot committed
727
STATS_FILES = stats
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 754 755 756 757 758

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
759
.depend.stats:
760 761 762 763 764 765 766 767 768 769 770 771 772
	$(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

773 774 775 776
###############
# Html
###############

François Bobot's avatar
François Bobot committed
777
HTML_FILES = html_session
778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808

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
809
.depend.html:
810 811 812 813 814 815 816 817 818 819 820 821 822
	$(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
823

824
###############
825
# Bench
826 827
###############

828 829
ifeq (@enable_bench@,yes)

830
BENCH_FILES = worker db bench benchrc benchdb whybench
831 832 833 834 835 836 837 838

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

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

839
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/bench -I @SQLITE3LIB@
840 841 842

# build targets

843 844
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
845

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

849
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
850 851 852 853
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

854
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
855 856 857
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

858 859 860
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

861 862 863 864 865 866 867 868 869 870 871 872
# 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/*~
873
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
874 875 876
	rm -f .depend.bench

install_no_local::
877
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
878 879

install_local: bin/why3bench
880

881 882
endif

883 884 885
##############
# Coq plugin
##############
886

887
ifeq (@enable_coq_plugin@,yes)
888

889 890 891 892 893 894 895 896 897 898 899 900 901
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))

902
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
903

904 905
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
906

907 908
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
909

910
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
911 912
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

913
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
914 915
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

916 917 918 919
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
920

921
include .depend.coq-plugin
922

923
.depend.coq-plugin: $(COQGENERATED)
924 925
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

926
depend: .depend.coq-plugin
927 928 929 930 931 932

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)
933 934 935 936 937 938 939 940 941 942
	rm -f .depend.coq-plugin

endif

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

ifeq (@enable_coq_libs@,yes)

943
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
944 945
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))

946
COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
947 948
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))

949 950 951 952 953
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
954 955

COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
956 957 958 959 960 961 962

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

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

963 964 965 966 967 968 969 970 971
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 "]" >> $@

972 973 974 975
all: $(COQVO)

install_no_local::
	mkdir -p $(LIBDIR)/why3/coq
976 977
	mkdir -p $(LIBDIR)/why3/coq/int
	cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
978
	mkdir -p $(LIBDIR)/why3/coq/real
979
	cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
980 981
ifeq (@enable_coq_fp_libs@,yes)
	mkdir -p $(LIBDIR)/why3/coq/floating_point
982
	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
983
endif
984 985 986 987 988 989 990 991 992 993 994

install_local: $(COQVO)

include .depend.coq-libs

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

depend: .depend.coq-libs

clean::
995
	rm -f $(COQVO) $(addsuffix .glob, $(COQLIBS_FILES))
996
	rm -f .depend.coq-libs
997

998 999 1000 1001 1002
else

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

1003
endif
1004

1005 1006 1007 1008
#######
# tools
#######

1009
TOOLS = bin/why3-cpulimit$(EXE)
1010 1011 1012

byte opt: $(TOOLS)

1013
bin/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
1014
	$(CC) -Wall -o $@ $^
1015 1016

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

1019
install_no_local::
1020
	cp -f bin/why3-cpulimit$(EXE) $(BINDIR)/why3-cpulimit$(EXE)
1021

1022 1023 1024 1025
#########
# why3doc
#########

1026 1027
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042

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

1043
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
1044 1045 1046 1047
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

1048
bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
1049 1050 1051
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^