Makefile.in 28.6 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 Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -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
.PHONY: byte opt clean depend all install install_no_local
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101

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

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

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

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

116
LIB_PARSER = ptree denv typing parser lexer
117

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

121
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
122
		inlining split_goal \
123
		eliminate_definition eliminate_algebraic \
124
		eliminate_inductive eliminate_let eliminate_if \
125
		encoding_enumeration encoding encoding_decorate_mono \
126
		libencoding encoding_decorate encoding_bridge \
127
		encoding_explicit encoding_sort \
128
		encoding_instantiate simplify_array filter_trigger \
129
		encoding_arrays \
130
		introduction abstraction close_epsilon lift_epsilon
131

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
132
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
133

134 135 136 137 138 139
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)) \
140
	      $(addprefix src/printer/, $(LIB_PRINTER))
141

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

145 146
ifeq (@enable_hypothesis_selection@,yes)
	LIB_TRANSFORM += hypothesis_selection
147
	INCLUDES += -I +ocamlgraph
148 149 150
	EXTLIBS += ocamlgraph/graph
endif

151 152 153 154
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
155

156
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
157
$(LIBCMX): OFLAGS += -for-pack Why
158

159
LIB_PARSER_POSTLUDE = \
160
  "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"
161 162

LIB_PARSER_INTERFACE = \
163 164
  -e "s/^val  *logic_file_eof *:/val logic_file_eof : Env.env ->/" \
  -e "s/^val  *list0_decl_eof *:/val list0_decl_eof : Env.env -> \
165 166
  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"

167 168
src/parser/parser.ml: src/parser/parser.pre.ml
	cp src/parser/parser.pre.ml src/parser/parser.ml
169
	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
170 171 172

src/parser/parser.mli: src/parser/parser.pre.mli
	sed $(LIB_PARSER_INTERFACE) src/parser/parser.pre.mli > \
173
					src/parser/parser.mli
174

175
# build targets
176

177 178
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
179

180
src/why.cma: src/why.cmo
181 182
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

183
src/why.cmxa: src/why.cmx
184 185
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

186 187
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
188

189 190 191 192
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
193

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
194 195
include .depend.lib

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

depend: .depend.lib

201 202
# clean target

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

216 217 218
###############
# installation
###############
219

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

MARCHE Claude's avatar
MARCHE Claude committed
239 240 241
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
	cp -f src/why.cm* $(OCAMLLIB)/why3
