Makefile.in 28.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
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

Andrei Paskevich's avatar
Andrei Paskevich committed
86
ifeq (@enable_plugins@,yes)
87
  DYNLINK = dynlink
88
else
89
  DYNLINK =
90 91
endif

92
EXTOBJS =
93
EXTLIBS = str unix nums $(DYNLINK)
94 95 96

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
97

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
98 99 100
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106
#############
107
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109

110
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
111 112
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
113
	       src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114

115 116
LIB_UTIL = exn_printer debug pp loc print_tree \
	   hashweak hashcons util sysutil rc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
117

118
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
119

120
LIB_PARSER = ptree denv typing parser lexer
121

122
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
123
	     whyconf autodetection
124

125
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
126
		inlining split_goal \
127
		eliminate_definition eliminate_algebraic \
128
		eliminate_inductive eliminate_let eliminate_if \
129
		encoding_enumeration encoding encoding_decorate_mono \
130
		libencoding encoding_decorate encoding_bridge \
131
		encoding_explicit encoding_simple2 \
132
		encoding_instantiate simplify_array filter_trigger \
133
		introduction abstraction close_epsilon lift_epsilon
134

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

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

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

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

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

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

162
LIB_PARSER_POSTLUDE = \
163
  "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"
164 165 166 167 168 169 170 171

LIB_PARSER_INTERFACE = \
  -e "s/^val \+logic_file_eof *:/\0 Env.env ->/" \
  -e "s/^val \+list0_decl_eof *:/\0 Env.env -> \
  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"

src/parser/parser.ml src/parser/parser.mli: src/parser/parser.mly
	$(OCAMLYACC) $<
172
	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
173 174
	sed -i $(LIB_PARSER_INTERFACE) src/parser/parser.mli

175
# build targets
176

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

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

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

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

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

# depend target
193

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
194 195
include .depend.lib

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

depend: .depend.lib

201 202
# clean target

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

