Makefile.in 29.6 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3
#  Copyright (C) 2010-                                                   #
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
#    François Bobot                                                     #
#    Jean-Christophe Filliâtre                                          #
#    Claude Marché                                                      #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
#    Andrei Paskevich                                                    #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8 9 10
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
11
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12 13 14 15 16 17 18 19
#  described in file LICENSE.                                            #
#                                                                        #
#  This software is distributed in the hope that it will be useful,      #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
#                                                                        #
##########################################################################

Andrei Paskevich's avatar
Andrei Paskevich committed
20
include Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

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

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

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

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

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

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

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

57 58
CAMLP5O   = @CAMLP5O@

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

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

73 74
RUBBER = @RUBBER@

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

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

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

86 87
# external libraries common to all binaries

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

EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93

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

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

100 101 102 103 104
ifeq (@enable_local@,yes)
all: install_local
endif

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106
#############
107
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109

110
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
111 112
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
113
	       src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114

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

118
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
119

120
LIB_PARSER = ptree denv typing parser lexer
121

122
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
123
	     whyconf autodetection
124

125
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
126
		inlining split_goal \
127
		eliminate_definition eliminate_algebraic \
128
		eliminate_inductive eliminate_let eliminate_if \
129
		encoding_enumeration encoding encoding_decorate_mono \
130
		libencoding encoding_decorate encoding_bridge \
François Bobot's avatar
François Bobot committed
131
		encoding_explicit encoding_guard encoding_sort \
132
		encoding_instantiate simplify_array filter_trigger \
133
		encoding_arrays \
134
		introduction abstraction close_epsilon lift_epsilon
135

136
LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa
137

138 139 140 141 142 143
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)) \
144
	      $(addprefix src/printer/, $(LIB_PRINTER))
145

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

149 150
ifeq (@enable_hypothesis_selection@,yes)
	LIB_TRANSFORM += hypothesis_selection
151
	INCLUDES += -I +ocamlgraph
152 153 154
	EXTLIBS += ocamlgraph/graph
endif

155 156 157 158
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
159

160
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
161
$(LIBCMX): OFLAGS += -for-pack Why
162

163
LIB_PARSER_POSTLUDE = \
164
  "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"
165 166

LIB_PARSER_INTERFACE = \
167 168
  -e "s/^val  *logic_file_eof *:/val logic_file_eof : Env.env ->/" \
  -e "s/^val  *list0_decl_eof *:/val list0_decl_eof : Env.env -> \
169 170
  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"

171 172
src/parser/parser.ml: src/parser/parser.pre.ml
	cp src/parser/parser.pre.ml src/parser/parser.ml
173
	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
174 175 176

src/parser/parser.mli: src/parser/parser.pre.mli
	sed $(LIB_PARSER_INTERFACE) src/parser/parser.pre.mli > \
177
					src/parser/parser.mli
178

179
# build targets
180

181 182
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183

184
src/why.cma: src/why.cmo
185 186
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

187
src/why.cmxa: src/why.cmx
188 189
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

190 191
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
192

193 194 195 196
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
197

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198 199
include .depend.lib

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

depend: .depend.lib

205 206
# clean target

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

220 221 222
###############
# installation
###############
223

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

MARCHE Claude's avatar
MARCHE Claude committed
243 244 245
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
	cp -f src/why.cm* $(OCAMLLIB)/why3
