Makefile.in 26.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
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
74
#PDFVIEWER = @PDFVIEWER@
75

76 77
BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -dtypes    -I src $(INCLUDES)
78

79 80 81 82 83
ifeq (@ENABLE_PROFILING@,yes)
OFLAGS += -g -p
STRIP = true
endif

84 85
# external libraries common to all binaries

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

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
91

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92 93 94
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100
#############
101
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103

104
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
105 106
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
107
	       src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

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

112
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
113

114
LIB_PARSER = ptree denv typing parser lexer
115

116
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
117
	     whyconf autodetection
118

119
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
120
		inlining split_goal \
121
		eliminate_definition eliminate_algebraic \
122
		eliminate_inductive eliminate_let eliminate_if \
123
		encoding_enumeration encoding encoding_decorate_mono \
124
		libencoding encoding_decorate encoding_bridge \
125
		encoding_explicit encoding_sort \
126
		encoding_instantiate simplify_array filter_trigger \
127
		encoding_arrays \
128
		introduction abstraction close_epsilon lift_epsilon
129

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
130
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
131

132 133 134 135 136 137
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)) \
138
	      $(addprefix src/printer/, $(LIB_PRINTER))
139

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

143 144
ifeq (@enable_hypothesis_selection@,yes)
	LIB_TRANSFORM += hypothesis_selection
145
	INCLUDES += -I +ocamlgraph
146 147 148
	EXTLIBS += ocamlgraph/graph
endif

149 150 151 152
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
153

154
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
155
$(LIBCMX): OFLAGS += -for-pack Why
156

157
LIB_PARSER_POSTLUDE = \
158
  "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"
159 160

LIB_PARSER_INTERFACE = \
161 162
  -e "s/^val  *logic_file_eof *:/val logic_file_eof : Env.env ->/" \
  -e "s/^val  *list0_decl_eof *:/val list0_decl_eof : Env.env -> \
163 164
  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"

165 166
src/parser/parser.ml: src/parser/parser.pre.ml
	cp src/parser/parser.pre.ml src/parser/parser.ml
167
	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
168 169 170

src/parser/parser.mli: src/parser/parser.pre.mli
	sed $(LIB_PARSER_INTERFACE) src/parser/parser.pre.mli > \
171
					src/parser/parser.mli
172

173
# build targets
174

175 176
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177

178
src/why.cma: src/why.cmo
179 180
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

181
src/why.cmxa: src/why.cmx
182 183
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

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

187 188 189 190
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
191

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
192 193
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
194
.depend.lib: src/config.ml $(LIBGENERATED)
195
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196 197 198

depend: .depend.lib

