Makefile.in 33.3 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
3
#  Copyright (C) 2010-2011                                               #
MARCHE Claude's avatar
MARCHE Claude committed
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 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
CAMLP5O   = @CAMLP5O@

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

69 70
RUBBER = @RUBBER@

71
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
72
#PDFVIEWER = @PDFVIEWER@
73

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

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

82 83
# external libraries common to all binaries

84
EXTOBJS =
François Bobot's avatar
META  
François Bobot committed
85
EXTLIBS = str unix nums @META_DYNLINK@
86 87 88

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
89

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90 91 92
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94
all: @OCAMLBEST@
Francois Bobot's avatar
Francois Bobot committed
95

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

100 101
plugins: plugins.@OCAMLBEST@

102
.PHONY: byte opt clean depend all install install_local install_no_local
103
.PHONY: plugins plugins.byte plugins.opt
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
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

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

François Bobot's avatar
François Bobot committed
114
LIB_UTIL = stdlib exn_printer debug pp loc print_tree \
115
	   cmdline hashweak hashcons util sysutil rc plugin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116

117
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
118

119
LIB_PARSER = ptree denv typing parser lexer
120

121
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
122
	     whyconf autodetection
123

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

136
LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3
137

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

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

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

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

160
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
161
$(LIBCMX): OFLAGS += -for-pack Why
162

163
LIB_PARSER_POSTLUDE = \
164
  "let logic_file_eof env = inside_env env logic_file_eof\nlet list0_decl_eof env lenv uc = inside_uc env lenv uc list0_decl_eof\n"
165 166

LIB_PARSER_INTERFACE = \
167 168
  -e "s/^val  *logic_file_eof *:/val logic_file_eof : Env.env ->/" \
  -e "s/^val  *list0_decl_eof *:/val list0_decl_eof : Env.env -> \
169 170
  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"

171 172
src/parser/parser.ml: src/parser/parser.pre.ml
	cp src/parser/parser.pre.ml src/parser/parser.ml
173
	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
174 175 176

src/parser/parser.mli: src/parser/parser.pre.mli
	sed $(LIB_PARSER_INTERFACE) src/parser/parser.pre.mli > \
177
					src/parser/parser.mli
178

179
# build targets
180

181 182
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183

184
src/why.cma: src/why.cmo
185 186
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

187
src/why.cmxa: src/why.cmx
188 189
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

190 191
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
192

193 194 195 196
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
197

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198 199
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
200
.depend.lib: src/config.ml $(LIBGENERATED)
201
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202 203 204

depend: .depend.lib

205 206
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
207
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
208 209
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
210 211
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
212 213 214 215 216 217
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
	rm -f src/why.cm[iox] src/why.[ao] src/why.cma src/why.cmxa
218
	rm -f .depend.lib
219

220 221 222
###############
# installation
###############
223

224
install_no_local::
225
	mkdir -p $(BINDIR)
226
	mkdir -p $(LIBDIR)/why3/plugins
227
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
228
	mkdir -p $(DATADIR)/why3/emacs
229
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
230 231
	mkdir -p $(DATADIR)/why3/theories
	mkdir -p $(DATADIR)/why3/theories/transform
232
	mkdir -p $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
233 234 235
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
	cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