246
	cp -f META $(OCAMLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
247 248
	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi

249 250 251 252 253
ifeq (@enable_local@,yes)
install install-lib:
	@echo "Why is configured in local installation mode."
	@echo "To install Why, run ./configure --disable-local ; make ; make install"
else
254
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
255
install-lib: install_no_local_lib
256 257
endif

MARCHE Claude's avatar
MARCHE Claude committed
258 259
install-all: install install-lib

260

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261
##################
262
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263 264
##################

265 266
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267

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

273
bin/why3.byte: src/why.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
274 275
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
276

277 278 279
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

280 281
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
282

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
283
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
284
	rm -f src/main.cm[iox] src/main.annot src/main.o
285
	rm -f bin/why3.byte bin/why3.opt bin/why3
286

287
install_no_local::
288 289 290
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3

install_local: bin/why3
291

292 293 294
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
295

296 297
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
298

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

301 302 303 304 305
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

306
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
307 308

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

310 311
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312

313
bin/why3ml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
314 315
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316 317
	$(STRIP) $@

318
bin/why3ml.byte: src/why.cma $(PGMCMO) src/main.cmo
319 320 321
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

322 323 324
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

325
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326 327

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

329
.depend.programs:
330
	$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332 333 334
depend: .depend.programs

clean::
335 336
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
337
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
338
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
339

340 341
# test target

342 343
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
344

345 346
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
347

348 349
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
350

351 352
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
353

354
install_no_local::
355
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
356

357
install_local: bin/why3ml
358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375

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

376 377
byte: bin/why3config.byte
opt:  bin/why3config.opt
378

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

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

388 389 390
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

391 392 393 394 395 396 397 398 399 400 401 402 403
# 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
404
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
405 406 407
	rm -f .why.conf
	rm -f .depend.config

408 409
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
410
		--detect --conf_file why.conf
411

412
install_no_local::
413
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
414

415
install_local: bin/why3config
416

MARCHE Claude's avatar
MARCHE Claude committed
417 418 419 420
###############
# IDE
###############

421 422
ifeq (@enable_ide@,yes)

423
IDE_FILES = gconfig worker scheduler db dbsync gmain
MARCHE Claude's avatar
MARCHE Claude committed
424 425 426 427 428 429 430 431

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

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

432
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide -I @SQLITE3LIB@
MARCHE Claude's avatar
MARCHE Claude committed
433

434
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
435

436 437
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
438

439
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -thread -I +threads -I @LABLGTK2LIB@ -I @SQLITE3LIB@
440 441
bin/why3ide.opt bin/why3ide.byte: EXTOBJS += gtkThread
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
442

443
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
444
	$(if $(QUIET), @echo 'Linking  $@' &&) \
445
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
446 447
	$(STRIP) $@

448
bin/why3ide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
449
	$(if $(QUIET),@echo 'Linking  $@' &&) \
450
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
451

452 453 454
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
455 456 457 458 459
# depend and clean targets

include .depend.ide

.depend.ide:
460
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
461 462 463 464 465 466

depend: .depend.ide

clean::
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
467
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
468 469
	rm -f .depend.ide

470
install_no_local::
471 472 473
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
474

475
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
476

477

478
###############
479
# Bench
480 481
###############

482 483
ifeq (@enable_bench@,yes)

484
BENCH_FILES = bench benchrc benchdb whybench
485 486 487

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

488
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
489 490 491 492 493 494

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

495
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
496 497 498

# build targets

499 500
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
501

502 503
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I +sqlite3
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
504

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

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

514 515 516
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

517 518 519 520 521 522 523 524 525 526 527 528
# 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/*~
529
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
530 531 532
	rm -f .depend.bench

install_no_local::
533 534 535
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
536

537 538
endif

539 540 541
##############
# Coq plugin
##############
542

543
ifeq (@enable_coq_support@,yes)
544

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

558
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
559

560 561
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
562

563 564
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
565

566
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
567 568
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

569
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
570 571
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

572 573 574 575
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
576

577 578 579 580 581 582 583 584 585 586 587 588 589 590
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

591
endif
592

593 594 595
########
# Tptp2why
########
596

597
ifeq (@enable_whytptp@,yes)
598

599 600
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
601

François Bobot's avatar
François Bobot committed
602
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
603

604
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
605 606 607 608 609 610

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

611 612
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
613 614 615

# build targets

François Bobot's avatar
François Bobot committed
616
plugins.byte byte: plugins/whytptp.cmo
617
plugins.opt  opt : plugins/whytptp.cmxs
618

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

622
plugins/whytptp.cmxs: $(TPTPCMX)
623
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
624
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
625

626
plugins/whytptp.cmo: $(TPTPCMO)
627
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
628 629
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
630 631 632
install_no_local::
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/plugins

633 634 635 636 637 638 639 640 641 642 643 644
# 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
645
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
646
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
647
	rm -f plugins/whytptp.cmxs plugins/whytptp.cmo
648 649
	rm -f .depend.tptp2why

650
endif
651

652 653 654 655
#######
# tools
#######

656
TOOLS = bin/why3-cpulimit
657 658 659

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
660
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
661
	$(CC) -Wall -o $@ $^
662 663

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

666
install_no_local::
667 668
	cp -f bin/why3-cpulimit $(BINDIR)

669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697
#########
# 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) $^

698 699 700
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

701 702 703 704 705 706 707 708 709 710 711 712
# 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/*~
713
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
714 715
	rm -f .depend.why3doc

716 717
install_local: bin/why3doc

718 719 720 721
########
# bench
########

François Bobot's avatar
François Bobot committed
722
.PHONY: bench test comp_bench_plugins
723

724
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
725
	sh bench/bench \
726 727
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
728

729
BENCH_PLUGINS_CMO := helloworld.cmo
730 731 732
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
733 734 735
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
736
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
737 738 739
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
740 741

###############
742
# test targets
743
###############
744

745 746
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
747

748
test: bin/why3.byte plugins.byte $(TOOLS)
749
	mkdir -p output_why3
750 751 752 753 754
	bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
	# bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
	# bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
	# bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
	echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
755
	@printf "*** Checking Coq file generation ***\\n"
756
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
757
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
758 759
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
760
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
761
		; do \
762
	  printf "Generating Coq file for $$i\\n" && \
763
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
764
	@printf "*** Checking Coq compilation ***\\n"
765
	@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
766

767 768 769
testl: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
	ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
770

771 772
testl-debug: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
773

774 775
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
776

777 778
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
779

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

784 785

## Examples : Plugins ##
786

787
ifeq (@enable_plugins@,yes)
788

789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
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
827

828
endif
829

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
830 831 832
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
833

834 835 836 837 838
.PHONY: doc

ifeq (@enable_doc@,yes)

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

841
BNF = qualid constant operator term type formula theory
842
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
843 844 845 846 847 848 849 850

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

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

851 852 853 854
DOC = api glossary ide intro library macros manpages \
      manual starting syntax syntaxref version whyml

DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
855

856
doc/manual.pdf: $(BNFTEX) $(DOCTEX)
857
	cd doc; $(RUBBER) -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
858

859 860
# 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
861

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
862
clean::
863 864 865 866 867 868 869
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

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

871
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
872
# API DOC
873
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
874

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
875 876
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
877
MODULESTODOC = util/util util/hashweak \
878
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
879
	core/env core/task \
880
	driver/whyconf driver/driver
MARCHE Claude's avatar
MARCHE Claude committed
881 882
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
883 884 885

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

886
apidoc: $(FILESTODOC)
887
	mkdir -p doc/apidoc
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
888
	$(OCAMLDOC) -d doc/apidoc -html -keep-code $(INCLUDES) \
889
		$(LIBINCLUDES) -I src $(FILESTODOC)
890
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
891

MARCHE Claude's avatar
MARCHE Claude committed
892
install_apidoc: apidoc
893
	rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
MARCHE Claude's avatar
MARCHE Claude committed
894

MARCHE Claude's avatar
MARCHE Claude committed
895
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
896
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
897
		$(LIBINCLUDES) -I src $(FILESTODOC)
898
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
899

900
clean::
901
	rm -f doc/apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
902

903
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
904
# generic rules
905
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
906

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

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

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

916
%.cmxs: %.ml
917
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
918

Andrei Paskevich's avatar
Andrei Paskevich committed
919
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
920 921
	$(OCAMLLEX) $<

922
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
923 924
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
934 935 936 937 938 939 940 941
# 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
942 943 944 945 946 947 948 949 950 951 952

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
953
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
954 955 956 957
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
958
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
959 960 961 962
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
963 964
	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
965

966 967 968 969 970
# 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
971
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
972
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
973

974
dep: depend
975
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
976
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
977

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
978 979 980
# distrib
#########

981 982 983 984
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

MARCHE Claude's avatar
MARCHE Claude committed
985
# CHANGES (not up-to-date, moreover is in French)
MARCHE Claude's avatar
MARCHE Claude committed
986
DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
MARCHE Claude's avatar
MARCHE Claude committed
987
      README INSTALL OCAML-LICENSE LICENSE \
988 989 990 991
      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
992
      examples/*.why examples/programs/*.mlw examples/tptp/*.why \
MARCHE Claude's avatar
MARCHE Claude committed
993
      examples/my_cosine/*.v \
994
      theories/*.why theories/*/*.why \
995
      modules/*.mlw \
996
      share/provers-detection-data.conf.in \
997 998 999 1000 1001 1002 1003 1004
      share/emacs/why.el share/images/*.png share/lang/*.lang

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

distrib:: $(DISTRIB_TAR)

1005
rmdistrib:
MARCHE Claude's avatar
MARCHE Claude committed
1006 1007 1008 1009
	rm -rf $(DISTRIB_DIR)

redistrib: rmdistrib distrib

1010 1011 1012 1013 1014 1015 1016
$(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
1017
	mkdir -p $(DISTRIB_DIR)/share
1018
	mkdir -p $(DISTRIB_DIR)/plugins
1019 1020 1021
	ln -s ../drivers $(DISTRIB_DIR)/share/drivers
	ln -s ../modules $(DISTRIB_DIR)/share/modules
	ln -s ../theories $(DISTRIB_DIR)/share/theories
1022 1023 1024
	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
1025
# distrib export: source export-doc export-www export-examples export-examples-c linux
1026
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1027 1028 1029
# 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
1030
# 	$(MAKE) -C /users/demons/filliatr/www/why install
1031 1032 1033
#
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
1034 1035
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
1036
# 	$(MAKE) export/$(NAME).tar.gz
1037
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1038
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
1039
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1040 1041
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
1042
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
1043
# 	echo "*** faire make all dans $(WWW)/examples ***"
1044
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1045 1046 1047 1048 1049 1050
# export-examples-c:
# 	mkdir -p $(WWW)/caduceus/examples
# 	cd examples-c; cp --parents */*.c */*.h $(WWW)/ca