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

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

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

120
LIB_PARSER = ptree denv typing parser lexer
121

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

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

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

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

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

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

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

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

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

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

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

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

179
# build targets
180

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

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

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

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

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

# depend target
197

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

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

depend: .depend.lib

205 206
# clean target

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

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

240 241 242 243 244 245 246 247 248
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
249
##################
250
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251 252 253 254 255
##################

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

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

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

265 266
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
267

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

272
install_no_local::
273 274
	cp -f bin/why.@OCAMLBEST@ $(BINDIR)/why3

275 276 277
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
278

279 280
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
	       src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
281

282 283
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
284

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

287 288 289 290 291
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

292
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
293 294

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

296 297
byte: bin/whyml.byte
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
298

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

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

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
309 310

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
315 316 317
depend: .depend.programs

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

325 326
# test target

327 328 329 330
%.gui: %.why bin/whyide.opt
	bin/whyide.opt $*.why

%.gui: %.mlw bin/whyide.opt
331
	bin/whyide.opt $*.mlw
332

333
install_no_local::
334
	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
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 373 374 375 376 377 378 379 380 381 382 383 384 385

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

386
install_no_local::
387 388 389
	cp -f bin/whyconfig.@OCAMLBEST@ $(BINDIR)/why3config


MARCHE Claude's avatar
MARCHE Claude committed
390 391 392 393
###############
# IDE
###############

394 395
ifeq (@enable_ide@,yes)

396
IDE_FILES = gconfig scheduler db gmain
MARCHE Claude's avatar
MARCHE Claude committed
397 398 399 400 401 402 403 404

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

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

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

407
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
408

409 410
byte: bin/whyide.byte
opt:  bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
411

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

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

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

# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

440
install_no_local::
441 442
	cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide

443
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
444

445

446 447 448 449
##############
# Coq plugin
##############

450 451 452 453 454 455 456 457 458 459 460 461 462
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))

463
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
464

Andrei Paskevich's avatar
Andrei Paskevich committed
465
ifeq (@enable_coq_support@,yes)
466 467
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
468
endif
469

470 471
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
472

473
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
474 475
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

476
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
477 478
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

479 480 481 482
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
483

484
ifeq (@enable_coq_support@,yes)
485 486 487 488 489 490
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
491
endif
492 493 494 495 496 497 498 499

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

500 501 502 503
########
# Tptp2why
########

504 505
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
506

François Bobot's avatar
François Bobot committed
507
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
508

509
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
510 511 512 513 514 515

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

516 517
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
518 519 520

# build targets

521
ifeq (@enable_whytptp@,yes)
François Bobot's avatar
François Bobot committed
522 523
byte: plugins/whytptp.cmo
opt:  plugins/whytptp.cmxs
524 525
endif

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

François Bobot's avatar
François Bobot committed
529 530 531 532
plugins:
	@mkdir plugins

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

François Bobot's avatar
François Bobot committed
536
src/tptp2why/whytptp.cmo: $(TPTPCMO)
537
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
538 539 540 541 542 543 544
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

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

plugins/whytptp.cmo: plugins src/tptp2why/whytptp.cmo
	@cp src/tptp2why/whytptp.cmo $@
545 546 547

# depend and clean targets

548
ifeq (@enable_whytptp@,yes)
549 550 551 552 553 554
include .depend.tptp2why

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

depend: .depend.tptp2why
555
endif
556 557 558 559 560

clean::
	rm -f $(TPTPGENERATED)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
561
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
562
	rm -f bin/whytptp.byte bin/whytptp.opt
563 564
	rm -f .depend.tptp2why

565 566 567 568
#######
# tools
#######

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
569
TOOLS = bin/why3-cpulimit
570 571 572

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
573
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
574
	$(CC) -Wall -o $@ $^
575 576

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

579
install_no_local::
580 581
	cp -f bin/why3-cpulimit $(BINDIR)

582 583 584 585
########
# bench
########

François Bobot's avatar
François Bobot committed
586
.PHONY: bench test comp_bench_plugins
587

MARCHE Claude's avatar
MARCHE Claude committed
588
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
589
	sh bench/bench \
