Makefile.in 28.2 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
PGM_FILES = pgm_ttree \
288
	    pgm_types 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 335
%.gui: %.why bin/whyide.opt
	bin/whyide.opt $*.why

%.gui: %.mlw bin/whyide.opt
336
	bin/whyide.opt $*.mlw
337

338
install_no_local::
339
	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
340

341 342 343 344 345 346 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

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

391
install_no_local::
392 393 394
	cp -f bin/whyconfig.@OCAMLBEST@ $(BINDIR)/why3config


MARCHE Claude's avatar
MARCHE Claude committed
395 396 397 398
###############
# IDE
###############

399 400
ifeq (@enable_ide@,yes)

401
IDE_FILES = gconfig scheduler db gmain
MARCHE Claude's avatar
MARCHE Claude committed
402 403 404 405 406 407 408 409

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

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

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

412
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
413

414 415
byte: bin/whyide.byte
opt:  bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
416

417
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
418
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
419
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
420

421
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
422
	$(if $(QUIET), @echo 'Linking  $@' &&) \
423
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
424 425
	$(STRIP) $@

426
bin/whyide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
427
	$(if $(QUIET),@echo 'Linking  $@' &&) \
428
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
429 430 431 432 433 434

# depend and clean targets

include .depend.ide

.depend.ide:
435
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
436 437 438 439 440 441

depend: .depend.ide

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

445
install_no_local::
446 447
	cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide

448
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
449

450

451 452 453 454
###############
# BENCH
###############

455
BENCH_FILES = bench benchrc whybench
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

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

503 504 505
##############
# Coq plugin
##############
506
ifeq (@enable_coq_support@,yes)
507 508 509 510 511 512 513 514 515 516 517 518 519
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))

520
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
521

522 523
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
524

525 526
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
527

528
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
529 530
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

531
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
532 533
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

534 535 536 537
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
538

539 540 541 542 543 544 545 546 547 548 549 550 551 552
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

553
endif
554 555 556
########
# Tptp2why
########
557
ifeq (@enable_whytptp@,yes)
558 559
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
560

François Bobot's avatar
François Bobot committed
561
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
562

563
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
564 565 566 567 568 569

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

570 571
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
572 573 574

# build targets

François Bobot's avatar
François Bobot committed
575 576
plugins.byte byte: plugins/whytptp.cmo
plugins.opt  opt :  plugins/whytptp.cmxs
577

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

François Bobot's avatar
François Bobot committed
581 582 583 584
plugins:
	@mkdir plugins

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

François Bobot's avatar
François Bobot committed
588
src/tptp2why/whytptp.cmo: $(TPTPCMO)
589
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
590 591 592 593 594 595 596
	    $(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 $@
597

François Bobot's avatar
François Bobot committed
598 599 600 601 602 603

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


604 605 606 607 608 609 610 611 612 613 614 615 616
# 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/*~
617
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
618
	rm -f bin/whytptp.byte bin/whytptp.opt
619 620
	rm -f .depend.tptp2why

621
endif
622 623 624 625
#######
# tools
#######

626
TOOLS = bin/why3-cpulimit
627 628 629

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
630
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
631
	$(CC) -Wall -o $@ $^
632 633

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

636
install_no_local::
637 638
	cp -f bin/why3-cpulimit $(BINDIR)

639 640 641 642 643 644 645 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
#########
# 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

683 684 685 686
########
# bench
########

François Bobot's avatar
François Bobot committed
687
.PHONY: bench test comp_bench_plugins
688

MARCHE Claude's avatar
MARCHE Claude committed
689
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
690
	sh bench/bench \
691
	    "bin/why.@OCAMLBEST@" \
692
	    "bin/whyml.@OCAMLBEST@"
693

694
BENCH_PLUGINS_CMO := helloworld.cmo
695 696 697
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
698 699 700 701 702 703 704
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
705 706

###############
707
# test targets
708
###############
709

710 711 712
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

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

732
testl: bin/whyml.byte
733
	ocamlrun -bt bin/whyml.byte tests/test-pgm-jcf.mlw
734
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
735

736 737 738
testl-debug: bin/whyml.byte
	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw

739 740 741
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

742
testl-type: bin/whyml.byte
743
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
744

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

749 750

## Examples : Plugins ##
751
ifeq (@enable_plugins@,yes)
752 753 754 755 756 757 758 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
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
790
endif
791

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
792 793 794
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
795

MARCHE Claude's avatar
MARCHE Claude committed
796 797
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
798

799
BNF = qualid constant operator term type formula theory
800
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
801 802 803 804 805 806 807 808

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

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

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

811 812
.PHONY:$(DOC)

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

816 817
# 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
818

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
819
clean::
820
	cd doc; rubber -d --clean manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
821

822
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
823
# API DOC
824
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
825

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
826 827
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
828
MODULESTODOC = util/util util/hashweak \
829
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
830
	core/env core/task \
MARCHE Claude's avatar
MARCHE Claude committed
831 832 833
	driver/whyconf driver/driver 
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
834 835 836

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

837
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
838
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
839
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
840
		$(LIBINCLUDES) -I src $(FILESTODOC)
841
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
842

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

MARCHE Claude's avatar
MARCHE Claude committed
846
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
847
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
848
		$(LIBINCLUDES) -I src $(FILESTODOC)
849
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
850

851 852
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
853

854
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
855
# generic rules
856
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
857

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

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

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

867
%.cmxs: %.ml
868
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
869

Andrei Paskevich's avatar
Andrei Paskevich committed
870
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
871 872
	$(OCAMLLEX) $<

873
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
874 875
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
885 886 887 888 889 890 891 892
# 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
893 894 895 896 897 898 899 900 901 902 903

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
904
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
905 906 907 908
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
909
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
910 911 912 913
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
914 915
	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
916

917 918 919 920 921
# 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
922
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
923
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
924

925
dep: depend
926
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
927
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
928

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
929 930 931
# distrib
#########

932 933 934 935
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

MARCHE Claude's avatar
MARCHE Claude committed
936
# CHANGES (not up-to-date, moreover is in French)
MARCHE Claude's avatar
MARCHE Claude committed
937
DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
MARCHE Claude's avatar
MARCHE Claude committed
938
      README INSTALL OCAML-LICENSE LICENSE \
939 940 941 942
      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
943
      examples/*.why examples/programs/*.mlw examples/tptp/*.why \
MARCHE Claude's avatar
MARCHE Claude committed
944
      examples/my_cosine/*.v \
945
      theories/*.why theories/*/*.why \
946
      modules/*.mlw \
947 948 949 950 951 952 953 954 955
      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
956 957 958 959 960
rmdistrib: 
	rm -rf $(DISTRIB_DIR)

redistrib: rmdistrib distrib

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