216 217 218
###############
# installation
###############
219
install_no_local::
220 221 222 223 224 225 226 227 228 229
	mkdir -p $(BINDIR)
	mkdir -p $(LIBDIR)/why3
	mkdir -p $(DATADIR)/why3/images
	mkdir -p $(DATADIR)/why3/lang
	cp -f --parents theories/*.why theories/*/*.why $(DATADIR)/why3/
	cp -f --parents drivers/*.drv $(DATADIR)/why3/
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

230 231 232 233 234 235 236 237 238
ifeq ("@ENABLE_LOCAL@","no")
install: install_no_local
else
install:
	@echo "You use a local configuration you can't install with it."
	@echo "Run ./configure without --enable-local"
endif


Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239
##################
240
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241 242 243 244 245
##################

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

246
bin/why.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
247 248
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249 250
	$(STRIP) $@

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

255 256
src/main.cmo: src/why.cmo
src/main.cmx: src/why.cmx
257

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
259
	rm -f src/main.cm[iox] src/main.annot src/main.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
260
	rm -f bin/why.byte bin/why.opt
261

262
install_no_local::
263 264
	cp -f bin/why.@OCAMLBEST@ $(BINDIR)/why3

265 266 267
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
268

269 270
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
	       src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
271

272 273
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
274

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

277 278 279 280 281
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

282
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
283 284

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

286 287
byte: bin/whyml.byte
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
288

289
bin/whyml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
290 291
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
292 293
	$(STRIP) $@

294
bin/whyml.byte: src/why.cma $(PGMCMO) src/main.cmo
295 296 297 298
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
299 300

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
305 306 307
depend: .depend.programs

clean::
308 309 310
	rm -f $(PGMGENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
311
	rm -f src/programs/*.output src/programs/*.automaton
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312
	rm -f bin/whyml.byte bin/whyml.opt
313
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
314

315 316 317
# test target

%: %.mlw bin/whyml.byte
318
	bin/whyml.byte -P alt-ergo $*.mlw
319

320
install_no_local::
321
	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
322

323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 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

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

373
install_no_local::
374 375 376
	cp -f bin/whyconfig.@OCAMLBEST@ $(BINDIR)/why3config


MARCHE Claude's avatar
MARCHE Claude committed
377 378 379 380
###############
# IDE
###############

MARCHE Claude's avatar
d  
MARCHE Claude committed
381
IDE_FILES = gconfig scheduler gmain
MARCHE Claude's avatar
MARCHE Claude committed
382 383 384 385 386 387 388 389

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

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

MARCHE Claude's avatar
d  
MARCHE Claude committed
390
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide 
MARCHE Claude's avatar
MARCHE Claude committed
391

392
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
393 394

ifeq (@enable_ide@,yes)
MARCHE Claude's avatar
d  
MARCHE Claude committed
395 396
byte: bin/whyide.byte 
opt:  bin/whyide.opt 
MARCHE Claude's avatar
MARCHE Claude committed
397 398
endif

MARCHE Claude's avatar
d  
MARCHE Claude committed
399
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 
400
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
MARCHE Claude's avatar
d  
MARCHE Claude committed
401
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
402

403
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
404
	$(if $(QUIET), @echo 'Linking  $@' &&) \
405
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
406 407
	$(STRIP) $@

408
bin/whyide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
409
	$(if $(QUIET),@echo 'Linking  $@' &&) \
410
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
411 412 413 414 415 416

# depend and clean targets

include .depend.ide

.depend.ide:
417
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
418 419 420 421 422 423

depend: .depend.ide

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

427
install_no_local::
428 429
	cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide

MARCHE Claude's avatar
d  
MARCHE Claude committed
430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 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

###############
# IDE WITH DB
###############

DB_FILES = gconfig scheduler db gdbmain

DBMODULES = $(addprefix src/ide/, $(DB_FILES))

DBML  = $(addsuffix .ml,  $(DBMODULES))
DBMLI = $(addsuffix .mli, $(DBMODULES))
DBCMO = $(addsuffix .cmo, $(DBMODULES))
DBCMX = $(addsuffix .cmx, $(DBMODULES))

$(DBCMO) $(DBCMX): INCLUDES += -I src/ide -I +sqlite3

# build targets

ifeq (@enable_ide@,yes)
byte: bin/whydb.byte 
opt:  bin/whydb.opt 
endif

bin/whydb.opt bin/whydb.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
bin/whydb.opt bin/whydb.byte: EXTOBJS += gtkThread
bin/whydb.opt bin/whydb.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3

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

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

# depend and clean targets

include .depend.db

.depend.db:
	$(OCAMLDEP) -slash -I src -I src/ide $(DBML) $(DBMLI) > $@

depend: .depend.db

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

install_no_local::
	cp -f bin/whydb.@OCAMLBEST@ $(BINDIR)/why3db

484 485 486 487
##############
# Coq plugin
##############

488 489 490 491 492 493 494 495 496 497 498 499 500
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))

501
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
502

Andrei Paskevich's avatar
Andrei Paskevich committed
503
ifeq (@enable_coq_support@,yes)
504 505
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
506
endif
507

508 509
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
510

511
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
512 513
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

514
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
515 516
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

517 518 519 520
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
521

522
ifeq (@enable_coq_support@,yes)
523 524 525 526 527 528
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
529
endif
530 531 532 533 534 535 536 537

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

538 539 540 541
########
# Tptp2why
########

542 543
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
544

545
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
546

547
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
548 549 550 551 552 553

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

554 555
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
556 557 558

# build targets

559
ifeq (@enable_whytptp@,yes)
560 561
byte: bin/whytptp.byte
opt:  bin/whytptp.opt
562 563 564 565
endif

bin/whytptp.opt bin/whytptp.byte: EXTOBJS += $(MENHIRLIB)
bin/whytptp.opt bin/whytptp.byte: INCLUDES += $(MENHIRINC)
566

567
bin/whytptp.opt: src/why.cmxa $(TPTPCMX) src/main.cmx
568
	$(if $(QUIET), @echo 'Linking  $@' &&) \
569
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
570 571
	$(STRIP) $@

572
bin/whytptp.byte: src/why.cma $(TPTPCMO) src/main.cmo
573
	$(if $(QUIET),@echo 'Linking  $@' &&) \
574
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
575 576 577

# depend and clean targets

578
ifeq (@enable_whytptp@,yes)
579 580 581 582 583 584
include .depend.tptp2why

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

depend: .depend.tptp2why
585
endif
586 587 588 589 590

clean::
	rm -f $(TPTPGENERATED)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
591
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
592
	rm -f bin/whytptp.byte bin/whytptp.opt
593 594
	rm -f .depend.tptp2why

595 596 597 598
#######
# tools
#######

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
599
TOOLS = bin/why3-cpulimit
600 601 602

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
603
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
604
	$(CC) -Wall -o $@ $^
605 606

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

609
install_no_local::
610 611
	cp -f bin/why3-cpulimit $(BINDIR)

612 613 614 615 616 617
########
# bench
########

.PHONY: bench test

MARCHE Claude's avatar
MARCHE Claude committed
618
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
619
	sh bench/bench \
620
	    "bin/why.@OCAMLBEST@" \
621
	    "bin/whyml.@OCAMLBEST@"
622

623
BENCH_PLUGINS_CMO := helloworld.cmo
624 625 626 627
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)
628
	bin/why.byte -D bench/plugins/helloworld.drv \
629
	tests/test-jcf.why -T Test -G G
630
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
631
	tests/test-jcf.why -T Test -G G
632 633

###############
634
# test targets
635
###############
636

637 638 639
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

640
test: bin/why.byte $(TOOLS)
641
	mkdir -p output_why3
642
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
643 644 645
	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
646
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
647
	@printf "*** Checking Coq file generation ***\\n"
648
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
649
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
650 651
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
652
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
653
		; do \
654
	  printf "Generating Coq file for $$i\\n" && \
655
	  	bin/why.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
656
	@printf "*** Checking Coq compilation ***\\n"
657
	@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
658

659
testl: bin/whyml.byte
660
	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
661
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
662

663 664 665
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

666
testl-type: bin/whyml.byte
667
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
668

MARCHE Claude's avatar
MARCHE Claude committed
669
test-api: src/why.cma
670
	ocaml unix.cma str.cma nums.cma dynlink.cma \
MARCHE Claude's avatar
MARCHE Claude committed
671 672
		src/why.cma -I src examples/use_api.ml \
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
673

674 675
## install: install-binary install-lib install-man
##
676
## BINARYFILES = $(BINARY) bin/whyide.$(OCAMLBEST)
677
##
Andrei Paskevich's avatar
Andrei Paskevich committed
678
## # install-binary should not depend on $(BINARYFILES); otherwise it
679
## # enforces the compilation of whyide, even when lablgtk2 is not installed
680
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
681 682
## 	mkdir -p $(BINDIR)
## 	cp -f $(BINARY) $(BINDIR)/why$(EXE)
683 684
## 	if test -f bin/whyide.$(OCAMLBEST); then \
## 		cp -f bin/whyide.$(OCAMLBEST) $(BINDIR)/whyide-bin$(EXE); \
Andrei Paskevich's avatar
Andrei Paskevich committed
685
## 	fi
686 687
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
688
## 	mkdir -p $(LIBDIR)/why/why
689
##
Andrei Paskevich's avatar
Andrei Paskevich committed
690 691 692
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
693
##
Andrei Paskevich's avatar
Andrei Paskevich committed
694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709
## 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
710
##
Andrei Paskevich's avatar
Andrei Paskevich committed
711 712 713 714 715 716 717 718
## 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 ======"
719
##
Andrei Paskevich's avatar
Andrei Paskevich committed
720 721 722 723 724
## 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
725
##
726
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/whyide.$(OCAMLBEST) byte bin/whyide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
727 728 729
## 	cp $(BINARY) $$HOME/bin/why
## 	cp $(WHYCONFIG) $$HOME/bin/why
## 	cp $(JESSIE) $$HOME/bin/jessie
730 731
## 	if test -f bin/whyide.$(OCAMLBEST); then \
## 	  cp -f bin/whyide.$(OCAMLBEST) $$HOME/bin/whyide; \
Andrei Paskevich's avatar
Andrei Paskevich committed
732
## 	fi
733
##
Andrei Paskevich's avatar
Andrei Paskevich committed
734
## local: install
735
##
Andrei Paskevich's avatar
Andrei Paskevich committed
736 737
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
738
##
Andrei Paskevich's avatar
Andrei Paskevich committed
739 740
## 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
741

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
742 743 744
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
745

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

MARCHE Claude's avatar
MARCHE Claude committed
749
doc: $(DOC) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
750

MARCHE Claude's avatar
MARCHE Claude committed
751 752 753
doc/manual.pdf: doc/apidoc.tex doc/manual.tex doc/version.tex
	cd doc; pdflatex manual
	cd doc; pdflatex manual
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
754 755

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
758
clean::
759
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
760

761
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
762
# API DOC
763
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
764

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
765 766
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
767 768
MODULESTODOC = core/ident core/ty core/term core/decl core/theory \
	core/env core/task \
769
	driver/whyconf driver/driver \
770 771
	transform/introduction \
	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
772 773 774

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

775
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
776
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
777 778 779 780
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 

MARCHE Claude's avatar
MARCHE Claude committed
781
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
782 783 784
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
785

786 787
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
788

789
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
790
# generic rules
791
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
792

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

MARCHE Claude's avatar
MARCHE Claude committed
796
%.cmo %.cmi: %.ml
797
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
798

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

802
%.cmxs: %.ml
803
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
804

Andrei Paskevich's avatar
Andrei Paskevich committed
805
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
806 807
	$(OCAMLLEX) $<

808
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
809 810
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
820 821 822 823 824 825 826 827
# 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
828 829 830 831 832 833 834 835 836 837 838

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

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

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

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

otags:
849 850
	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
851

852 853 854 855 856
# 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
857
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
858
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
859

860
dep: depend
861
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
862
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
863

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
864 865 866
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
867 868
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
869
#
Andrei Paskevich's avatar
Andrei Paskevich committed
870 871 872
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
873
#
874
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/whyide.sh \
875 876 877 878 879
#       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
880 881 882 883 884 885 886
# 	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 \
887
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905
# 	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* \
906 907 908
#	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
909
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
910
#
Andrei Paskevich's avatar
Andrei Paskevich committed
911
# distrib export: source export-doc export-www export-examples export-examples-c linux
912
#
Andrei Paskevich's avatar
Andrei Paskevich committed
913 914 915
# 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
916
# 	$(MAKE) -C /users/demons/filliatr/www/why install
917
#
Andrei Paskevich's avatar
Andrei Paskevich committed
918 919
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
920
#
Andrei Paskevich's avatar
Andrei Paskevich committed
921 922 923 924 925 926
# 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
927 928
#
# tarball-for-framac:
929
# 	$(MAKE) tarball
Andrei Paskevich's avatar
Andrei Paskevich committed
930
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
931 932
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
933 934
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
935
# 	$(MAKE) export/$(NAME).tar.gz
936
#
Andrei Paskevich's avatar
Andrei Paskevich committed
937
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
938
#
Andrei Paskevich's avatar
Andrei Paskevich committed
939 940
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
941
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
942
# 	echo "*** faire make all dans $(WWW)/examples ***"
943
#
Andrei Paskevich's avatar
Andrei Paskevich committed
944 945 946 947 948 949
# 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
950
#
Andrei Paskevich's avatar
Andrei Paskevich committed
951 952 953 954 955 956 957 958
# 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)
959
#
Andrei Paskevich's avatar
Andrei Paskevich committed
960
# OSTYPE  ?= linux
961
#
Andrei Paskevich's avatar
Andrei Paskevich committed
962
# BINARYNAME = $(NAME)-$(OSTYPE)
963
#
Andrei Paskevich's avatar
Andrei Paskevich committed
964
# linux: binary
965 966 967
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
968 969 970 971 972
# 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
973

974
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
975
# file headers
976 977
###############

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

982
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
983
# myself
984
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
985

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
986
Makefile: Makefile.in config.status
987
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
988

989
src/config.sh: src/config.sh.in config.status
990
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
991

992
src/config.ml: src/config.sh
993
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
994

Andrei Paskevich's avatar
Andrei Paskevich committed
995
doc/version.tex: doc/version.tex.in config.status
996
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
997 998

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
999 1000 1001
	./config.status --recheck

configure: configure.in
1002
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1003

1004
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1005
# clean and depend
1006
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1007

1008
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1009

1010
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
1011 1012
	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
1013

1014 1015 1016 1017
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1018 1019 1020 1021 1022 1023 1024
#################################################################
# 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:
1025
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1026 1027 1028 1029 1030 1031 1032 1033
# 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.