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

338
%.gui: %.mlw bin/whyide.opt
339
	bin/whyide.opt $*.mlw
340

341
install_no_local::
342
	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
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 391 392 393

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

394
install_no_local::
395 396 397
	cp -f bin/whyconfig.@OCAMLBEST@ $(BINDIR)/why3config


MARCHE Claude's avatar
MARCHE Claude committed
398 399 400 401
###############
# IDE
###############

402 403
ifeq (@enable_ide@,yes)

404
IDE_FILES = gconfig scheduler db gmain
MARCHE Claude's avatar
MARCHE Claude committed
405 406 407 408 409 410 411 412

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

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

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

415
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
416

417 418
byte: bin/whyide.byte
opt:  bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
419

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

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

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

# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

448
install_no_local::
449 450
	cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide

451
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
452

453

454 455 456 457
###############
# BENCH
###############

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

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

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

523
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
524

525 526
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
527

528 529
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
530

531
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
532 533
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

534
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
535 536
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

537 538 539 540
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
541

542 543 544 545 546 547 548 549 550 551 552 553 554 555
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

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

François Bobot's avatar
François Bobot committed
564
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
565

566
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
567 568 569 570 571 572

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

573 574
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
575 576 577

# build targets

François Bobot's avatar
François Bobot committed
578 579
plugins.byte byte: plugins/whytptp.cmo
plugins.opt  opt :  plugins/whytptp.cmxs
580

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

François Bobot's avatar
François Bobot committed
584 585 586 587
plugins:
	@mkdir plugins

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

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

François Bobot's avatar
François Bobot committed
601 602 603 604 605 606

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


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

624
endif
625 626 627 628
#######
# tools
#######

629
TOOLS = bin/why3-cpulimit
630 631 632

byte opt: $(TOOLS)

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

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

639
install_no_local::
640 641
	cp -f bin/why3-cpulimit $(BINDIR)

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 683 684 685
#########
# 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

686 687 688 689
########
# bench
########

François Bobot's avatar
François Bobot committed
690
.PHONY: bench test comp_bench_plugins
691

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

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

###############
710
# test targets
711
###############
712

713 714 715
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

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

735
testl: bin/whyml.byte
736
	ocamlrun -bt bin/whyml.byte tests/test-pgm-jcf.mlw
737
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
738

739
testl-debug: bin/whyml.byte
740
	ocamlrun -bt bin/whyml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
741

742 743 744
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

745
testl-type: bin/whyml.byte
746
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
747

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

752 753

## Examples : Plugins ##
754
ifeq (@enable_plugins@,yes)
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 790 791 792
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
793
endif
794

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
795 796 797
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
798

MARCHE Claude's avatar
MARCHE Claude committed
799 800
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
801

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

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

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

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

814 815
.PHONY:$(DOC)

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

819 820
# 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
821

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
822
clean::
823
	cd doc; rubber -d --clean manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
824

825
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
826
# API DOC
827
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
828

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
829 830
.PHONY: apidoc

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

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

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

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

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

854 855
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
856

857
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
858
# generic rules
859
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
860

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

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

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

870
%.cmxs: %.ml
871
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
872

Andrei Paskevich's avatar
Andrei Paskevich committed
873
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
874 875
	$(OCAMLLEX) $<

876
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
877 878
	$(OCAMLYACC) -v $<

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

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

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

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

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

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

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

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

otags:
917 918
	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
919

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
932 933 934
# distrib
#########

935 936 937 938
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

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

redistrib: rmdistrib distrib

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

1024
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1025
# file headers
1026 1027
###############

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1028
headers:
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1029
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
1030 1031 1032
	    Makefile.in configure.in src/*.ml* src/*/*.ml* \
	    src/tools/cpulimit.c

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

1034
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1035
# myself
1036
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
1037

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1038
Makefile: Makefile.in config.status
1039
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1040

1041
src/config.sh: src/config.sh.in config.status
1042
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1043

1044
src/config.ml: src/config.sh
1045
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
1046

Andrei Paskevich's avatar
Andrei Paskevich committed
1047
doc/version.tex: doc/version.tex.in config.status
1048
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1049 1050

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

François Bobot's avatar
META  
François Bobot committed
1053 1054 1055 1056 1057
opt byte : META

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1058
configure: configure.in
1059
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1060

1061
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1062
# clean and depend
1063
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1064

1065
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1066

1067
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
1068 1069
	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
1070

1071 1072 1073 1074
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1075 1076 1077 1078 1079 1080 1081
#################################################################
# Building the Why platform with ocamlbuild (OCaml 3.10 needed) #
#################################################################

# There used to be targets here but they are no longer useful.

# To build using Ocamlbuild:
1082
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1083 1084 1085 1086 1087 1088 1089 1090
# are generated.
# 2) Run Ocamlbuild with any target to generate the sanitization script.
# 3) Run ./sanitize to delete the generated files that shouldn't be generated
# (i.e. all lexers and parsers).
# 4) Run Ocamlbuild with the target you need, for example:
# ocamlbuild jc/jc_main.native

# You can also use the Makefile ./build.makefile which has some handy targets.