Makefile.in 33.3 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3
#  Copyright (C) 2010-                                                   #
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 60 61 62 63 64
ifeq (@enable_menhirlib@,yes)
  MENHIR = @MENHIR@ --table
else
  MENHIR = @MENHIR@
endif

65 66 67 68 69 70 71 72
ifeq (@enable_menhirlib@,yes)
  MENHIRINC = -I +menhirLib
  MENHIRLIB = menhirLib
else
  MENHIRINC =
  MENHIRLIB =
endif

73 74
RUBBER = @RUBBER@

75
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
76
#PDFVIEWER = @PDFVIEWER@
77

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

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

86 87
# external libraries common to all binaries

88
EXTOBJS =
François Bobot's avatar
META  
François Bobot committed
89
EXTLIBS = str unix nums @META_DYNLINK@
90 91 92

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
93

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94 95 96
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
97

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

100 101 102 103
ifeq (@enable_local@,yes)
all: install_local
endif

104 105
plugins: plugins.@OCAMLBEST@

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109
#############
110
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
111
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
112

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

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

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

123
LIB_PARSER = ptree denv typing parser lexer
124

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

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

141
LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3
142

143 144 145 146 147 148
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)) \
149
	      $(addprefix src/printer/, $(LIB_PRINTER))
150

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

154 155
ifeq (@enable_hypothesis_selection@,yes)
	LIB_TRANSFORM += hypothesis_selection
156
	INCLUDES += -I +ocamlgraph
157 158 159
	EXTLIBS += ocamlgraph/graph
endif

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

165
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
166
$(LIBCMX): OFLAGS += -for-pack Why
167

168
LIB_PARSER_POSTLUDE = \
169
  "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"
170 171

LIB_PARSER_INTERFACE = \
172 173
  -e "s/^val  *logic_file_eof *:/val logic_file_eof : Env.env ->/" \
  -e "s/^val  *list0_decl_eof *:/val list0_decl_eof : Env.env -> \
174 175
  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"

176 177
src/parser/parser.ml: src/parser/parser.pre.ml
	cp src/parser/parser.pre.ml src/parser/parser.ml
178
	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
179 180 181

src/parser/parser.mli: src/parser/parser.pre.mli
	sed $(LIB_PARSER_INTERFACE) src/parser/parser.pre.mli > \
182
					src/parser/parser.mli
183

184
# build targets
185

186 187
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
188

189
src/why.cma: src/why.cmo
190 191
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

192
src/why.cmxa: src/why.cmx
193 194
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

195 196
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
197

198 199 200 201
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
202

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203 204
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
205
.depend.lib: src/config.ml $(LIBGENERATED)
206
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
207 208 209

depend: .depend.lib

210 211
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
212
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
213 214
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
215 216
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
217 218 219 220 221 222
	   $(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
223
	rm -f .depend.lib
224

225 226 227
###############
# installation
###############
228

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

MARCHE Claude's avatar
MARCHE Claude committed
248 249 250
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
	cp -f src/why.cm* $(OCAMLLIB)/why3
251
	cp -f META $(OCAMLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
252 253
	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi

254 255 256 257 258
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
259
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
260
install-lib: install_no_local_lib
261 262
endif

MARCHE Claude's avatar
MARCHE Claude committed
263 264
install-all: install install-lib

265

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
266
##################
267
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
268 269
##################

270 271
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
272

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

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

282 283 284
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

285 286
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
287

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
288
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
289
	rm -f src/main.cm[iox] src/main.annot src/main.o
290
	rm -f bin/why3.byte bin/why3.opt bin/why3
291

292
install_no_local::
293 294 295
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3

install_local: bin/why3
296

297 298 299
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300

301 302
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
303

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

306 307 308 309 310
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

311
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
312 313

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

315 316
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
317

318
bin/why3ml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
319 320
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321 322
	$(STRIP) $@

323
bin/why3ml.byte: src/why.cma $(PGMCMO) src/main.cmo
324 325 326
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

327 328 329
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

330
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331 332

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337 338 339
depend: .depend.programs

clean::
340 341
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
342
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
343
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
344

345 346
# test target

347 348
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
349

350 351
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
352

353 354
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
355

356 357
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
358

359 360 361
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

362
install_no_local::
363
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
364

365
install_local: bin/why3ml
366

367 368 369 370
##########
# gallery
##########

371
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
372
        power mergesort_list mac_carthy isqrt insertion_sort_list flag \
373
	distance muller fib_memo fibonacci \
374 375
        vstte10_aqueue vstte10_inverting vstte10_max_sum \
	vstte10_queens vstte10_search_list \
376
        vacid_0_sparse_array
377 378 379

.PHONY: gallery

380 381 382 383 384 385 386
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
387

388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
########
# 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

405 406
byte: bin/why3config.byte
opt:  bin/why3config.opt
407

408
bin/why3config.opt: src/why.cmxa $(CONFIGCMX)
409 410 411 412
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

413
bin/why3config.byte: src/why.cma $(CONFIGCMO)
414 415 416
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

417 418 419
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

420 421 422 423 424 425 426 427 428 429 430 431 432
# 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
433
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
434 435 436
	rm -f .why.conf
	rm -f .depend.config

437 438
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
439
		--detect --conf_file why.conf
440

441
install_no_local::
442
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
443

444
install_local: bin/why3config
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 502 503 504 505 506
###############
# 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
507 508 509 510
###############
# IDE
###############

511 512
ifeq (@enable_ide@,yes)

513 514
# IDE_FILES = xml session gconfig db gmain
IDE_FILES = xml session gconfig newmain
MARCHE Claude's avatar
MARCHE Claude committed
515 516 517 518 519 520 521 522

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

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

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

525
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
526

527 528
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
529

530
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
531
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
532
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2 
MARCHE Claude's avatar
MARCHE Claude committed
533

534
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
535
	$(if $(QUIET), @echo 'Linking  $@' &&) \
536
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
537 538
	$(STRIP) $@

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

543 544 545
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
546 547 548 549
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
550
.depend.ide: src/ide/xml.ml
551
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
552 553 554 555 556 557

depend: .depend.ide

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

561
install_no_local::
562 563 564
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
565

566
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
567

568

MARCHE Claude's avatar
MARCHE Claude committed
569 570 571 572 573 574 575 576 577 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 617 618 619 620 621
###############
# 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))

$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide 

# 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


622
###############
623
# Bench
624 625
###############

626 627
ifeq (@enable_bench@,yes)

628
BENCH_FILES = bench benchrc benchdb whybench
629 630 631

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

632
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
633 634 635 636 637 638

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

639
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
640 641 642

# build targets

643 644
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
645

646 647
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I +sqlite3
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
648

649
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
650 651 652 653
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

654
bin/why3bench.byte: src/why.cma  $(PGMCMO) $(BENCHCMO)
655 656 657
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

658 659 660
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

661 662 663 664 665 666 667 668 669 670 671 672
# 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/*~
673
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
674 675 676
	rm -f .depend.bench

install_no_local::
677 678 679
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
680

681 682
endif

683 684 685
##############
# Coq plugin
##############
686

687
ifeq (@enable_coq_support@,yes)
688

689 690 691 692 693 694 695 696 697 698 699 700 701
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))

