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 226 227 228 229
	mkdir -p $(DATADIR)/why3/theories
	mkdir -p $(DATADIR)/why3/theories/transform
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
	cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
	cp -f drivers/*.drv $(DATADIR)/why3/drivers
230 231
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
232
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
233 234
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

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

241 242
ifeq ("@ENABLE_LOCAL@","no")
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
243
install-lib: install_no_local_lib
244
else
MARCHE Claude's avatar
MARCHE Claude committed
245
install install-lib:
246 247 248 249
	@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
250 251
install-all: install install-lib

252

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

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

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

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

269 270
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
271

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

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

279 280 281
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282

283 284
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
	       src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
285

286
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer \
287
	    pgm_types pgm_module pgm_wp pgm_env pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
288

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

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

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

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

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

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

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

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

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

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

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

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

329 330
# test target

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

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

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

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

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

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


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

398 399
ifeq (@enable_ide@,yes)

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

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

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

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

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

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

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

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

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

# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

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

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

449

450 451 452 453
###############
# BENCH
###############

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

# build targets

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

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

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

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

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

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

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


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

620
endif
621 622 623 624
#######
# tools
#######

625
TOOLS = bin/why3-cpulimit
626 627 628

byte opt: $(TOOLS)

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

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

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

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

682 683 684 685
########
# bench
########

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

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

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

###############
706
# test targets
707
###############
708

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

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

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

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

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

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

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

748 749

## Examples : Plugins ##
750
ifeq (@enable_plugins@,yes)
751 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
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
789
endif
790

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

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

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

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

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

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

810 811
.PHONY:$(DOC)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

redistrib: rmdistrib distrib

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

1019
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1020
# file headers
1021 1022
###############

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1023
headers:
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1024
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
1025 1026 1027
	    Makefile.in configure.in src/*.ml* src/*/*.ml* \
	    src/tools/cpulimit.c

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

1029
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1030
# myself
1031
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
1032

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1033
Makefile: Makefile.in config.status
1034
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1035

1036
src/config.sh: src/config.sh.in config.status
1037
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1038

1039
src/config.ml: src/config.sh
1040
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
1041

Andrei Paskevich's avatar
Andrei Paskevich committed
1042
doc/version.tex: doc/version.tex.in config.status
1043
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1044 1045

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

François Bobot's avatar
META  
François Bobot committed
1048 1049 1050 1051 1052
opt byte : META

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1053
configure: configure.in
1054
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1055

1056
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1057
# clean and depend
1058
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1059

1060
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1061

1062
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
1063 1064
	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
1065

1066 1067 1068 1069
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1070 1071 1072 1073 1074 1075 1076
#################################################################
# 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:
1077
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1078 1079 1080 1081 1082 1083 1084 1085
# 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.