Makefile.in 21.1 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 4 5 6 7
#  Copyright (C) 2010-                                                   #
#    Francois Bobot                                                      #
#    Jean-Christophe Filliatre                                           #
#    Johannes Kanig                                                      #
#    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 34 35 36 37 38 39 40

prefix 	    = @prefix@
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
DATADIR = $(DESTDIR)@datadir@
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
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
Andrei Paskevich's avatar
Andrei Paskevich committed
55
#CAMLP4   = @CAMLP4O@
56 57 58 59

OCAMLVERSION = @OCAMLVERSION@

#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
60
#PDFVIEWER = @PDFVIEWER@
61

62 63
BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -dtypes    -I src $(INCLUDES)
64 65 66

# external libraries common to all binaries

Andrei Paskevich's avatar
Andrei Paskevich committed
67
ifeq (@enable_plugins@,yes)
68
  DYNLINK = dynlink
69
else
70
  DYNLINK =
71 72
endif

73 74 75
EXTLIBS = str unix nums $(DYNLINK)
EXTCMA	= $(addsuffix .cma,$(EXTLIBS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77 78 79
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83
.PHONY: byte opt clean depend all
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
#############
86
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88

89
LIBGENERATED = src/util/rc.ml \
90 91 92 93
	       src/parser/parser.mli src/parser/parser.ml \
	       src/parser/parser.output src/parser/lexer.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
	       src/driver/driver_parser.output src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94

95
LIB_UTIL = pp loc prtree util hashcons sysutil hashweak rc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96

97
LIB_CORE = ident ty term pattern decl theory task pretty trans env register
98

99
LIB_PARSER = ptree parser lexer denv typing
100

101
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver whyconf
102

103 104 105 106 107
LIB_TRANSFORM = simplify_recursive_definition inlining \
		split_conjunction encoding_decorate \
		remove_logic_definition eliminate_inductive \
		compile_match eliminate_algebraic \
		eliminate_let eliminate_definition
108

109
LIB_PRINTER = print_real alt_ergo why3 smt coq
110

111 112 113 114 115 116
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)) \
117
	      $(addprefix src/printer/, $(LIB_PRINTER))
118

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

122 123 124 125
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
126

127 128
$(LIBCMO) $(LIBCMX): INCLUDES = $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why
129

130
# build targets
131

132 133
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134

135
src/why.cma: src/why.cmo
136 137
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

138
src/why.cmxa: src/why.cmx
139 140
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

141 142
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
143

144 145 146 147
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

src/why.cmi: src/why.cmo src/why.cmx
148
	@echo -n
Francois Bobot's avatar
Francois Bobot committed
149

150
# depend target
151

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152 153
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
154
.depend.lib: src/config.ml $(LIBGENERATED)
155
	$(OCAMLDEP) -slash $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156 157 158

depend: .depend.lib

159 160
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
161
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
162 163 164 165 166 167 168 169 170
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
	   $(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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171
##################
172
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173 174 175 176 177
##################

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

178
bin/why.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
179 180
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181 182
	$(STRIP) $@

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

187 188
src/main.cmo src/main.cmx: src/why.cmi

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
190
	rm -f src/main.cm[iox] src/main.annot src/main.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191
	rm -f bin/why.byte bin/why.opt
192

193 194 195
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196

197 198
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
	       src/programs/pgm_parser.output src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
199

200
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
201

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

204 205 206 207 208 209 210 211 212
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

$(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs
$(PGMCMO) $(PGMCMX): src/why.cmi

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214
byte: bin/whyml.byte
215
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
216

217 218 219
bin/whyml.opt: src/why.cmxa $(PGMCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220 221
	$(STRIP) $@

222 223 224 225 226
bin/whyml.byte: src/why.cma $(PGMCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227 228

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233 234 235
depend: .depend.programs

clean::
236 237 238
	rm -f $(PGMGENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239 240 241
	rm -f bin/whyml.byte bin/whyml.opt

###############
242
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243 244
###############

245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
MNG_FILES = db test

MNGMODULES = $(addprefix src/manager/, $(MNG_FILES))

MNGML  = $(addsuffix .ml,  $(MNGMODULES))
MNGMLI = $(addsuffix .mli, $(MNGMODULES))
MNGCMO = $(addsuffix .cmo, $(MNGMODULES))
MNGCMX = $(addsuffix .cmx, $(MNGMODULES))

$(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3
$(MNGCMO) $(MNGCMX): src/why.cmi

#byte: bin/manager.byte
#opt:  bin/manager.opt

MARCHE Claude's avatar
MARCHE Claude committed
260 261
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3

262 263
bin/manager.opt: src/why.cmxa $(MNGCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
MARCHE Claude's avatar
MARCHE Claude committed
264
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^
265
	$(STRIP) $@
MARCHE Claude's avatar
MARCHE Claude committed
266

267 268 269
bin/manager.byte: src/why.cma $(MNGCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
270

271
# depend and clean targets
MARCHE Claude's avatar
MARCHE Claude committed
272 273 274

include .depend.manager

275 276
.depend.manager:
	$(OCAMLDEP) -slash -I src/manager/ $(MNGML) $(MNGMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
277

278
depend: .depend.manager
MARCHE Claude's avatar
MARCHE Claude committed
279 280

clean::
281 282
	rm -f src/manager/*.cm[iox] src/manager/*.o
	rm -f src/manager/*.annot src/manager/*~
MARCHE Claude's avatar
MARCHE Claude committed
283
	rm -f bin/manager.byte bin/manager.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284

285
#####################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286 287 288
# graphical interface
#####################

289
IDE_FILES = ide_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
290

291 292 293 294 295 296 297 298 299 300 301
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))

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

$(IDECMO) $(IDECMX): INCLUDES = -I src/ide -I +lablgtk2 -I +threads
$(IDECMO) $(IDECMX): src/why.cmi

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

Andrei Paskevich's avatar
Andrei Paskevich committed
303 304 305 306
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt:  bin/whyide.opt
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
307

MARCHE Claude's avatar
MARCHE Claude committed
308 309
bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads

310
bin/whyide.opt: src/why.cmxa $(IDE_CMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
311 312 313 314
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
	    lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
	$(STRIP) $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
315

MARCHE Claude's avatar
MARCHE Claude committed
316

317
bin/whyide.byte: src/why.cma $(IDE_CMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
318 319 320
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
	    lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321

322 323
# depend and clean targets

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324 325 326
include .depend.ide

.depend.ide:
327
	$(OCAMLDEP) -slash -I src/ide $(IDEML) $(IDEMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328 329 330 331

depend: .depend.ide

clean::
332 333
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334
	rm -f bin/whyide.byte bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
335

336 337 338 339
##############
# Coq plugin
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
340
ifeq (@enable_coq_support@,yes)
341
#byte: src/coq-plugin/whytac.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
342 343
opt:  src/coq-plugin/whytac.cmxs
endif
344

345
COQTREES = kernel lib interp parsing proofs pretyping tactics library
Andrei Paskevich's avatar
Andrei Paskevich committed
346

347 348 349 350
#src/coq-plugin/whytac.cmo:  INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))

#src/coq-plugin/whytac.cmo:  BFLAGS+=-rectypes
351 352
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes

353
src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml
354 355
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393
#######
# tools
#######

TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

bin/why-cpulimit: src/tools/@CPULIMIT@.c
	$(CC) -o $@ $^

clean::
	rm -f bin/why-cpulimit src/tools/*~

########
# bench
########

.PHONY: bench test

bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
	sh bench/bench \
	    "bin/why.@OCAMLBEST@ -I theories" \
	    "bin/whyml.@OCAMLBEST@ -I theories"

BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
	bin/why.byte -D bench/plugins/helloworld.drv -I theories/ \
	src/test.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv -I theories/ \
	src/test.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/simplify_array.drv -I theories/ \
	src/test.why -t Test_simplify_array -g G

###############
394
# test targets
395
###############
396

397
test: bin/why.byte $(TOOLS)
398
	mkdir -p output_why3
399 400 401 402 403 404 405
	ocamlrun -bt bin/why.byte -I theories/ -D drivers/why3.drv \
		-o output_why3 src/test.why
	bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		src/test.why -t Test -g G
	bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		--timeout 3 --prove src/test.why -t Test -g G
	bin/why.byte -D drivers/coq.drv -I theories/ \
406
		src/test.why -t Test -g G
407
	echo bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
408
		--timeout 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
409
	@printf "*** Checking Coq file generation ***\\n"
410
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
411
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
412 413
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
414
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
415
		; do \
MARCHE Claude's avatar
MARCHE Claude committed
416
	  printf "Generating Coq file for $$i\\n" && bin/why.byte \
417 418
		-D drivers/coq.drv -I theories/ \
		-o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
419
	@printf "*** Checking Coq compilation ***\\n"
420
	@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
421

422 423
testl: bin/whyml.byte
	ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw
424

425 426
examples/programs/%: bin/whyml.byte
	bin/whyml.byte -I theories examples/programs/$*.mlw
427

428
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
# installation
430
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
431

432 433 434 435
## install: install-binary install-lib install-man
##
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST)
##
Andrei Paskevich's avatar
Andrei Paskevich committed
436 437
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
438
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
439 440 441 442 443
## 	mkdir -p $(BINDIR)
## 	cp -f $(BINARY) $(BINDIR)/why$(EXE)
## 	if test -f bin/why-ide.$(OCAMLBEST); then \
## 		cp -f bin/why-ide.$(OCAMLBEST) $(BINDIR)/why-ide-bin$(EXE); \
## 	fi
444 445
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
446
## 	mkdir -p $(LIBDIR)/why/why
447
##
Andrei Paskevich's avatar
Andrei Paskevich committed
448 449 450
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
451
##
Andrei Paskevich's avatar
Andrei Paskevich committed
452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
## install-coq-no:
## install-coq-yes: install-coq-@COQVER@
## install-coq-v7:
## 	mkdir -p $(LIBDIR)/why/coq7
## 	cp -f $(V7FILES) $(LIBDIR)/why/coq7
## 	cp -f $(VO7) $(LIBDIR)/why/coq7
## install-coq-v8 install-coq-v8.1:
## 	if test -w $(COQLIB) ; then \
## 	 mkdir -p $(COQLIB)/user-contrib ; \
## 	 cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
## 	 cp -f $(VO8) $(COQLIB)/user-contrib ; \
## 	else \
## 	echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
## 	mkdir -p $(LIBDIR)/why/coq ;\
## 	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
## 	fi
468
##
Andrei Paskevich's avatar
Andrei Paskevich committed
469 470 471 472 473 474 475 476
## install-pvs-no:
## install-pvs-yes: $(PVSFILES)
## 	mkdir -p $(PVSLIB)/why
## 	cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(PVSLIB)/why
## 	cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(PVSLIB)/why
## 	@echo "======  Compiling PVS theories, this may take some time ======"
## 	(cd $(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out)
## 	@echo "======  Done compiling PVS theories ======"
477
##
Andrei Paskevich's avatar
Andrei Paskevich committed
478 479 480 481 482
## install-mizar-no:
## install-mizar-yes:
## 	mkdir -p @MIZARLIB@/mml/dict
## 	cp lib/mizar/why.miz @MIZARLIB@/mml
## 	cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict
483 484
##
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
485 486 487 488 489 490
## 	cp $(BINARY) $$HOME/bin/why
## 	cp $(WHYCONFIG) $$HOME/bin/why
## 	cp $(JESSIE) $$HOME/bin/jessie
## 	if test -f bin/why-ide.$(OCAMLBEST); then \
## 	  cp -f bin/why-ide.$(OCAMLBEST) $$HOME/bin/why-ide; \
## 	fi
491
##
Andrei Paskevich's avatar
Andrei Paskevich committed
492
## local: install
493
##
Andrei Paskevich's avatar
Andrei Paskevich committed
494 495
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
496
##
Andrei Paskevich's avatar
Andrei Paskevich committed
497 498
## zip:
## 	zip -A -r why-$(VERSION).zip c:/why/bin c:/why/lib c:/coq/lib/contrib/why c:/coq/lib/contrib7/why
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
499

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
500 501 502
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
503

504
DOC = doc/manual.pdf doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
505

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
508 509
doc/manual.pdf: doc/manual.tex doc/version.tex
	make -C doc manual.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
510 511 512 513

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
514 515
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
516

517
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
518
# API DOC
519
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
520

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
521 522
.PHONY: apidoc

523
apidoc:
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
524
	mkdir -p apidoc
525 526
	$(OCAMLDOC) -d apidoc -html -I src $(LIBINCLUDES) -I +sqlite3 \
	    $(LIBML) $(LIBMLI) $(MNGML) $(MNGMLI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
527

528 529
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530

531
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
532
# generic rules
533
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
534

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

538
%.cmo %cmi: %.ml
539
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
540

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

544
%.cmxs: %.ml
545
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
546

Andrei Paskevich's avatar
Andrei Paskevich committed
547
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
548 549
	$(OCAMLLEX) $<

Andrei Paskevich's avatar
Andrei Paskevich committed
550
%.ml %.mli %.output: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
551 552
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
562 563 564 565 566 567 568 569
# 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
570 571 572 573 574 575 576 577 578 579 580

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
581
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
582 583 584 585
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
586
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
587 588 589 590 591 592 593
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
	otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml

wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
594
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
595

596
dep:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
597
	$(MAKE) depend
598
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
599
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
600

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
601 602 603
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
604 605
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
606
#
Andrei Paskevich's avatar
Andrei Paskevich committed
607 608 609
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
610
#
Andrei Paskevich's avatar
Andrei Paskevich committed
611
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
612 613 614 615 616
#       mix/*.ml* \
#       version.sh Version Makefile.in configure.in configure .depend .depend.coq \
#       config/check_ocamlgraph.ml \
#       README INSTALL COPYING LICENSE CHANGES \
#       doc/Makefile doc/manual.ps doc/why.1 \
Andrei Paskevich's avatar
Andrei Paskevich committed
617 618 619 620 621 622 623
# 	examples-c/*/*.h examples-c/*/*.c \
# 	examples-c/Makefile examples-c/*/Makefile \
# 	examples-c/*/coq/*.v \
# 	examples/Makefile* \
# 	examples/*/*.mlw examples/*/*.why examples/*/*.v examples/*/*.sx \
# 	examples/*/.depend examples/*/Makefile \
# 	bench/bench.in bench/good*/*.mlw bench/good*/*.v \
624
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
# 	bench/jc/bench bench/jc/good/*.jc \
# 	bench/java/bench bench/java/*/*.java bench/provers/*.mlw \
# 	tests/regtest.sh tests/java/*.java \
# 	tests/java/coq/*.v \
# 	tests/java/result/README tests/java/oracle/*.oracle \
# 	lib/coq*/*.v \
# 	lib/pvs/pvscontext.el lib/pvs/*.pvs lib/pvs/*.prf \
# 	lib/mizar/why.miz lib/mizar/dict/why.voc \
# 	lib/why/*.why lib/isabelle/*.thy lib/hol4/*.ml lib/harvey/*.rv \
# 	lib/java_api/java/*/*.java \
# 	lib/javacard_api/java/lang/*.java \
# 	lib/javacard_api/javacard/*/*.java \
# 	lib/javacard_api/javacardx/crypto/*.java \
# 	lib/javacard_api/com/sun/javacard/impl/*.java \
# 	lib/images/*.png \
# 	atp/*.ml atp/LICENSE.txt atp/Makefile atp/Mk_ml_file \
# 	ocamlgraph/configure.in ocamlgraph/configure ocamlgraph/.depend \
# 	ocamlgraph/Makefile.in ocamlgraph/META.in ocamlgraph/*/*.ml* \
643 644 645
#	frama-c-plugin/Makefile frama-c-plugin/configure \
# 	frama-c-plugin/*.ml* frama-c-plugin/share/jessie/*.h
#
Andrei Paskevich's avatar
Andrei Paskevich committed
646
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
647
#
Andrei Paskevich's avatar
Andrei Paskevich committed
648
# distrib export: source export-doc export-www export-examples export-examples-c linux
649
#
Andrei Paskevich's avatar
Andrei Paskevich committed
650 651 652 653
# 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
# 	make -C /users/demons/filliatr/www/why install
654
#
Andrei Paskevich's avatar
Andrei Paskevich committed
655 656
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
657
#
Andrei Paskevich's avatar
Andrei Paskevich committed
658 659 660 661 662 663
# export/$(NAME).tar.gz: $(FILES)
# 	rm -rf $(EXPORT)
# 	mkdir -p $(EXPORT)/bin
# 	cp --parents $(FILES) $(EXPORT)
# 	cd $(EXPORT); rm -f $(GENERATED)
# 	cd export; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
664 665
#
# tarball-for-framac:
Andrei Paskevich's avatar
Andrei Paskevich committed
666 667
# 	make tarball
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
668 669
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
670 671 672
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
# 	make export/$(NAME).tar.gz
673
#
Andrei Paskevich's avatar
Andrei Paskevich committed
674
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
675
#
Andrei Paskevich's avatar
Andrei Paskevich committed
676 677 678 679
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
# 	make -C $(WWW)/examples clean depend
# 	echo "*** faire make all dans $(WWW)/examples ***"
680
#
Andrei Paskevich's avatar
Andrei Paskevich committed
681 682 683 684 685 686
# 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
687
#
Andrei Paskevich's avatar
Andrei Paskevich committed
688 689 690 691 692 693 694 695
# 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)
696
#
Andrei Paskevich's avatar
Andrei Paskevich committed
697
# OSTYPE  ?= linux
698
#
Andrei Paskevich's avatar
Andrei Paskevich committed
699
# BINARYNAME = $(NAME)-$(OSTYPE)
700
#
Andrei Paskevich's avatar
Andrei Paskevich committed
701
# linux: binary
702 703 704
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
705 706 707 708 709
# 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
710

711
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
712
# file headers
713 714
###############

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

719
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
720
# myself
721
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
722

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
723
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
724 725 726 727
	./config.status --file $@

src/config.ml: src/config.ml.in config.status
	./config.status --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
728

Andrei Paskevich's avatar
Andrei Paskevich committed
729 730 731 732
doc/version.tex: doc/version.tex.in config.status
	./config.status --file $@

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
733 734 735
	./config.status --recheck

configure: configure.in
736
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
737

738
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
739
# clean and depend
740
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
741

742
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
743

744
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
745 746
	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
747 748 749 750 751 752 753 754

#################################################################
# 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:
755
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
756 757 758 759 760 761 762 763
# 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.