François Bobot's avatar
META  
François Bobot committed
242
	cp -f META  $(OCAMLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
243 244
	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi

245 246 247 248 249
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
250
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
251
install-lib: install_no_local_lib
252 253
endif

MARCHE Claude's avatar
MARCHE Claude committed
254 255
install-all: install install-lib

256

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
257
##################
258
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
259 260 261 262 263
##################

byte: bin/why.byte
opt:  bin/why.opt

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

269
bin/why.byte: src/why.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
270 271
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
272

273 274
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
275

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
276
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
277
	rm -f src/main.cm[iox] src/main.annot src/main.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
278
	rm -f bin/why.byte bin/why.opt
279

280
install_no_local::
281 282
	cp -f bin/why.@OCAMLBEST@ $(BINDIR)/why3

283 284 285
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286

287
PGMGENERATED =
Francois Bobot's avatar
Francois Bobot committed
288

289 290
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
291

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

294 295 296 297 298
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

299
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
300 301

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

303 304
byte: bin/whyml.byte
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
305

306
bin/whyml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
307 308
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
309 310
	$(STRIP) $@

311
bin/whyml.byte: src/why.cma $(PGMCMO) src/main.cmo
312 313 314 315
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316 317

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

319
.depend.programs: $(PGMGENERATED)
320
	$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
322 323 324
depend: .depend.programs

clean::
325 326 327
	rm -f $(PGMGENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
328
	rm -f src/programs/*.output src/programs/*.automaton
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
329
	rm -f bin/whyml.byte bin/whyml.opt
330
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331

332 333
# test target

334 335 336
%.gui: %.why bin/whyide.opt
	bin/whyide.opt $*.why

337 338 339
%: %.mlw bin/whyml.opt
	bin/whyml.opt $*.mlw

François Bobot's avatar
François Bobot committed
340 341 342 343

%: %.why bin/why.opt
	bin/why.opt $*.why

344
%.gui: %.mlw bin/whyide.opt
345
	bin/whyide.opt $*.mlw
346

347
install_no_local::
348
	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
349

350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399

########
# Config
########

CONFIG_FILES = whyconfig

CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))

CONFIGML  = $(addsuffix .ml,  $(CONFIGMODULES))
CONFIGMLI = $(addsuffix .mli, $(CONFIGMODULES))
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

$(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs

# build targets

byte: bin/whyconfig.byte
opt:  bin/whyconfig.opt

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

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

# 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
	rm -f bin/whyconfig.byte bin/whyconfig.opt
	rm -f .why.conf
	rm -f .depend.config

local_config: bin/whyconfig.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/whyconfig.@OCAMLBEST@ --autodetect-provers --conf_file .why.conf

400
install_no_local::
401 402 403
	cp -f bin/whyconfig.@OCAMLBEST@ $(BINDIR)/why3config


MARCHE Claude's avatar
MARCHE Claude committed
404 405 406 407
###############
# IDE
###############

408 409
ifeq (@enable_ide@,yes)

410
IDE_FILES = gconfig scheduler db gmain
MARCHE Claude's avatar
MARCHE Claude committed
411 412 413 414 415 416 417 418

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

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

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

421
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
422

423 424
byte: bin/whyide.byte
opt:  bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
425

426
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
427
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
428
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
429

430
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
431
	$(if $(QUIET), @echo 'Linking  $@' &&) \
432
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
433 434
	$(STRIP) $@

435
bin/whyide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
436
	$(if $(QUIET),@echo 'Linking  $@' &&) \
437
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
438 439 440 441 442 443

# depend and clean targets

include .depend.ide

.depend.ide:
444
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
445 446 447 448 449 450

depend: .depend.ide

clean::
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
451
	rm -f bin/whyide.byte bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
452 453
	rm -f .depend.ide

454
install_no_local::
455 456
	cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide

457
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
458

459

460 461 462 463
###############
# BENCH
###############

464 465
ifeq (@enable_bench@,yes)

466
BENCH_FILES = bench benchrc whybench
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 507 508 509 510 511 512 513

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

BENCHMODULES := src/ide/scheduler $(BENCHMODULES)

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

$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I +sqlite3

# build targets

byte: bin/whybench.byte
opt:  bin/whybench.opt

bin/whybench.opt bin/whybench.byte: INCLUDES += -thread -I +threads
bin/whybench.opt bin/whybench.byte: EXTLIBS += threads

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

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

# 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/*~
	rm -f bin/whybench.byte bin/whybench.opt
	rm -f .depend.bench

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

514 515
endif

516 517 518
##############
# Coq plugin
##############
519

520
ifeq (@enable_coq_support@,yes)
521

522 523 524 525 526 527 528 529 530 531 532 533 534
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))

535
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
536

537 538
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
539

540 541
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
542

543
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
544 545
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

546
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
547 548
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

549 550 551 552
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
553

554 555 556 557 558 559 560 561 562 563 564 565 566 567
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

568
endif
569

570 571 572
########
# Tptp2why
########
573

574
ifeq (@enable_whytptp@,yes)
575

576 577
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
578

François Bobot's avatar
François Bobot committed
579
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
580

581
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
582 583 584 585 586 587

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

588 589
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
590 591 592

# build targets

François Bobot's avatar
François Bobot committed
593
plugins.byte byte: plugins/whytptp.cmo
594
plugins.opt  opt : plugins/whytptp.cmxs
595

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

François Bobot's avatar
François Bobot committed
599 600 601 602
plugins:
	@mkdir plugins

src/tptp2why/whytptp.cmxs: $(TPTPCMX)
603
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
604
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
605

François Bobot's avatar
François Bobot committed
606
src/tptp2why/whytptp.cmo: $(TPTPCMO)
607
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
608 609 610 611 612 613 614
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

plugins/whytptp.cmxs: plugins src/tptp2why/whytptp.cmxs
	@cp src/tptp2why/whytptp.cmxs $@

plugins/whytptp.cmo: plugins src/tptp2why/whytptp.cmo
	@cp src/tptp2why/whytptp.cmo $@
615

François Bobot's avatar
François Bobot committed
616 617 618 619
install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/plugins

620 621 622 623 624 625 626 627 628 629 630 631 632
# 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)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
633
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
634
	rm -f bin/whytptp.byte bin/whytptp.opt
635 636
	rm -f .depend.tptp2why

637
endif
638

639 640 641 642
#######
# tools
#######

643
TOOLS = bin/why3-cpulimit
644 645 646

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
647
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
648
	$(CC) -Wall -o $@ $^
649 650

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

653
install_no_local::
654 655
	cp -f bin/why3-cpulimit $(BINDIR)

656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699
#########
# why3doc
#########

WHY3DOC_FILES = doc_html doc_main

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

# depend and clean targets

include .depend.why3doc

.depend.why3doc:
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

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

700 701 702 703
########
# bench
########

François Bobot's avatar
François Bobot committed
704
.PHONY: bench test comp_bench_plugins
705

MARCHE Claude's avatar
MARCHE Claude committed
706
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
707
	sh bench/bench \
708
	    "bin/why.@OCAMLBEST@" \
709
	    "bin/whyml.@OCAMLBEST@"
710

711
BENCH_PLUGINS_CMO := helloworld.cmo
712 713 714
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
715 716 717 718 719 720 721
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
# 	bin/why.byte -D bench/plugins/helloworld.drv \
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
722 723

###############
724
# test targets
725
###############
726

727 728 729
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

François Bobot's avatar
François Bobot committed
730
test: bin/why.byte plugins.byte $(TOOLS)
731
	mkdir -p output_why3
732
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
François Bobot's avatar
François Bobot committed
733 734 735
	# bin/why.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
	# bin/why.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
	# bin/why.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
736
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
737
	@printf "*** Checking Coq file generation ***\\n"
738
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
739
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
740 741
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
742
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
743
		; do \
744
	  printf "Generating Coq file for $$i\\n" && \
745
	  	bin/why.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
746
	@printf "*** Checking Coq compilation ***\\n"
747
	@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
748

749
testl: bin/whyml.byte
750
	ocamlrun -bt bin/whyml.byte tests/test-pgm-jcf.mlw
751
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
752

753
testl-debug: bin/whyml.byte
754
	ocamlrun -bt bin/whyml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
755

756 757 758
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

759
testl-type: bin/whyml.byte
760
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
761

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

766 767

## Examples : Plugins ##
768

769
ifeq (@enable_plugins@,yes)
770

771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808
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
809

810
endif
811

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
812 813 814
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
815

816 817 818 819 820
.PHONY: doc

ifeq (@enable_doc@,yes)

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

823
BNF = qualid constant operator term type formula theory
824
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
825 826 827 828 829 830 831 832

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

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

833
doc: $(DOC)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
834

835
doc/manual.pdf: $(BNFTEX) doc/apidoc.tex doc/manual.tex doc/version.tex
836
	cd doc; $(RUBBER) -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
837

838 839
# 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
840

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
841
clean::
842 843 844 845 846 847 848
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

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

850
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
851
# API DOC
852
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
853

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
854 855
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
856
MODULESTODOC = util/util util/hashweak \
857
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
858
	core/env core/task \
859
	driver/whyconf driver/driver
MARCHE Claude's avatar
MARCHE Claude committed
860 861
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
862 863 864

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

865
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
866
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
867
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
868
		$(LIBINCLUDES) -I src $(FILESTODOC)
869
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
870

MARCHE Claude's avatar
MARCHE Claude committed
871 872 873
install_apidoc: apidoc
	rsync -av apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/

MARCHE Claude's avatar
MARCHE Claude committed
874
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
875
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
876
		$(LIBINCLUDES) -I src $(FILESTODOC)
877
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
878

879 880
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
881

882
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
883
# generic rules
884
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
885

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

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

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

895
%.cmxs: %.ml
896
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
897

Andrei Paskevich's avatar
Andrei Paskevich committed
898
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
899 900
	$(OCAMLLEX) $<

901
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
902 903
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
913 914 915 916 917 918 919 920
# 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
921 922 923 924 925 926 927 928 929 930 931

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
932
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
933 934 935 936
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
937
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
938 939 940 941
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
942 943
	find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags
#	otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
944

945 946 947 948 949
# the previous seems broken. This one is intented for vi(m) users, but could
# be adapted for emacs (remove the -vi option ?)
otags-vi:
	find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags -vi

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
950
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
951
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
952

953
dep: depend
954
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
955
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
956

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
957 958 959
# distrib
#########

960 961 962 963
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

MARCHE Claude's avatar
MARCHE Claude committed
964
# CHANGES (not up-to-date, moreover is in French)
MARCHE Claude's avatar
MARCHE Claude committed
965
DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
MARCHE Claude's avatar
MARCHE Claude committed
966
      README INSTALL OCAML-LICENSE LICENSE \
967 968 969 970
      src/*.ml* src/*/*.ml* src/*/*.c \
      src/config.sh.in \
      doc/version.tex.in doc/manual.pdf \
      drivers/*.drv \
MARCHE Claude's avatar
MARCHE Claude committed
971
      examples/*.why examples/programs/*.mlw examples/tptp/*.why \
MARCHE Claude's avatar
MARCHE Claude committed
972
      examples/my_cosine/*.v \
973
      theories/*.why theories/*/*.why \
974
      modules/*.mlw \
975 976 977 978 979 980 981 982 983
      share/*.conf \
      share/emacs/why.el share/images/*.png share/lang/*.lang

# TODO?
# share/zsh ?
# symbolic links in share/ ?

distrib:: $(DISTRIB_TAR)

984
rmdistrib:
MARCHE Claude's avatar
MARCHE Claude committed
985 986 987 988
	rm -rf $(DISTRIB_DIR)

redistrib: rmdistrib distrib

989 990 991 992 993 994 995
$(DISTRIB_TAR): doc/manual.pdf
	@if test -d $(DISTRIB_DIR); then \
	  echo "Hum... there is already a directory $(NAME)"; \
	  echo "Please increase the version number"; exit 1; \
        fi
	mkdir -p $(DISTRIB_DIR)
	mkdir -p $(DISTRIB_DIR)/bin
996 997 998 999
	mkdir -p $(DISTRIB_DIR)/share
	ln -s ../drivers $(DISTRIB_DIR)/share/drivers
	ln -s ../modules $(DISTRIB_DIR)/share/modules
	ln -s ../theories $(DISTRIB_DIR)/share/theories
1000 1001 1002
	cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR)
	cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar

Andrei Paskevich's avatar
Andrei Paskevich committed
1003
# distrib export: source export-doc export-www export-examples export-examples-c linux
1004
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1005 1006 1007
# export-www:
# 	echo "<#def version>$(VERSION)</#def>" > /users/demons/filliatr/www/why/version.prehtml
# 	echo "<#def cversion>$(CVERSION)</#def>" >> /users/demons/filliatr/www/why/version.prehtml
1008
# 	$(MAKE) -C /users/demons/filliatr/www/why install
1009 1010 1011
#
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
1012 1013
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
1014
# 	$(MAKE) export/$(NAME).tar.gz
1015
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1016
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
1017
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1018 1019
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
1020
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
1021
# 	echo "*** faire make all dans $(WWW)/examples ***"
1022
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1023 1024 1025 1026 1027 1028
# export-examples-c:
# 	mkdir -p $(WWW)/caduceus/examples
# 	cd examples-c; cp --parents */*.c */*.h $(WWW)/caduceus/examples
# 	mkdir -p $(WWW)/caduceus/examples/bench
# 	cp bench/c/good/*.c $(WWW)/caduceus/examples/bench
# 	rm -f $(WWW)/caduceus/examples/bench/test.c
1029
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1030 1031 1032 1033 1034 1035 1036 1037
# export-doc: $(DOC)
# 	cp doc/manual.ps doc/manual.html $(WWW)/manual
# 	cp doc/logic_syntax.bnf $(WWW)/manual
# 	(cd $(WWW)/manual; hacha manual.html)
# 	cp doc/caduceus.ps doc/caduceus.html $(WWW)/caduceus/manual
# 	(cd $(WWW)/caduceus/manual; hacha caduceus.html)
# 	cp doc/krakatoa.pdf doc/krakatoa.html $(WWWKRAKATOA)/manual
# 	(cd $(WWWKRAKATOA)/manual; hacha krakatoa.html)
1038
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1039
# OSTYPE  ?= linux
1040
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1041
# BINARYNAME = $(NAME)-$(OSTYPE)
1042
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1043
# linux: binary
1044 1045 1046
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1047 1048 1049 1050 1051
# binary: $(ALLBINARYFILES)
# 	mkdir -p export/$(BINARYNAME)
# 	cp --parents $(ALLBINARYFILES) export/$(BINARYNAME)
# 	(cd export; tar czf $(BINARYNAME).tar.gz $(BINARYNAME))
# 	cp export/$(BINARYNAME).tar.gz $(FTP)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1052

1053
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1054
# file headers
1055 1056
###############

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1057
headers:
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1058
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
1059 1060 1061
	    Makefile.in configure.in src/*.ml* src/*/*.ml* \
	    src/tools/cpulimit.c

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1062

1063
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1064
# myself
1065
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
1066

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1067
Makefile: Makefile.in config.status
1068
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1069

1070
src/config.sh: src/config.sh.in config.status
1071
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1072

1073
src/config.ml: src/config.sh
1074
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
1075

Andrei Paskevich's avatar
Andrei Paskevich committed
1076
doc/version.tex: doc/version.tex.in config.status
1077
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1078 1079

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1080 1081
	./config.status --recheck

François Bobot's avatar
META  
François Bobot committed
1082 1083 1084 1085 1086
opt byte : META

META: META.in config.status
	./config.status chmod --file $@

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1087
configure: configure.in
1088
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1089

1090
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1091
# clean and depend
1092
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1093

1094
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1095

1096
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
1097 1098
	rm -f config.status config.cache config.log \
	    Makefile src/config.ml doc/version.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1099

1100 1101 1102 1103
depend:
	rm -f $^
	$(MAKE) $^

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