Makefile.in 29.4 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 \
François Bobot's avatar
François Bobot committed
116
	   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 \
131
		encoding_explicit encoding_sort \
132
		encoding_instantiate simplify_array filter_trigger \
133
		encoding_arrays \
134
		introduction abstraction close_epsilon lift_epsilon
135

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
136
LIB_PRINTER = print_real alt_ergo why3 smt 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 226 227
	mkdir -p $(BINDIR)
	mkdir -p $(LIBDIR)/why3
	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
François Bobot's avatar
META  
François Bobot committed
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
PGMGENERATED =
Francois Bobot's avatar
Francois Bobot committed
297

298 299
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
300

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

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

308
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
309 310

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

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

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

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

324 325 326
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334 335 336
depend: .depend.programs

clean::
337 338 339
	rm -f $(PGMGENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
340
	rm -f src/programs/*.output src/programs/*.automaton
341
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
342
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343

344 345
# test target

346 347
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
348

349 350
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
351

352 353
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
354

355 356
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
357

358
install_no_local::
359
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
360

361
install_local: bin/why3ml
362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379

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

380 381
byte: bin/why3config.byte
opt:  bin/why3config.opt
382

383
bin/why3config.opt: src/why.cmxa $(CONFIGCMX)
384 385 386 387
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

388
bin/why3config.byte: src/why.cma $(CONFIGCMO)
389 390 391
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

392 393 394
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

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

412 413
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
414
		--detect --conf_file .why.conf
415

416
install_no_local::
417
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
418

419
install_local: bin/why3config
420

MARCHE Claude's avatar
MARCHE Claude committed
421 422 423 424
###############
# IDE
###############

425 426
ifeq (@enable_ide@,yes)

427
IDE_FILES = gconfig worker scheduler db gmain
MARCHE Claude's avatar
MARCHE Claude committed
428 429 430 431 432 433 434 435

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

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

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

438
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
439

440 441
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
442

443 444 445
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
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
446

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

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

456 457 458
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
459 460 461 462 463
# depend and clean targets

include .depend.ide

.depend.ide:
464
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
465 466 467 468 469 470

depend: .depend.ide

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

474
install_no_local::
475 476 477
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
478

479
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
480

481

482 483 484 485
###############
# BENCH
###############

486 487
ifeq (@enable_bench@,yes)

488
BENCH_FILES = bench benchrc whybench
489 490 491

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

492
BENCHMODULES := src/ide/worker src/ide/scheduler $(BENCHMODULES)
493 494 495 496 497 498 499 500 501 502

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

503 504
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
505

506 507
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads
508

509
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
510 511 512 513
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

514
bin/why3bench.byte: src/why.cma  $(PGMCMO) $(BENCHCMO)
515 516 517
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

518 519 520
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

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

install_no_local::
537 538 539
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
540

541 542
endif

543 544 545
##############
# Coq plugin
##############
546

547
ifeq (@enable_coq_support@,yes)
548

549 550 551 552 553 554 555 556 557 558 559 560 561
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))

562
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
563

564 565
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
566

567 568
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
569

570
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
571 572
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

573
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
574 575
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

576 577 578 579
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
580

581 582 583 584 585 586 587 588 589 590 591 592 593 594
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

595
endif
596

597 598 599
########
# Tptp2why
########
600

601
ifeq (@enable_whytptp@,yes)
602

603 604
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
605

François Bobot's avatar
François Bobot committed
606
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
607

608
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
609 610 611 612 613 614

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

615 616
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
617 618 619

# build targets

François Bobot's avatar
François Bobot committed
620
plugins.byte byte: plugins/whytptp.cmo
621
plugins.opt  opt : plugins/whytptp.cmxs
622

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

François Bobot's avatar
François Bobot committed
626 627 628 629
plugins:
	@mkdir plugins

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

François Bobot's avatar
François Bobot committed
633
src/tptp2why/whytptp.cmo: $(TPTPCMO)
634
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
635 636 637 638 639 640 641
	    $(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 $@
642

François Bobot's avatar
François Bobot committed
643 644 645 646
install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/plugins

647 648 649 650 651 652 653 654 655 656 657 658 659
# 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/*~
660
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
661
	rm -f bin/whytptp.byte bin/whytptp.opt
662 663
	rm -f .depend.tptp2why

664
endif
665

666 667 668 669
#######
# tools
#######

670
TOOLS = bin/why3-cpulimit
671 672 673

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
674
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
675
	$(CC) -Wall -o $@ $^
676 677

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

680
install_no_local::
681 682
	cp -f bin/why3-cpulimit $(BINDIR)

683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711
#########
# 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) $^

712 713 714
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

715 716 717 718 719 720 721 722 723 724 725 726
# 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/*~
727
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
728 729
	rm -f .depend.why3doc

730 731
install_local: bin/why3doc

732 733 734 735
########
# bench
########

François Bobot's avatar
François Bobot committed
736
.PHONY: bench test comp_bench_plugins
737

738
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
739
	sh bench/bench \
740 741
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
742

743
BENCH_PLUGINS_CMO := helloworld.cmo
744 745 746
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
747 748 749
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
750
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
751 752 753
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
754 755

###############
756
# test targets
757
###############
758

759 760
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
761

762
test: bin/why3.byte plugins.byte $(TOOLS)
763
	mkdir -p output_why3
764 765 766 767 768
	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
769
	@printf "*** Checking Coq file generation ***\\n"
770
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
771
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
772 773
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
774
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
775
		; do \
776
	  printf "Generating Coq file for $$i\\n" && \
777
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
778
	@printf "*** Checking Coq compilation ***\\n"
779
	@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
780

781 782 783
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
784

785 786
testl-debug: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
787

788 789
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
790

791 792
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
793

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

798 799

## Examples : Plugins ##
800

801
ifeq (@enable_plugins@,yes)
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 827 828 829 830 831 832 833 834 835 836 837 838 839 840
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
841

842
endif
843

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
844 845 846
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
847

848 849 850 851 852
.PHONY: doc

ifeq (@enable_doc@,yes)

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

855
BNF = qualid constant operator term type formula theory
856
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
857 858 859 860 861 862 863 864

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

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

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

867
doc/manual.pdf: $(BNFTEX) doc/*.tex doc/manual.tex doc/version.tex
868
	cd doc; $(RUBBER) -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
869

870 871
# 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
872

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
873
clean::
874 875 876 877 878 879 880
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

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

882
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
883
# API DOC
884
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
885

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
886 887
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
888
MODULESTODOC = util/util util/hashweak \
889
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
890
	core/env core/task \
891
	driver/whyconf driver/driver
MARCHE Claude's avatar
MARCHE Claude committed
892 893
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
894 895 896

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

897
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
898
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
899
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
900
		$(LIBINCLUDES) -I src $(FILESTODOC)
901
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
902

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

MARCHE Claude's avatar
MARCHE Claude committed
906
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
907
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
908
		$(LIBINCLUDES) -I src $(FILESTODOC)
909
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
910

911 912
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
913

914
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
915
# generic rules
916
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
917

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

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

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

927
%.cmxs: %.ml
928
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
929

Andrei Paskevich's avatar
Andrei Paskevich committed
930
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
931 932
	$(OCAMLLEX) $<

933
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
934 935
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
945 946 947 948 949 950 951 952
# 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
953 954 955 956 957 958 959 960 961 962 963

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
964
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
965 966 967 968
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
969
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
970 971 972 973
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
974 975
	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
976

977 978 979 980 981
# 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
982
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
983
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
984

985
dep: depend
986
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
987
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
988

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
989 990 991
# distrib
#########

992 993 994 995
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

MARCHE Claude's avatar
MARCHE Claude committed
996
# CHANGES (not up-to-date, moreover is in French)
MARCHE Claude's avatar
MARCHE Claude committed
997
DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
MARCHE Claude's avatar
MARCHE Claude committed
998
      README INSTALL OCAML-LICENSE LICENSE \
999 1000 1001 1002
      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
1003
      examples/*.why examples/programs/*.mlw examples/tptp/*.why \
MARCHE Claude's avatar
MARCHE Claude committed
1004
      examples/my_cosine/*.v \
1005
      theories/*.why theories/*/*.why \
1006
      modules/*.mlw \
1007
      share/provers-detection-data.conf.in \
1008 1009 1010 1011 1012 1013 1014 1015
      share/emacs/why.el share/images/*.png share/lang/*.lang

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

distrib:: $(DISTRIB_TAR)

1016
rmdistrib:
MARCHE Claude's avatar
MARCHE Claude committed
1017 1018 1019 1020
	rm -rf $(DISTRIB_DIR)

redistrib: rmdistrib distrib

1021 1022 1023 1024 1025 1026 1027
$(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
1028 1029 1030 1031
	mkdir -p $(DISTRIB_DIR)/share
	ln -s ../drivers $(DISTRIB_DIR)/share/drivers
	ln -s ../modules $(DISTRIB_DIR)/share/modules
	ln -s ../theories $(DISTRIB_DIR)/share/theories
1032 1033 1034
	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
1035
# distrib export: source export-doc export-www export-examples export-examples-c linux
1036
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1037 1038 1039
# 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
1040
# 	$(MAKE) -C /users/demons/filliatr/www/why install
1041 1042 1043
#
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
1044 1045
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
1046
# 	$(MAKE) export/$(NAME).tar.gz
1047
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1048
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
1049
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1050 1051
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
1052
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
1053
# 	echo "*** faire make all dans $(WWW)/examples ***"
1054
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1055 1056 1057 1058 1059 1060
# 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
1061
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1062 1063 1064 1065 1066 1067 1068 1069
# 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)
1070
#
Andrei Paskevich's avatar
Andrei Paskevich committed
1071
# OSTYPE  ?= linux
1072
#