Makefile.in 33.2 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
		introduction abstraction close_epsilon lift_epsilon
139

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

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

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

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

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

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

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

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

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

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

183
# build targets
184

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

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

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

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

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

# depend target
201

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

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

depend: .depend.lib

209 210
# clean target

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

224 225 226
###############
# installation
###############
227

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

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

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

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

264

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

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

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

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

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

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

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

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

install_local: bin/why3
295

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

344 345
# test target

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

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

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

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

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

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

364
install_local: bin/why3ml
365

366 367 368 369
##########
# gallery
##########

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

.PHONY: gallery

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

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

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

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

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

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

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

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

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

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

510 511
ifeq (@enable_ide@,yes)

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

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

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

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

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

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

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

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

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

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

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

include .depend.ide

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

depend: .depend.ide

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

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

install_local: bin/why3ide
564

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

567

MARCHE Claude's avatar
MARCHE Claude committed
568 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
###############
# 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


621
###############
622
# Bench
623 624
###############

625 626
ifeq (@enable_bench@,yes)

627
BENCH_FILES = bench benchrc benchdb whybench
628 629 630

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

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

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

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

# build targets

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

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

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

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

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

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

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

install_local: bin/why3bench
679

680 681
endif

682 683 684
##############
# Coq plugin
##############
685

686
ifeq (@enable_coq_support@,yes)
687

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

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

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

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

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

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

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

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

734
endif
735

736 737 738
########
# Tptp2why
########
739

740
ifeq (@enable_whytptp@,yes)
741

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

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

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

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

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

# build targets

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

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

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

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

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

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

793
endif
794

795 796 797 798
#######
# tools
#######

799
TOOLS = bin/why3-cpulimit
800 801 802

byte opt: $(TOOLS)

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

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

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

812 813 814 815
#########
# why3doc
#########

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

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

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

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

848 849
# depend and clean targets

850 851
WHY3DOCGENERATED=src/why3doc/to_html.ml

852 853
include .depend.why3doc

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

depend: .depend.why3doc

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

866 867
install_local: bin/why3doc

868 869 870 871
########
# bench
########

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

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

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

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

###############
893
# test targets
894
###############
895

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

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

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
931
test-api: src/why.cma
932
	ocaml $(EXTCMA)	src/why.cma -I src examples/use_api.ml \
MARCHE Claude's avatar
MARCHE Claude committed
933
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
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 1100 1101 1102 1103 1104

# %_why.v: %.mlw $(BINARY)
# 	$(BINARY) -coq $*.mlw

# %_why.pvs: %.mlw $(BINARY)
# 	$(BINARY) -pvs $*.mlw

# Emacs tags
############

tags:
Francois Bobot's avatar
 
Francois Bobot committed
1105
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1106 1107 1108 1109
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
1110
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1111 1112 1113 1114
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags: