Makefile.in 20.9 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 260 261 262 263
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

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

265 266 267
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
268

269
# depend and clean targets
MARCHE Claude's avatar
MARCHE Claude committed
270 271 272

include .depend.manager

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

276
depend: .depend.manager
MARCHE Claude's avatar
MARCHE Claude committed
277 278

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

283
#####################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284 285 286
# graphical interface
#####################

287
IDE_FILES = ide_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
288

289 290 291 292 293 294 295 296 297 298 299
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
300

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

306
bin/whyide.opt: src/why.cmxa $(IDE_CMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
307 308 309 310
	$(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
311

312
bin/whyide.byte: src/why.cma $(IDE_CMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
313 314 315
	$(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
316

317 318
# depend and clean targets

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319 320 321
include .depend.ide

.depend.ide:
322
	$(OCAMLDEP) -slash -I src/ide $(IDEML) $(IDEMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
323 324 325 326

depend: .depend.ide

clean::
327 328
	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
329
	rm -f bin/whyide.byte bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
330

331 332 333 334
##############
# Coq plugin
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
335
ifeq (@enable_coq_support@,yes)
336
#byte: src/coq-plugin/whytac.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
337 338
opt:  src/coq-plugin/whytac.cmxs
endif
339

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

342 343 344 345
#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
346 347
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes

348
src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml
349 350
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

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

###############
389
# test targets
390
###############
391

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

417 418
testl: bin/whyml.byte
	ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw
419

420 421
examples/programs/%: bin/whyml.byte
	bin/whyml.byte -I theories examples/programs/$*.mlw
422

423
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
# installation
425
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
426

427 428 429 430
## install: install-binary install-lib install-man
##
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST)
##
Andrei Paskevich's avatar
Andrei Paskevich committed
431 432
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
433
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
434 435 436 437 438
## 	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
439 440
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
441
## 	mkdir -p $(LIBDIR)/why/why
442
##
Andrei Paskevich's avatar
Andrei Paskevich committed
443 444 445
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
446
##
Andrei Paskevich's avatar
Andrei Paskevich committed
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462
## 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
463
##
Andrei Paskevich's avatar
Andrei Paskevich committed
464 465 466 467 468 469 470 471
## 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 ======"
472
##
Andrei Paskevich's avatar
Andrei Paskevich committed
473 474 475 476 477
## 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
478 479
##
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
480 481 482 483 484 485
## 	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
486
##
Andrei Paskevich's avatar
Andrei Paskevich committed
487
## local: install
488
##
Andrei Paskevich's avatar
Andrei Paskevich committed
489 490
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
491
##
Andrei Paskevich's avatar
Andrei Paskevich committed
492 493
## 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
494

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
495 496 497
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
503 504
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
505 506 507 508

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
509 510
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
511

512
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
513
# API DOC
514
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
515

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
516 517
.PHONY: apidoc

518
apidoc:
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
519
	mkdir -p apidoc
520 521
	$(OCAMLDOC) -d apidoc -html -I src $(LIBINCLUDES) -I +sqlite3 \
	    $(LIBML) $(LIBMLI) $(MNGML) $(MNGMLI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
522

523 524
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525

526
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
527
# generic rules
528
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
529

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

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

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

539
%.cmxs: %.ml
540
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
541

Andrei Paskevich's avatar
Andrei Paskevich committed
542
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
543 544
	$(OCAMLLEX) $<

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
557 558 559 560 561 562 563 564
# 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
565 566 567 568 569 570 571 572 573 574 575

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
576
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
577 578 579 580
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
581
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
582 583 584 585 586 587 588
	      "--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
589
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
590

591
dep:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
592
	$(MAKE) depend
593
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
594
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
595

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
596 597 598
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
599 600
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
601
#
Andrei Paskevich's avatar
Andrei Paskevich committed
602 603 604
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
605
#
Andrei Paskevich's avatar
Andrei Paskevich committed
606
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
607 608 609 610 611
#       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
612 613 614 615 616 617 618
# 	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 \
619
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637
# 	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* \
638 639 640
#	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
641
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
642
#
Andrei Paskevich's avatar
Andrei Paskevich committed
643
# distrib export: source export-doc export-www export-examples export-examples-c linux
644
#
Andrei Paskevich's avatar
Andrei Paskevich committed
645 646 647 648
# 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
649
#
Andrei Paskevich's avatar
Andrei Paskevich committed
650 651
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
652
#
Andrei Paskevich's avatar
Andrei Paskevich committed
653 654 655 656 657 658
# 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
659 660
#
# tarball-for-framac:
Andrei Paskevich's avatar
Andrei Paskevich committed
661 662
# 	make tarball
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
663 664
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
665 666 667
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
# 	make export/$(NAME).tar.gz
668
#
Andrei Paskevich's avatar
Andrei Paskevich committed
669
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
670
#
Andrei Paskevich's avatar
Andrei Paskevich committed
671 672 673 674
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
# 	make -C $(WWW)/examples clean depend
# 	echo "*** faire make all dans $(WWW)/examples ***"
675
#
Andrei Paskevich's avatar
Andrei Paskevich committed
676 677 678 679 680 681
# 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
682
#
Andrei Paskevich's avatar
Andrei Paskevich committed
683 684 685 686 687 688 689 690
# 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)
691
#
Andrei Paskevich's avatar
Andrei Paskevich committed
692
# OSTYPE  ?= linux
693
#
Andrei Paskevich's avatar
Andrei Paskevich committed
694
# BINARYNAME = $(NAME)-$(OSTYPE)
695
#
Andrei Paskevich's avatar
Andrei Paskevich committed
696
# linux: binary
697 698 699
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
700 701 702 703 704
# 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
705

706
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
707
# file headers
708 709
###############

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

714
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
715
# myself
716
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
717

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
718
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
719 720 721 722
	./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
723

Andrei Paskevich's avatar
Andrei Paskevich committed
724 725 726 727
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
728 729 730
	./config.status --recheck

configure: configure.in
731
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
732

733
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
734
# clean and depend
735
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
736

737
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
738

739
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
740 741
	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
742 743 744 745 746 747 748 749

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