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_distinction \
129
		encoding_enumeration encoding \
130 131
		libencoding encoding_select \
		encoding_decorate encoding_bridge \
François Bobot's avatar
François Bobot committed
132
		encoding_explicit encoding_guard encoding_sort \
133
		encoding_instantiate simplify_array filter_trigger \
134 135
		introduction abstraction close_epsilon lift_epsilon \
	        eval_match
136

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

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

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

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

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

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

164
LIB_PARSER_POSTLUDE = \
165
  "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"
166 167

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

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

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

180
# build targets
181

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

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

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

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

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

# depend target
198

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

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

depend: .depend.lib

206 207
# clean target

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

221 222 223
###############
# installation
###############
224

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

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

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

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

261

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

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

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

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

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

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

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

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

install_local: bin/why3
292

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

297 298
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
299

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

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

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

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

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

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

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

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

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

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

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

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

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

341 342
# test target

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

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

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

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

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

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

361
install_local: bin/why3ml
362

363 364 365 366
##########
# gallery
##########

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

.PHONY: gallery

376 377 378 379 380 381 382
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
383

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

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

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

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

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

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

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

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

440
install_local: bin/why3config
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 502
###############
# 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
503 504 505 506
###############
# IDE
###############

507 508
ifeq (@enable_ide@,yes)

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

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

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

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

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

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

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

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

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

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

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

include .depend.ide

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

depend: .depend.ide

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

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

install_local: bin/why3ide
561

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

564

MARCHE Claude's avatar
MARCHE Claude committed
565 566 567 568 569 570 571 572 573 574 575 576 577
###############
# 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
578
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
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

# 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


618
###############
619
# Bench
620 621
###############

622 623
ifeq (@enable_bench@,yes)

624
BENCH_FILES = bench benchrc benchdb whybench
625 626 627

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

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

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

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

# build targets

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

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

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

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

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

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

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

install_local: bin/why3bench
676

677 678
endif

679 680 681
##############
# Coq plugin
##############
682

683
ifeq (@enable_coq_support@,yes)
684

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

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

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

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

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

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

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

717 718 719 720 721 722 723 724 725 726 727 728 729 730
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

731
endif
732

733 734 735
########
# Tptp2why
########
736

737
ifeq (@enable_whytptp@,yes)
738

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

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

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

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

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

# build targets

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

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

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

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

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

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

790
endif
791

792 793 794 795
#######
# tools
#######

796
TOOLS = bin/why3-cpulimit
797 798 799

byte opt: $(TOOLS)

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

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

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

809 810 811 812
#########
# why3doc
#########

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

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

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

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

845 846
# depend and clean targets

847 848
WHY3DOCGENERATED=src/why3doc/to_html.ml

849 850
include .depend.why3doc

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

depend: .depend.why3doc

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

863 864
install_local: bin/why3doc

865 866 867 868
########
# bench
########

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

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

877
BENCH_PLUGINS_CMO := helloworld.cmo
878 879 880
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
881 882 883
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

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

###############
890
# test targets
891
###############
892

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

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

915 916 917
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
918

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

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

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

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

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

935 936

## Examples : Plugins ##
937

938
ifeq (@enable_plugins@,yes)
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 977
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
978

979
endif
980

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

985 986 987 988 989
.PHONY: doc

ifeq (@enable_doc@,yes)

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

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

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

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

1002 1003 1004 1005
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
1006

1007
doc/manual.pdf: $(BNFTEX) $(DOCTEX)
1008
	cd doc; $(RUBBER) -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1009

1010 1011
# doc/manual.html: doc/manual.tex doc/version.tex
# 	$(MAKE) -C doc manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1012

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1013
clean::
1014 1015 1016 1017 1018 1019 1020
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1021

1022
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
1023
# API DOC
1024
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1025

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
1026 1027
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
1028
MODULESTODOC = util/util util/hashweak \
1029
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
1030
	core/env core/task \
1031 1032
	driver/whyconf driver/driver \
	ide/session
MARCHE Claude's avatar
MARCHE Claude committed
1033 1034
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
1035 1036 1037

FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))

1038
apidoc: $(FILESTODOC)
1039
	mkdir -p doc/apidoc
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
1040
	$(OCAMLDOC) -d doc/apidoc -html -keep-code $(INCLUDES) \
1041
		$(LIBINCLUDES) -I src $(FILESTODOC)
1042
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
1043

MARCHE Claude's avatar
MARCHE Claude committed
1044
install_apidoc: apidoc
1045
	rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
MARCHE Claude's avatar
MARCHE Claude committed
1046

MARCHE Claude's avatar
MARCHE Claude committed
1047
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
1048
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
1049
		$(LIBINCLUDES) -I src $(FILESTODOC)
1050
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1051

1052
clean::
1053
	rm -f doc/apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1054

1055
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1056
# generic rules
1057
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1058

Andrei Paskevich's avatar
Andrei Paskevich committed
1059
%.cmi: %.mli
1060
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1061

Francois Bobot's avatar
Francois Bobot committed
1062
%.cmo: %.ml
1063
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1064

1065
%.cmx: %.ml
1066
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1067

1068
%.cmxs: %.ml
1069
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
1070

Andrei Paskevich's avatar
Andrei Paskevich committed
1071
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1072 1073
	$(OCAMLLEX) $<

1074
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1075 1076
	$(OCAMLYACC) -v $<

Andrei Paskevich's avatar
Andrei Paskevich committed
1077 1078
# .ml4.ml:
# 	$(CAMLP4) pr_o.cmo -impl $< > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1079

Andrei Paskevich's avatar
Andrei Paskevich committed
1080 1081
# lib/coq/%.vo: lib/coq/%.v
# 	$(COQC8) -I lib/coq $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1082

Andrei Paskevich's avatar
Andrei Paskevich committed
1083 1084
# lib/coq-v7/%.vo: lib/coq-v7/%.v
# 	$(COQC7) -I lib/coq-v7 $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1085

Andrei Paskevich's avatar
Andrei Paskevich committed
1086 1087 1088 1089 1090 1091 1092 1093
# jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile
# 	if test "@enable_apron@" = "yes" ; then \
# 	  echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \
# 	  cat jc/jc_annot_inference.ml >> jc/jc_ai.ml; \
# 	else \
# 	  echo "# 1 \"jc/jc_annot_fail.ml\"" > jc/jc_ai.ml; \
# 	  cat jc/jc_annot_fail.ml >> jc/jc_ai.ml; \
# 	fi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1094 1095 1096 1097 1098 1099