702
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
703

704 705
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
706

707 708
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
709

710
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
711 712
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

713
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
714 715
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

716 717 718 719
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
720

721 722 723 724 725 726 727 728 729 730 731 732 733 734
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

735
endif
736

737 738 739
########
# Tptp2why
########
740

741
ifeq (@enable_whytptp@,yes)
742

743 744
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
745

François Bobot's avatar
François Bobot committed
746
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
747

748
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
749 750 751 752 753 754

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

755 756
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
757 758 759

# build targets

François Bobot's avatar
François Bobot committed
760
plugins.byte byte: plugins/whytptp.cmo
761
plugins.opt  opt : plugins/whytptp.cmxs
762

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

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

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

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

777 778 779 780 781 782 783 784 785 786 787
# 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)
788
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
789
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
790
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
791
	rm -f plugins/whytptp.cm* plugins/whytptp.o
792 793
	rm -f .depend.tptp2why

794
endif
795

796 797 798 799
#######
# tools
#######

800
TOOLS = bin/why3-cpulimit
801 802 803

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
804
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
805
	$(CC) -Wall -o $@ $^
806 807

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

810
install_no_local::
811 812
	cp -f bin/why3-cpulimit $(BINDIR)

813 814 815 816
#########
# why3doc
#########

817 818
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842

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) $^

843 844 845
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

846 847 848
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

849 850
# depend and clean targets

851 852
WHY3DOCGENERATED=src/why3doc/to_html.ml

853 854
include .depend.why3doc

855
.depend.why3doc: $(WHY3DOCGENERATED)
856 857 858 859 860
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
861
	rm -f $(WHY3DOCGENERATED)
862 863
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
864
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
865 866
	rm -f .depend.why3doc

867 868
install_local: bin/why3doc

869 870 871 872
########
# bench
########

François Bobot's avatar
François Bobot committed
873
.PHONY: bench test comp_bench_plugins
874

875 876
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
	$(MAKE) test-api
877
	sh bench/bench \
878 879
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
880

881
BENCH_PLUGINS_CMO := helloworld.cmo
882 883 884
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
885 886 887
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
888
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
889 890 891
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
892 893

###############
894
# test targets
895
###############
896

897 898
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
899

900
test: bin/why3.byte plugins.byte $(TOOLS)
901
	mkdir -p output_why3
902 903 904 905 906
	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
907
	@printf "*** Checking Coq file generation ***\\n"
908
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
909
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
910 911
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
912
		floating_point.Test map.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
913
		; do \
914
	  printf "Generating Coq file for $$i\\n" && \
915
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
916
	@printf "*** Checking Coq compilation ***\\n"
917
	@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
918

919 920 921
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
922

923 924
testl-debug: bin/why3ml.opt
	bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
925

926 927
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
928

929 930
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
931

MARCHE Claude's avatar
MARCHE Claude committed
932
test-api: src/why.cma
933
	ocaml $(EXTCMA)	src/why.cma -I src examples/use_api.ml \
MARCHE Claude's avatar
MARCHE Claude committed
934
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
935

MARCHE Claude's avatar
MARCHE Claude committed
936 937 938
bts12244: src/why.cma
	ocaml $(EXTCMA)	src/why.cma -I src examples/bts12244.ml 

939 940

## Examples : Plugins ##
941

942
ifeq (@enable_plugins@,yes)
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 977 978 979 980 981
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
982

983
endif
984

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
985 986 987
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
988

989 990 991 992 993
.PHONY: doc

ifeq (@enable_doc@,yes)

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

996
BNF = qualid constant operator term type formula theory
997
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
998 999 1000 1001 1002 1003 1004 1005

doc/%_bnf.tex: doc/%.bnf doc/bnf
	doc/bnf $< > $@

doc/bnf: doc/bnf.mll
	$(OCAMLLEX) $<
	$(OCAMLOPT) -o $@ doc/bnf.ml

1006 1007 1008 1009
DOC = api glossary ide intro library macros manpages \
      manual starting syntax syntaxref version whyml

DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1010

1011
doc/manual.pdf: $(BNFTEX) $(DOCTEX)
1012
	cd doc; $(RUBBER) -d manual.tex