Makefile.in 30.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 Aer-29 -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aer-29 -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_distinction \
130
		encoding_enumeration encoding encoding_decorate_mono \
131 132
		libencoding encoding_select \
		encoding_decorate encoding_bridge \
François Bobot's avatar
François Bobot committed
133
		encoding_explicit encoding_guard encoding_sort \
134
		encoding_instantiate simplify_array filter_trigger \
135
		introduction abstraction close_epsilon lift_epsilon
136

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

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

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

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

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

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

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

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

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

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

180
# build targets
181

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

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

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

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

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

# depend target
198

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

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

depend: .depend.lib

206 207
# clean target

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

221 222 223
###############
# installation
###############
224

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

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

250 251 252 253 254
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
255
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
256
install-lib: install_no_local_lib
257 258
endif

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

261

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

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

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

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

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

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

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

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

install_local: bin/why3
292

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

341 342
# test target

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

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

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

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

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

358
install_local: bin/why3ml
359

360 361 362 363
##########
# gallery
##########

364
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
365
        power mergesort_list mac_carthy isqrt insertion_sort_list flag \
366
	distance muller fib_memo fibonacci \
367 368
        vstte10_aqueue vstte10_inverting vstte10_max_sum \
	vstte10_queens vstte10_search_list \
369
        vacid_0_sparse_array
370 371 372

.PHONY: gallery

373 374 375 376 377 378 379
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	@for f in $(GALLERYPGMS); do \
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
	done
380

381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397
########
# 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

398 399
byte: bin/why3config.byte
opt:  bin/why3config.opt
400

401
bin/why3config.opt: src/why.cmxa $(CONFIGCMX)
402 403 404 405
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

406
bin/why3config.byte: src/why.cma $(CONFIGCMO)
407 408 409
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

410 411 412
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

413 414 415 416 417 418 419 420 421 422 423 424 425
# 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
426
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
427 428 429
	rm -f .why.conf
	rm -f .depend.config

430 431
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
432
		--detect --conf_file why.conf
433

434
install_no_local::
435
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
436

437
install_local: bin/why3config
438

MARCHE Claude's avatar
MARCHE Claude committed
439 440 441 442
###############
# IDE
###############

443 444
ifeq (@enable_ide@,yes)

MARCHE Claude's avatar
MARCHE Claude committed
445 446
IDE_FILES = xml session gconfig db gmain
# IDE_FILES = xml session gconfig newmain
MARCHE Claude's avatar
MARCHE Claude committed
447 448 449 450 451 452 453 454

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

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

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

457
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
458

459 460
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
461

MARCHE Claude's avatar
MARCHE Claude committed
462 463 464
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@ -I @SQLITE3LIB@
bin/why3ide.opt bin/why3ide.byte: EXTOBJS += 
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2 sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
465

466
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
467
	$(if $(QUIET), @echo 'Linking  $@' &&) \
468
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
469 470
	$(STRIP) $@

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

475 476 477
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
478 479 480 481
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
482
.depend.ide: src/ide/xml.ml
483
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
484 485 486 487 488 489

depend: .depend.ide

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

493
install_no_local::
494 495 496
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
497

498
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
499

500

501
###############
502
# Bench
503 504
###############

505 506
ifeq (@enable_bench@,yes)

507
BENCH_FILES = bench benchrc benchdb whybench
508 509 510

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

511
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
512 513 514 515 516 517

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

518
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
519 520 521

# build targets

522 523
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
524

525 526
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I +sqlite3
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
527

528
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
529 530 531 532
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

533
bin/why3bench.byte: src/why.cma  $(PGMCMO) $(BENCHCMO)
534 535 536
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

537 538 539
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

540 541 542 543 544 545 546 547 548 549 550 551
# 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/*~
552
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
553 554 555
	rm -f .depend.bench

install_no_local::
556 557 558
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
559

560 561
endif

562 563 564
##############
# Coq plugin
##############
565

566
ifeq (@enable_coq_support@,yes)
567

568 569 570 571 572 573 574 575 576 577 578 579 580
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))

581
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
582

583 584
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
585

586 587
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
588

589
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
590 591
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

592
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
593 594
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

595 596 597 598
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
599

600 601 602 603 604 605 606 607 608 609 610 611 612 613
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

614
endif
615

616 617 618
########
# Tptp2why
########
619

620
ifeq (@enable_whytptp@,yes)
621

622 623
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
624

François Bobot's avatar
François Bobot committed
625
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
626

627
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
628 629 630 631 632 633

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

634 635
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
636 637 638

# build targets

François Bobot's avatar
François Bobot committed
639
plugins.byte byte: plugins/whytptp.cmo
640
plugins.opt  opt : plugins/whytptp.cmxs
641

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

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

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

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

656 657 658 659 660 661 662 663 664 665 666 667
# 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
668
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
669
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
670
	rm -f plugins/whytptp.cmxs plugins/whytptp.cmo