236
	cp -f modules/*.mlw $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
237
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
238 239
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
240
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
241 242
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

MARCHE Claude's avatar
MARCHE Claude committed
243 244 245
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
	cp -f src/why.cm* $(OCAMLLIB)/why3
246
	cp -f META $(OCAMLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
247 248
	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi

249 250 251 252 253
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
254
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
255
install-lib: install_no_local_lib
256 257
endif

MARCHE Claude's avatar
MARCHE Claude committed
258 259
install-all: install install-lib

260

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261
##################
262
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263 264
##################

265 266
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267

268
bin/why3.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
269 270
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
271 272
	$(STRIP) $@

273
bin/why3.byte: src/why.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
274 275
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
276

277 278 279
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

280 281
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
282

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
283
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
284
	rm -f src/main.cm[iox] src/main.annot src/main.o
285
	rm -f bin/why3.byte bin/why3.opt bin/why3
286

287
install_no_local::
288 289 290
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3

install_local: bin/why3
291

292 293 294
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
295

296 297
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
	    pgm_module pgm_wp pgm_env pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
298

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

301 302 303 304 305
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

306
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
307 308

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

310 311
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312

313
bin/why3ml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
314 315
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316 317
	$(STRIP) $@

318
bin/why3ml.byte: src/why.cma $(PGMCMO) src/main.cmo
319 320 321
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

322 323 324
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

325
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326 327

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332 333 334
depend: .depend.programs

clean::
335 336
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
337
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
338
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
339

340 341
# test target

342 343
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
344

345 346
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
347

348 349
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
350

351 352
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
353

354 355 356
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

357
install_no_local::
358
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
359

360
install_local: bin/why3ml
361

362 363 364 365
##########
# gallery
##########

366
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
367
        power mergesort_list mac_carthy isqrt insertion_sort_list flag \
368
	distance muller fib_memo fibonacci \
369 370
        vstte10_aqueue vstte10_inverting vstte10_max_sum \
	vstte10_queens vstte10_search_list \
371
        vacid_0_sparse_array
372 373 374

.PHONY: gallery

375 376 377 378 379 380 381
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	@for f in $(GALLERYPGMS); do \
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
	done
382

383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399
########
# 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

400 401
byte: bin/why3config.byte
opt:  bin/why3config.opt
402

403
bin/why3config.opt: src/why.cmxa $(CONFIGCMX)
404 405 406 407
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

408
bin/why3config.byte: src/why.cma $(CONFIGCMO)
409 410 411
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

412 413 414
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

415 416 417 418 419 420 421 422 423 424 425 426 427
# 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
428
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
429 430 431
	rm -f .why.conf
	rm -f .depend.config

432 433
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
434
		--detect --conf_file why.conf
435

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

439
install_local: bin/why3config
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 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501
###############
# GUI
###############

ifeq (@enable_ide@,yes)

GUI_FILES = xml session gconfig db gmain

GUIMODULES = $(addprefix src/ide/, $(GUI_FILES))

GUIML  = $(addsuffix .ml,  $(GUIMODULES))
GUIMLI = $(addsuffix .mli, $(GUIMODULES))
GUICMO = $(addsuffix .cmo, $(GUIMODULES))
GUICMX = $(addsuffix .cmx, $(GUIMODULES))

$(GUICMO) $(GUICMX): INCLUDES += -I src/ide -I @SQLITE3LIB@

# build targets

byte: bin/why3gui.byte
opt:  bin/why3gui.opt

bin/why3gui.opt bin/why3gui.byte: INCLUDES += -I @LABLGTK2LIB@ -I @SQLITE3LIB@
bin/why3gui.opt bin/why3gui.byte: EXTOBJS +=
bin/why3gui.opt bin/why3gui.byte: EXTLIBS += lablgtk lablgtksourceview2 sqlite3

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

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

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

# depend and clean targets

include .depend.gui

.depend.gui: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(GUIML) $(GUIMLI) > $@

depend: .depend.gui

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

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

install_local: bin/why3gui

endif


MARCHE Claude's avatar
MARCHE Claude committed
502 503 504 505
###############
# IDE
###############

506 507
ifeq (@enable_ide@,yes)

508 509
# IDE_FILES = xml session gconfig db gmain
IDE_FILES = xml session gconfig newmain
MARCHE Claude's avatar
MARCHE Claude committed
510 511 512 513 514 515 516 517

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

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

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

520
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
521

522 523
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
524

525
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
526
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
527
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
528

529
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
530
	$(if $(QUIET), @echo 'Linking  $@' &&) \
531
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
532 533
	$(STRIP) $@

534
bin/why3ide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
535
	$(if $(QUIET),@echo 'Linking  $@' &&) \
536
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
537

538 539 540
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
541 542 543 544
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
545
.depend.ide: src/ide/xml.ml
546
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
547 548 549 550 551 552

depend: .depend.ide

clean::
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
553
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
554 555
	rm -f .depend.ide

556
install_no_local::
557 558 559
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
560

561
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
562

563

MARCHE Claude's avatar
MARCHE Claude committed
564 565 566 567 568 569 570 571 572 573 574 575 576
###############
# Replayer
###############

REPLAYER_FILES = xml session replay

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
577
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616

# build targets

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

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

bin/why3replayer.byte: src/why.cma $(PGMCMO) $(REPLAYERCMO)
	$(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::
	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::
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer

install_local: bin/why3replayer


617
###############
618
# Bench
619 620
###############

621 622
ifeq (@enable_bench@,yes)

623
BENCH_FILES = bench benchrc benchdb whybench
624 625 626

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

627
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
628 629 630 631 632 633

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

634
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
635 636 637

# build targets

638 639
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
640

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

644
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
645 646 647 648
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

649
bin/why3bench.byte: src/why.cma  $(PGMCMO) $(BENCHCMO)
650 651 652
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

653 654 655
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

656 657 658 659 660 661 662 663 664 665 666 667
# 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/*~
668
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
669 670 671
	rm -f .depend.bench

install_no_local::
672 673 674
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
675

676 677
endif

678 679 680
##############
# Coq plugin
##############
681

682
ifeq (@enable_coq_support@,yes)
683

684 685 686 687 688 689 690 691 692 693 694 695 696
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))

697
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
698

699 700
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
701

702 703
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
704

705
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
706 707
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

708
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
709 710
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

711 712 713 714
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
715

716 717 718 719 720 721 722 723 724 725 726 727 728 729
include .depend.coq

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

depend: .depend.coq

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)
	rm -f .depend.coq

730
endif
731

732 733 734
########
# Tptp2why
########
735

736
ifeq (@enable_whytptp@,yes)
737

738 739
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
740

François Bobot's avatar
François Bobot committed
741
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
742

743
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
744 745 746 747 748 749

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

750 751
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
752 753 754

# build targets

François Bobot's avatar
François Bobot committed
755
plugins.byte byte: plugins/whytptp.cmo
756
plugins.opt  opt : plugins/whytptp.cmxs
757

François Bobot's avatar
François Bobot committed
758 759
plugins/whytptp.cmxs plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
plugins/whytptp.cmxs plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
760

761
plugins/whytptp.cmxs: $(TPTPCMX)
762
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
763
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
764

765
plugins/whytptp.cmo: $(TPTPCMO)
766
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
767 768
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
769 770 771
install_no_local::
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/plugins

772 773 774 775 776 777 778 779 780 781 782
# 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)
783
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
784
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
785
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
786
	rm -f plugins/whytptp.cm* plugins/whytptp.o
787 788
	rm -f .depend.tptp2why

789
endif
790

791 792 793 794
#######
# tools
#######

795
TOOLS = bin/why3-cpulimit
796 797 798

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
799
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
800
	$(CC) -Wall -o $@ $^
801 802

clean::
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
803
	rm -f bin/why3-cpulimit src/tools/*~
804

805
install_no_local::
806 807
	cp -f bin/why3-cpulimit $(BINDIR)

808 809 810 811
#########
# why3doc
#########

812 813
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837

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

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

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

838 839 840
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

841 842 843
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

844 845
# depend and clean targets

846 847
WHY3DOCGENERATED=src/why3doc/to_html.ml

848 849
include .depend.why3doc

850
.depend.why3doc: $(WHY3DOCGENERATED)
851 852 853 854 855
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
856
	rm -f $(WHY3DOCGENERATED)
857 858
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
859
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
860 861
	rm -f .depend.why3doc

862 863
install_local: bin/why3doc

864 865 866 867
########
# bench
########

François Bobot's avatar
François Bobot committed
868
.PHONY: bench test comp_bench_plugins
869

870 871
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
	$(MAKE) test-api
872
	sh bench/bench \
873 874
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
875

876
BENCH_PLUGINS_CMO := helloworld.cmo
877 878 879
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

François Bobot's avatar
François Bobot committed
880 881 882
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
883
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
884 885 886
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
887 888

###############
889
# test targets
890
###############
891

892 893
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
894

895
test: bin/why3.byte plugins.byte $(TOOLS)
896
	mkdir -p output_why3
897 898 899 900 901
	bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
	# bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
	# bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
	# bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
	echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
902
	@printf "*** Checking Coq file generation ***\\n"
903
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
904
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
905 906
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
907
		floating_point.Test map.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
908
		; do \
909
	  printf "Generating Coq file for $$i\\n" && \
910
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
911
	@printf "*** Checking Coq compilation ***\\n"
912
	@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
913

914 915 916
testl: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
	ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
917

918 919
testl-debug: bin/why3ml.opt
	bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
920

921 922
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
923

924 925
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
926

MARCHE Claude's avatar
MARCHE Claude committed
927
test-api: src/why.cma
Andrei Paskevich's avatar
Andrei Paskevich committed
928
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/use_api.ml \
MARCHE Claude's avatar
MARCHE Claude committed
929
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
930

MARCHE Claude's avatar
MARCHE Claude committed
931
bts12244: src/why.cma
Andrei Paskevich's avatar
Andrei Paskevich committed
932
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/bts12244.ml
MARCHE Claude's avatar
MARCHE Claude committed
933

934 935

## Examples : Plugins ##
936

937
ifeq (@enable_plugins@,yes)
938

939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976
PLUGDIR = examples/plugins/
PLUG_FILES = genequlin

PLUGMODULES = $(addprefix $(PLUGDIR), $(PLUG_FILES))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES))

# ifeq (@enable_plug_support@,yes)
# byte: src/plug-plugin/whytac.cma
# opt:  src/plug-plugin/whytac.cmxs
# endif

# $(PLUGCMO):  src/why.cma
# $(PLUGCMXS): src/why.cmxa

.PHONY: examples_plugins.byte examples_plugins.opt

examples_plugins.byte : $(PLUGCMO)
examples_plugins.opt : $(PLUGCMXS)

# depend and clean targets

include .depend.plug

.depend.plug: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I $(PLUGDIR) $(PLUGML) | sed "s/cmx/cmxs/" > $@

depend: .depend.plug

clean::
	rm -f $(PLUGDIR)/*.cm[iox] $(PLUGDIR)/*.o
	rm -f $(PLUGDIR)/*.cma $(PLUGDIR)/*.cmxs
	rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~
	rm -f $(PLUGGENERATED)
	rm -f .depend.plug
977

978
endif
979

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
980 981 982
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
983

984 985 986 987 988
.PHONY: doc

ifeq (@enable_doc@,yes)

doc: doc/manual.pdf
MARCHE Claude's avatar
MARCHE Claude committed
989
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
990

991 992
BNF = qualid constant operator term type formula theory why_file  \
      typev expr module whyml_file
993
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
994 995 996 997 998