199 200
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
201
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
202 203
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
204 205
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
206 207 208 209 210 211
	   $(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
212
	rm -f .depend.lib
213

214 215 216
###############
# installation
###############
217
install_no_local::
218 219 220
	mkdir -p $(BINDIR)
	mkdir -p $(LIBDIR)/why3
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
221
	mkdir -p $(DATADIR)/why3/emacs
222
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
223 224 225 226 227 228
	mkdir -p $(DATADIR)/why3/theories
	mkdir -p $(DATADIR)/why3/theories/transform
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
	cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
	cp -f drivers/*.drv $(DATADIR)/why3/drivers
229 230
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
231
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
232 233
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

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

240 241
ifeq ("@ENABLE_LOCAL@","no")
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
242
install-lib: install_no_local_lib
243
else
MARCHE Claude's avatar
MARCHE Claude committed
244
install install-lib:
245 246 247 248
	@echo "You use a local configuration you can't install with it."
	@echo "Run ./configure without --enable-local"
endif

MARCHE Claude's avatar
MARCHE Claude committed
249 250
install-all: install install-lib

251

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

328 329
# test target

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

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

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

339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388

########
# Config
########

CONFIG_FILES = whyconfig

CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))

CONFIGML  = $(addsuffix .ml,  $(CONFIGMODULES))
CONFIGMLI = $(addsuffix .mli, $(CONFIGMODULES))
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

$(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs

# build targets

byte: bin/whyconfig.byte
opt:  bin/whyconfig.opt

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

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

# depend and clean targets

include .depend.config

.depend.config: $(CONFIGGENERATED)
	$(OCAMLDEP) -slash -I src -I src/config $(CONFIGML) $(CONFIGMLI) > $@

depend: .depend.config

clean::
	rm -f src/config/*.cm[iox] src/config/*.o
	rm -f src/config/*.annot src/config/*~
	rm -f src/config/*.output src/config/*.automaton
	rm -f bin/whyconfig.byte bin/whyconfig.opt
	rm -f .why.conf
	rm -f .depend.config

local_config: bin/whyconfig.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/whyconfig.@OCAMLBEST@ --autodetect-provers --conf_file .why.conf

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


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

397 398
ifeq (@enable_ide@,yes)

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

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

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

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

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

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

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

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

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

# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

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

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

448

449 450 451 452
###############
# BENCH
###############

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

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

BENCHMODULES := src/ide/scheduler $(BENCHMODULES)

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

$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I +sqlite3

# build targets

byte: bin/whybench.byte
opt:  bin/whybench.opt

bin/whybench.opt bin/whybench.byte: INCLUDES += -thread -I +threads
bin/whybench.opt bin/whybench.byte: EXTLIBS += threads

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

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

# depend and clean targets

include .depend.bench

.depend.bench:
	$(OCAMLDEP) -slash -I src -I src/bench -I src/ide $(BENCHML) $(BENCHMLI) > $@

depend: .depend.bench

clean::
	rm -f src/bench/*.cm[iox] src/bench/*.o
	rm -f src/bench/*.annot src/bench/*~
	rm -f bin/whybench.byte bin/whybench.opt
	rm -f .depend.bench

install_no_local::
	cp -f bin/whybench.@OCAMLBEST@ $(BINDIR)/why3bench

501 502 503 504
##############
# Coq plugin
##############

505 506 507 508 509 510 511 512 513 514 515 516 517
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))

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

Andrei Paskevich's avatar
Andrei Paskevich committed
520
ifeq (@enable_coq_support@,yes)
521 522
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
523
endif
524

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

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

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

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

539
ifeq (@enable_coq_support@,yes)
540 541 542 543 544 545
include .depend.coq

.depend.coq: $(COQGENERATED)
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

depend: .depend.coq
Andrei Paskevich's avatar
Andrei Paskevich committed
546
endif
547 548 549 550 551 552 553 554

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

555 556 557 558
########
# Tptp2why
########

559 560
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
561

François Bobot's avatar
François Bobot committed
562
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
563

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

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

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

# build targets

576
ifeq (@enable_whytptp@,yes)
François Bobot's avatar
François Bobot committed
577 578
byte: plugins/whytptp.cmo
opt:  plugins/whytptp.cmxs
579 580
endif

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

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

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

François Bobot's avatar
François Bobot committed
591
src/tptp2why/whytptp.cmo: $(TPTPCMO)
592
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
593 594 595 596 597 598 599
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

plugins/whytptp.cmxs: plugins src/tptp2why/whytptp.cmxs
	@cp src/tptp2why/whytptp.cmxs $@

plugins/whytptp.cmo: plugins src/tptp2why/whytptp.cmo
	@cp src/tptp2why/whytptp.cmo $@
600 601 602

# depend and clean targets

603
ifeq (@enable_whytptp@,yes)
604 605 606 607 608 609
include .depend.tptp2why

.depend.tptp2why: $(TPTPGENERATED)
	$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@

depend: .depend.tptp2why
610
endif
611 612 613 614 615

clean::
	rm -f $(TPTPGENERATED)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
616
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
617
	rm -f bin/whytptp.byte bin/whytptp.opt
618 619
	rm -f .depend.tptp2why

620 621 622 623
#######
# tools
#######

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
624
TOOLS = bin/why3-cpulimit
625 626 627

byte opt: $(TOOLS)

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

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

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

637 638 639 640
########
# bench
########

François Bobot's avatar
François Bobot committed
641
.PHONY: bench test comp_bench_plugins
642

MARCHE Claude's avatar
MARCHE Claude committed
643
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
644
	sh bench/bench \
645
	    "bin/why.@OCAMLBEST@" \
646
	    "bin/whyml.@OCAMLBEST@"
647

648
BENCH_PLUGINS_CMO := helloworld.cmo
649 650 651
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
652 653 654 655 656 657 658
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
# 	bin/why.byte -D bench/plugins/helloworld.drv \
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
659 660

###############
661
# test targets
662
###############
663

664 665 666
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

667
test: bin/why.byte $(TOOLS)
668
	mkdir -p output_why3
669
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
670 671 672
	bin/why.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
	bin/why.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
	bin/why.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
673
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
674
	@printf "*** Checking Coq file generation ***\\n"
675
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
676
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
677 678
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
679
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
680
		; do \
681
	  printf "Generating Coq file for $$i\\n" && \
682
	  	bin/why.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
683
	@printf "*** Checking Coq compilation ***\\n"
684
	@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
685

686
testl: bin/whyml.byte
687
	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
688
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
689

690 691 692
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

693
testl-type: bin/whyml.byte
694
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
695

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

700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743

## Examples : Plugins ##

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

ifeq (@enable_plugins@,yes)
include .depend.plug

.depend.plug: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I $(PLUGDIR) $(PLUGML) | sed "s/cmx/cmxs/" > $@

depend: .depend.plug
endif

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
744 745 746
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
747

MARCHE Claude's avatar
MARCHE Claude committed
748 749
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
750

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

MARCHE Claude's avatar
MARCHE Claude committed
753 754
doc/manual.pdf: doc/apidoc.tex doc/manual.tex doc/version.tex
	cd doc; pdflatex manual
Andrei Paskevich's avatar
Andrei Paskevich committed
755 756 757
	cd doc; makeglossaries manual
	cd doc; pdflatex manual
	cd doc; makeglossaries manual
MARCHE Claude's avatar
MARCHE Claude committed
758
	cd doc; pdflatex manual
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
759 760

doc/manual.html: doc/manual.tex doc/version.tex
761
	$(MAKE) -C doc manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
762

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
763
clean::
764
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
765

766
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
767
# API DOC
768
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
769

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
770 771
.PHONY: apidoc

772 773
MODULESTODOC = util/util \
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
774
	core/env core/task \
MARCHE Claude's avatar
MARCHE Claude committed
775 776 777
	driver/whyconf driver/driver 
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
778 779 780

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

781
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
782
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
783
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
784
		$(LIBINCLUDES) -I src $(FILESTODOC)
785
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
786

MARCHE Claude's avatar
MARCHE Claude committed
787
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
788
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
789
		$(LIBINCLUDES) -I src $(FILESTODOC)
790
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
791

792 793
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
794

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

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

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

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

808
%.cmxs: %.ml
809
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
810

Andrei Paskevich's avatar
Andrei Paskevich committed
811
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
812 813
	$(OCAMLLEX) $<

814
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
815 816
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
826 827 828 829 830 831 832 833
# 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
834 835 836 837 838 839 840 841 842 843 844

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
845
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
846 847 848 849
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
850
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
851 852 853 854
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
855 856
	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
857

858 859 860 861 862
# 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
863
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
864
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
865

866
dep: depend
867
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
868
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
869

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
870 871 872
# distrib
#########

873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903
NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz

DISTRIB_FILES = Version Makefile.in configure.in configure .depend.* \
      README INSTALL OCAML-LICENSE LICENSE CHANGES \
      src/*.ml* src/*/*.ml* src/*/*.c \
      src/config.sh.in \
      doc/version.tex.in doc/manual.pdf \
      drivers/*.drv \
      examples/*.why \
      theories/*.why theories/*/*.why \
      share/*.conf \
      share/emacs/why.el share/images/*.png share/lang/*.lang

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

distrib:: $(DISTRIB_TAR)

$(DISTRIB_TAR): doc/manual.pdf
	@if test -d $(DISTRIB_DIR); then \
	  echo "Hum... there is already a directory $(NAME)"; \
	  echo "Please increase the version number"; exit 1; \
        fi
	mkdir -p $(DISTRIB_DIR)
	mkdir -p $(DISTRIB_DIR)/bin
	cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR)
	cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar

Andrei Paskevich's avatar
Andrei Paskevich committed
904
# distrib export: source export-doc export-www export-examples export-examples-c linux
905
#
Andrei Paskevich's avatar
Andrei Paskevich committed
906 907 908
# 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
909
# 	$(MAKE) -C /users/demons/filliatr/www/why install
910 911 912
#
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
913 914
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
915
# 	$(MAKE) export/$(NAME).tar.gz
916
#
Andrei Paskevich's avatar
Andrei Paskevich committed
917
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
918
#
Andrei Paskevich's avatar
Andrei Paskevich committed
919 920
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
921
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
922
# 	echo "*** faire make all dans $(WWW)/examples ***"
923
#
Andrei Paskevich's avatar
Andrei Paskevich committed
924 925 926 927 928 929
# 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
930
#
Andrei Paskevich's avatar
Andrei Paskevich committed
931 932 933 934 935 936 937 938
# 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)
939
#
Andrei Paskevich's avatar
Andrei Paskevich committed
940
# OSTYPE  ?= linux
941
#
Andrei Paskevich's avatar
Andrei Paskevich committed
942
# BINARYNAME = $(NAME)-$(OSTYPE)
943
#
Andrei Paskevich's avatar
Andrei Paskevich committed
944
# linux: binary
945 946 947
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
948 949 950 951 952
# binary: $(ALLBINARYFILES)
# 	mkdir -p export/$(BINARYNAME)
# 	cp --parents $(ALLBINARYFILES) export/$(BINARYNAME)
# 	(cd export; tar czf $(BINARYNAME).tar.gz $(BINARYNAME))
# 	cp export/$(BINARYNAME).tar.gz $(FTP)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
953

954
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
955
# file headers
956 957
###############

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
958
headers:
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
959
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
960
	    Makefile.in configure.in */*.ml */*/*.ml */*/*.ml[ily4]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
961

962
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
963
# myself
964
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
965

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
966
Makefile: Makefile.in config.status
967
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
968

969
src/config.sh: src/config.sh.in config.status
970
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
971

972
src/config.ml: src/config.sh
973
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
974

Andrei Paskevich's avatar
Andrei Paskevich committed
975
doc/version.tex: doc/version.tex.in config.status
976
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
977 978

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

François Bobot's avatar
META  
François Bobot committed
981 982 983 984 985
opt byte : META

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
986
configure: configure.in
987
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
988

989
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
990
# clean and depend
991
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
992

993
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
994

995
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
996 997
	rm -f config.status config.cache config.log \
	    Makefile src/config.ml doc/version.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
998

999 1000 1001 1002
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1003 1004 1005 1006 1007 1008 1009
#################################################################
# Building the Why platform with ocamlbuild (OCaml 3.10 needed) #
#################################################################

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

# To build using Ocamlbuild:
1010
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1011 1012 1013 1014 1015 1016 1017 1018
# are generated.
# 2) Run Ocamlbuild with any target to generate the sanitization script.
# 3) Run ./sanitize to delete the generated files that shouldn't be generated
# (i.e. all lexers and parsers).
# 4) Run Ocamlbuild with the target you need, for example:
# ocamlbuild jc/jc_main.native

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