671 672
	rm -f .depend.tptp2why

673
endif
674

675 676 677 678
#######
# tools
#######

679
TOOLS = bin/why3-cpulimit
680 681 682

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
683
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
684
	$(CC) -Wall -o $@ $^
685 686

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

689
install_no_local::
690 691
	cp -f bin/why3-cpulimit $(BINDIR)

692 693 694 695
#########
# why3doc
#########

696 697
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721

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) $^

722 723 724
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

725 726 727
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

728 729
# depend and clean targets

730 731
WHY3DOCGENERATED=src/why3doc/to_html.ml

732 733
include .depend.why3doc

734
.depend.why3doc: $(WHY3DOCGENERATED)
735 736 737 738 739
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
740
	rm -f $(WHY3DOCGENERATED)
741 742
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
743
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
744 745
	rm -f .depend.why3doc

746 747
install_local: bin/why3doc

748 749 750 751
########
# bench
########

François Bobot's avatar
François Bobot committed
752
.PHONY: bench test comp_bench_plugins
753

754
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
755
	sh bench/bench \
756 757
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
758

759
BENCH_PLUGINS_CMO := helloworld.cmo
760 761 762
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
763 764 765
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
766
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
767 768 769
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
770 771

###############
772
# test targets
773
###############
774

775 776
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
777

778
test: bin/why3.byte plugins.byte $(TOOLS)
779
	mkdir -p output_why3
780 781 782 783 784
	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
785
	@printf "*** Checking Coq file generation ***\\n"
786
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
787
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
788 789
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
790
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
791
		; do \
792
	  printf "Generating Coq file for $$i\\n" && \
793
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
794
	@printf "*** Checking Coq compilation ***\\n"
795
	@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
796

797 798 799
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
800

801 802
testl-debug: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
803

804 805
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
806

807 808
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
809

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

814 815

## Examples : Plugins ##
816

817
ifeq (@enable_plugins@,yes)
818

819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856
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
857

858
endif
859

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
860 861 862
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
863

864 865 866 867 868
.PHONY: doc

ifeq (@enable_doc@,yes)

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

871
BNF = qualid constant operator term type formula theory
872
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
873 874 875 876 877 878 879 880

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

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

881 882 883 884
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
885

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

889 890
# 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
891

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
892
clean::
893 894 895 896 897 898 899
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

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

901
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
902
# API DOC
903
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
904

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
905 906
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
907
MODULESTODOC = util/util util/hashweak \
908
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
909
	core/env core/task \
910
	driver/whyconf driver/driver
MARCHE Claude's avatar
MARCHE Claude committed
911 912
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
913 914 915

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

916
apidoc: $(FILESTODOC)
917
	mkdir -p doc/apidoc
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
918
	$(OCAMLDOC) -d doc/apidoc -html -keep-code $(INCLUDES) \
919
		$(LIBINCLUDES) -I src $(FILESTODOC)
920
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
921

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

MARCHE Claude's avatar
MARCHE Claude committed
925
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
926
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
927
		$(LIBINCLUDES) -I src $(FILESTODOC)
928
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
929

930
clean::
931
	rm -f doc/apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
932

933
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
934
# generic rules
935
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
936

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

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

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

946
%.cmxs: %.ml
947
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
948

Andrei Paskevich's avatar
Andrei Paskevich committed
949
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
950 951
	$(OCAMLLEX) $<

952
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
953 954
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
964 965 966 967 968 969 970 971
# 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
972 973 974 975 976 977 978 979 980 981 982

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
983
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
984 985 986 987
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
988
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
989 990 991 992
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
993 994
	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
995

996 997 998 999 1000
# 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
1001
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1002
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1003

1004
dep: depend
1005
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
1006
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1007

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1008 1009 1010
# distrib
#########

1011 1012 1013 1014
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

MARCHE Claude's avatar
MARCHE Claude committed
1015
# CHANGES (not up-to-date, moreover is in French)
MARCHE Claude's avatar
MARCHE Claude committed
1016
DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
MARCHE Claude's avatar
MARCHE Claude committed
1017
      README INSTALL OCAML-LICENSE LICENSE \
1018 1019 1020 1021
      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
1022
      examples/*.why examples/programs/*.mlw examples/tptp/*.why \
MARCHE Claude's avatar
MARCHE Claude committed
1023
      examples/my_cosine/*.v \
1024
      theories/*.why theories/*/*.why \
1025
      modules/*.mlw \
1026
      share/provers-detection-data.conf.in \
1027 1028 1029 1030 1031 1032 1033 1034
      share/emacs/why.el share/images/*.png share/lang/*.lang

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

distrib:: $(DISTRIB_TAR)

1035
rmdistrib:
MARCHE Claude's avatar
MARCHE Claude committed
1036 1037 1038 1039
	rm -rf $(DISTRIB_DIR)

redistrib: rmdistrib distrib

1040 1041 1042 1043 1044 1045 1046
$(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;