Makefile.in 28.3 KB
Newer Older
1

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
2 3
##########################################################################
#                                                                        #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
4
#  Copyright (C) 2010-                                                   #
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7
#    François Bobot                                                     #
#    Jean-Christophe Filliâtre                                          #
#    Claude Marché                                                      #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
8
#    Andrei Paskevich                                                    #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
9 10 11
#                                                                        #
#  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
12
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
13 14 15 16 17 18 19 20
#  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
21
include Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
22

23 24 25 26 27 28
VERBOSEMAKE ?= @enable_verbose_make@

ifeq ($(VERBOSEMAKE),yes)
  QUIET =
else
  QUIET = yes
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
29 30
endif

31
# install the binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32
DESTDIR =
33

34
prefix	    = @prefix@
35 36 37 38 39
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
40
DATADIR = $(DESTDIR)@datarootdir@
41
MANDIR  = $(DESTDIR)@mandir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
42

Andrei Paskevich's avatar
Andrei Paskevich committed
43
# OS specific stuff
44 45
EXE   = @EXE@
STRIP = @STRIP@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46 47

# other variables
48 49 50 51 52 53 54 55 56 57
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@

58 59
CAMLP5O   = @CAMLP5O@

60 61 62 63 64 65
ifeq (@enable_menhirlib@,yes)
  MENHIR = @MENHIR@ --table
else
  MENHIR = @MENHIR@
endif

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

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

77 78
BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -dtypes    -I src $(INCLUDES)
79

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

85 86
# external libraries common to all binaries

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

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
92

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

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

99
.PHONY: byte opt clean depend all install install_no_local
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100

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

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

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

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

115
LIB_PARSER = ptree denv typing parser lexer
116

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

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

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

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

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

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

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

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

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

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

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

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

174
# build targets
175

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

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

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

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

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

# depend target
192

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

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

depend: .depend.lib

200 201
# clean target

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

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

MARCHE Claude's avatar
MARCHE Claude committed
237 238 239
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
240
	cp -f META  $(OCAMLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
241 242
	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi

243 244
ifeq ("@ENABLE_LOCAL@","no")
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
245
install-lib: install_no_local_lib
246
else
MARCHE Claude's avatar
MARCHE Claude committed
247
install install-lib:
248 249 250 251
	@echo "You use a local configuration you can't install with it."
	@echo "Run ./configure without --enable-local"
endif

MARCHE Claude's avatar
MARCHE Claude committed
252 253
install-all: install install-lib

254

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

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

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

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

271 272
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
273

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

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

281 282 283
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284

285
PGMGENERATED = 
Francois Bobot's avatar
Francois Bobot committed
286

287 288
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
289

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

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

297
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
298 299

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

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

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

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

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
314 315

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
320 321 322
depend: .depend.programs

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

330 331
# test target

332 333 334
%.gui: %.why bin/whyide.opt
	bin/whyide.opt $*.why

335 336 337
%: %.mlw bin/whyml.opt
	bin/whyml.opt $*.mlw

François Bobot's avatar
François Bobot committed
338 339 340 341

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

342
%.gui: %.mlw bin/whyide.opt
343
	bin/whyide.opt $*.mlw
344

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

348 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

########
# 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

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


MARCHE Claude's avatar
MARCHE Claude committed
402 403 404 405
###############
# IDE
###############

406 407
ifeq (@enable_ide@,yes)

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

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

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

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

419
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
420

421 422
byte: bin/whyide.byte
opt:  bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
423

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

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

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

# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

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

455
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
456

457

458 459 460 461
###############
# BENCH
###############

462
BENCH_FILES = bench benchrc whybench
463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509

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

510 511 512
##############
# Coq plugin
##############
513
ifeq (@enable_coq_support@,yes)
514 515 516 517 518 519 520 521 522 523 524 525 526
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))

527
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
528

529 530
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
531

532 533
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
534

535
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
536 537
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

538
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
539 540
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

541 542 543 544
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
545

546 547 548 549 550 551 552 553 554 555 556 557 558 559
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

560
endif
561 562 563
########
# Tptp2why
########
564
ifeq (@enable_whytptp@,yes)
565 566
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
567

François Bobot's avatar
François Bobot committed
568
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
569

570
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
571 572 573 574 575 576

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

577 578
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
579 580 581

# build targets

François Bobot's avatar
François Bobot committed
582 583
plugins.byte byte: plugins/whytptp.cmo
plugins.opt  opt :  plugins/whytptp.cmxs
584

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

François Bobot's avatar
François Bobot committed
588 589 590 591
plugins:
	@mkdir plugins

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