590
	    "bin/why.@OCAMLBEST@" \
591
	    "bin/whyml.@OCAMLBEST@"
592

593
BENCH_PLUGINS_CMO := helloworld.cmo
594 595 596
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

François Bobot's avatar
François Bobot committed
597 598 599 600 601 602 603
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

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

###############
606
# test targets
607
###############
608

609 610 611
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

612
test: bin/why.byte $(TOOLS)
613
	mkdir -p output_why3
614
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
615 616 617
	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
618
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
619
	@printf "*** Checking Coq file generation ***\\n"
620
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
621
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
622 623
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
624
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
625
		; do \
626
	  printf "Generating Coq file for $$i\\n" && \
627
	  	bin/why.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
628
	@printf "*** Checking Coq compilation ***\\n"
629
	@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
630

631
testl: bin/whyml.byte
632
	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
633
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
634

635 636 637
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

638
testl-type: bin/whyml.byte
639
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
640

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

645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688

## Examples : Plugins ##

PLUGDIR = examples/plugins/
PLUG_FILES = genequlin

PLUGMODULES = $(addprefix $(PLUGDIR), $(PLUG_FILES))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES))

# ifeq (@enable_plug_support@,yes)
# byte: src/plug-plugin/whytac.cma
# opt:  src/plug-plugin/whytac.cmxs
# endif

# $(PLUGCMO):  src/why.cma
# $(PLUGCMXS): src/why.cmxa

.PHONY: examples_plugins.byte examples_plugins.opt

examples_plugins.byte : $(PLUGCMO)
examples_plugins.opt : $(PLUGCMXS)

# depend and clean targets

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

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

depend: .depend.plug
endif

clean::
	rm -f $(PLUGDIR)/*.cm[iox] $(PLUGDIR)/*.o
	rm -f $(PLUGDIR)/*.cma $(PLUGDIR)/*.cmxs
	rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~
	rm -f $(PLUGGENERATED)
	rm -f .depend.plug

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
757 758 759
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
760

MARCHE Claude's avatar
MARCHE Claude committed
761 762
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
763

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

MARCHE Claude's avatar
MARCHE Claude committed
766 767 768
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
769 770

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
773
clean::
774
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
775

776
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
777
# API DOC
778
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
779

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
780 781
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
782 783
MODULESTODOC = core/ident core/ty core/term core/decl core/theory \
	core/env core/task \
784
	driver/whyconf driver/driver \
785 786
	transform/introduction \
	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
787 788 789

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

790
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
791
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
792 793
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
794
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
795

MARCHE Claude's avatar
MARCHE Claude committed
796
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
797 798
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
799
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
800

801 802
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
803

804
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
805
# generic rules
806
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
807

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

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

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

817
%.cmxs: %.ml
818
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
819

Andrei Paskevich's avatar
Andrei Paskevich committed
820
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
821 822
	$(OCAMLLEX) $<

823
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
824 825
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
835 836 837 838 839 840 841 842
# 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
843 844 845 846 847 848 849 850 851 852 853

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
854
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
855 856 857 858
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
859
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
860 861 862 863
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
864 865
	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
866

867 868 869 870 871
# 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
872
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
873
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
874

875
dep: depend
876
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
877
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
878

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
879 880 881
# distrib
#########

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

989
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
990
# file headers
991 992
###############

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

997
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
998
# myself
999
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
1000

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1001
Makefile: Makefile.in config.status
1002
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1003

1004
src/config.sh: src/config.sh.in config.status
1005
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1006

1007
src/config.ml: src/config.sh
1008
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
1009

Andrei Paskevich's avatar
Andrei Paskevich committed
1010
doc/version.tex: doc/version.tex.in config.status
1011
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
1012 1013

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1014 1015 1016
	./config.status --recheck

configure: configure.in
1017
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1018

1019
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1020
# clean and depend
1021
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1022

1023
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1024

1025
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
1026 1027
	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
1028

1029 1030 1031 1032
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1033 1034 1035 1036 1037 1038 1039
#################################################################
# 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:
1040
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1041 1042 1043 1044 1045 1046 1047 1048
# 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.