François Bobot's avatar
François Bobot committed
595
src/tptp2why/whytptp.cmo: $(TPTPCMO)
596
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
597 598 599 600 601 602 603
	    $(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 $@
604

François Bobot's avatar
François Bobot committed
605 606 607 608 609 610

install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/plugins


611 612 613 614 615 616 617 618 619 620 621 622 623
# 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/*~
624
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
625
	rm -f bin/whytptp.byte bin/whytptp.opt
626 627
	rm -f .depend.tptp2why

628
endif
629 630 631 632
#######
# tools
#######

633
TOOLS = bin/why3-cpulimit
634 635 636

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
637
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
638
	$(CC) -Wall -o $@ $^
639 640

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

643
install_no_local::
644 645
	cp -f bin/why3-cpulimit $(BINDIR)

646 647 648 649 650 651 652 653 654 655 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
#########
# 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

690 691 692 693
########
# bench
########

François Bobot's avatar
François Bobot committed
694
.PHONY: bench test comp_bench_plugins
695

MARCHE Claude's avatar
MARCHE Claude committed
696
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
697
	sh bench/bench \
698
	    "bin/why.@OCAMLBEST@" \
699
	    "bin/whyml.@OCAMLBEST@"
700

701
BENCH_PLUGINS_CMO := helloworld.cmo
702 703 704
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
705 706 707 708 709 710 711
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
712 713

###############
714
# test targets
715
###############
716

717 718 719
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

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

739
testl: bin/whyml.byte
740
	ocamlrun -bt bin/whyml.byte tests/test-pgm-jcf.mlw
741
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
742

743
testl-debug: bin/whyml.byte
744
	ocamlrun -bt bin/whyml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
745

746 747 748
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

749
testl-type: bin/whyml.byte
750
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
751

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

756 757

## Examples : Plugins ##
758
ifeq (@enable_plugins@,yes)
759 760 761 762 763 764 765 766 767 768 769 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
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
797
endif
798

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
799 800 801
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
802

MARCHE Claude's avatar
MARCHE Claude committed
803 804
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
805

806
BNF = qualid constant operator term type formula theory
807
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
808 809 810 811 812 813 814 815

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

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

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

818 819
.PHONY:$(DOC)

820
doc/manual.pdf: $(BNFTEX) doc/apidoc.tex doc/manual.tex doc/version.tex
821
	cd doc; rubber -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
822

823 824
# 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
825

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
826
clean::
827
	cd doc; rubber -d --clean manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
828

829
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
830
# API DOC
831
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
832

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
833 834
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
835
MODULESTODOC = util/util util/hashweak \
836
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
837
	core/env core/task \
MARCHE Claude's avatar
MARCHE Claude committed
838 839 840
	driver/whyconf driver/driver 
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
841 842 843

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

844
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
845
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
846
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
847
		$(LIBINCLUDES) -I src $(FILESTODOC)
848
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
849

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

MARCHE Claude's avatar
MARCHE Claude committed
853
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
854
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
855
		$(LIBINCLUDES) -I src $(FILESTODOC)
856
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
857

858 859
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
860

861
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
862
# generic rules
863
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
864

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

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

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

874
%.cmxs: %.ml
875
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
876

Andrei Paskevich's avatar
Andrei Paskevich committed
877
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
878 879
	$(OCAMLLEX) $<

880
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
881 882
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
892 893 894 895 896 897 898 899
# 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
900 901 902 903 904 905 906 907 908 909 910

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
911
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
912 913 914 915
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
916
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
917 918 919 920
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
921 922
	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
923

924 925 926 927 928
# 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
929
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
930
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
931

932
dep: depend
933
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
934
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
935

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
936 937 938
# distrib
#########

939 940 941 942
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

MARCHE Claude's avatar
MARCHE Claude committed
943
# CHANGES (not up-to-date, moreover is in French)
MARCHE Claude's avatar
MARCHE Claude committed
944
DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
MARCHE Claude's avatar
MARCHE Claude committed
945
      README INSTALL OCAML-LICENSE LICENSE \
946 947 948 949
      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
950
      examples/*.why examples/programs/*.mlw examples/tptp/*.why \
MARCHE Claude's avatar
MARCHE Claude committed
951
      examples/my_cosine/*.v \
952
      theories/*.why theories/*/*.why \
953
      modules/*.mlw \
954 955 956 957 958 959 960 961 962
      share/*.conf \
      share/emacs/why.el share/images/*.png share/lang/*.lang

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

distrib:: $(DISTRIB_TAR)

MARCHE Claude's avatar
MARCHE Claude committed
963 964 965 966 967
rmdistrib: 
	rm -rf $(DISTRIB_DIR)

redistrib: rmdistrib distrib

968 969 970 971 972 973 974 975 976 977
$(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
	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
978
# distrib export: source export-doc export-www export-examples export-examples-c linux
979
#
Andrei Paskevich's avatar
Andrei Paskevich committed
980 981 982
# 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
983
# 	$(MAKE) -C /users/demons/filliatr/www/why install
984 985 986
#
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
987 988
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
989
# 	$(MAKE) export/$(NAME).tar.gz
990
#
Andrei Paskevich's avatar
Andrei Paskevich committed
991
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
992
#
Andrei Paskevich's avatar
Andrei Paskevich committed
993 994
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
995
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
996
# 	echo "*** faire make all dans $(WWW)/examples ***"
997
#
Andrei Paskevich's avatar
Andrei Paskevich committed
998 999 1000 1001 1002 1003
# 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