Makefile.in 26.8 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 \
Johannes Kanig's avatar
Johannes Kanig committed
133
		introduction abstraction close_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
db  
MARCHE Claude committed
381
IDE_FILES = gconfig scheduler db 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))

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

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

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

MARCHE Claude's avatar
db  
MARCHE Claude committed
399
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
400
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
MARCHE Claude's avatar
db  
MARCHE Claude committed
401
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
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

430 431 432 433
##############
# Coq plugin
##############

434 435 436 437 438 439 440 441 442 443 444 445 446
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))

447
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
448

Andrei Paskevich's avatar
Andrei Paskevich committed
449
ifeq (@enable_coq_support@,yes)
450 451
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
452
endif
453

454 455
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
456

457
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
458 459
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

460
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
461 462
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

463 464 465 466
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
467

468
ifeq (@enable_coq_support@,yes)
469 470 471 472 473 474
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
475
endif
476 477 478 479 480 481 482 483

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

484 485 486 487
########
# Tptp2why
########

488 489
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
490

491
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
492

493
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
494 495 496 497 498 499

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

500 501
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
502 503 504

# build targets

505
ifeq (@enable_whytptp@,yes)
506 507
byte: bin/whytptp.byte
opt:  bin/whytptp.opt
508 509 510 511
endif

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

513
bin/whytptp.opt: src/why.cmxa $(TPTPCMX) src/main.cmx
514
	$(if $(QUIET), @echo 'Linking  $@' &&) \
515
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
516 517
	$(STRIP) $@

518
bin/whytptp.byte: src/why.cma $(TPTPCMO) src/main.cmo
519
	$(if $(QUIET),@echo 'Linking  $@' &&) \
520
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
521 522 523

# depend and clean targets

524
ifeq (@enable_whytptp@,yes)
525 526 527 528 529 530
include .depend.tptp2why

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

depend: .depend.tptp2why
531
endif
532 533 534 535 536

clean::
	rm -f $(TPTPGENERATED)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
537
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
538
	rm -f bin/whytptp.byte bin/whytptp.opt
539 540
	rm -f .depend.tptp2why

541 542 543 544
#######
# tools
#######

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
545
TOOLS = bin/why3-cpulimit
546 547 548

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
549
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
550
	$(CC) -Wall -o $@ $^
551 552

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

555
install_no_local::
556 557
	cp -f bin/why3-cpulimit $(BINDIR)

558 559 560 561 562 563
########
# bench
########

.PHONY: bench test

MARCHE Claude's avatar
MARCHE Claude committed
564
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
565
	sh bench/bench \
566
	    "bin/why.@OCAMLBEST@" \
567
	    "bin/whyml.@OCAMLBEST@"
568

569
BENCH_PLUGINS_CMO := helloworld.cmo
570 571 572 573
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)
574
	bin/why.byte -D bench/plugins/helloworld.drv \
575
	tests/test-jcf.why -T Test -G G
576
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
577
	tests/test-jcf.why -T Test -G G
578 579

###############
580
# test targets
581
###############
582

583 584 585
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

586
test: bin/why.byte $(TOOLS)
587
	mkdir -p output_why3
588
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
589 590 591
	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
592
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
593
	@printf "*** Checking Coq file generation ***\\n"
594
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
595
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
596 597
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
598
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
599
		; do \
600
	  printf "Generating Coq file for $$i\\n" && \
601
	  	bin/why.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
602
	@printf "*** Checking Coq compilation ***\\n"
603
	@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
604

605
testl: bin/whyml.byte
606
	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
607
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
608

609 610 611
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

612
testl-type: bin/whyml.byte
613
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
614

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

620 621
## install: install-binary install-lib install-man
##
622
## BINARYFILES = $(BINARY) bin/whyide.$(OCAMLBEST)
623
##
Andrei Paskevich's avatar
Andrei Paskevich committed
624
## # install-binary should not depend on $(BINARYFILES); otherwise it
625
## # enforces the compilation of whyide, even when lablgtk2 is not installed
626
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
627 628
## 	mkdir -p $(BINDIR)
## 	cp -f $(BINARY) $(BINDIR)/why$(EXE)
629 630
## 	if test -f bin/whyide.$(OCAMLBEST); then \
## 		cp -f bin/whyide.$(OCAMLBEST) $(BINDIR)/whyide-bin$(EXE); \
Andrei Paskevich's avatar
Andrei Paskevich committed
631
## 	fi
632 633
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
634
## 	mkdir -p $(LIBDIR)/why/why
635
##
Andrei Paskevich's avatar
Andrei Paskevich committed
636 637 638
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
639
##
Andrei Paskevich's avatar
Andrei Paskevich committed
640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655
## 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
656
##
Andrei Paskevich's avatar
Andrei Paskevich committed
657 658 659 660 661 662 663 664
## 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 ======"
665
##
Andrei Paskevich's avatar
Andrei Paskevich committed
666 667 668 669 670
## 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
671
##
672
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/whyide.$(OCAMLBEST) byte bin/whyide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
673 674 675
## 	cp $(BINARY) $$HOME/bin/why
## 	cp $(WHYCONFIG) $$HOME/bin/why
## 	cp $(JESSIE) $$HOME/bin/jessie
676 677
## 	if test -f bin/whyide.$(OCAMLBEST); then \
## 	  cp -f bin/whyide.$(OCAMLBEST) $$HOME/bin/whyide; \
Andrei Paskevich's avatar
Andrei Paskevich committed
678
## 	fi
679
##
Andrei Paskevich's avatar
Andrei Paskevich committed
680
## local: install
681
##
Andrei Paskevich's avatar
Andrei Paskevich committed
682 683
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
684
##
Andrei Paskevich's avatar
Andrei Paskevich committed
685 686
## 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
687

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
688 689 690
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
691

MARCHE Claude's avatar
MARCHE Claude committed
692 693
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
694

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

MARCHE Claude's avatar
MARCHE Claude committed
697 698 699
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
700 701

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
704
clean::
705
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
706

707
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
708
# API DOC
709
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
710

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
711 712
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
713 714
MODULESTODOC = core/ident core/ty core/term core/decl core/theory \
	core/env core/task \
715
	driver/whyconf driver/driver \
716 717
	transform/introduction \
	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
718 719 720

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

721
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
722
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
723 724 725 726
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 

MARCHE Claude's avatar
MARCHE Claude committed
727
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
728 729 730
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
731

732 733
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
734

735
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
736
# generic rules
737
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
738

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

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

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

748
%.cmxs: %.ml
749
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
750

Andrei Paskevich's avatar
Andrei Paskevich committed
751
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
752 753
	$(OCAMLLEX) $<

754
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
755 756
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
766 767 768 769 770 771 772 773
# 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
774 775 776 777 778 779 780 781 782 783 784

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
785
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
786 787 788 789
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
790
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
791 792 793 794
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
795 796
	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
797

798 799 800 801 802
# 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
803
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
804
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
805

806
dep: depend
807
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
808
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
809

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
810 811 812
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
813 814
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
815
#
Andrei Paskevich's avatar
Andrei Paskevich committed
816 817 818
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
819
#
820
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/whyide.sh \
821 822 823 824 825
#       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
826 827 828 829 830 831 832
# 	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 \
833
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851
# 	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* \
852 853 854
#	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
855
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
856
#
Andrei Paskevich's avatar
Andrei Paskevich committed
857
# distrib export: source export-doc export-www export-examples export-examples-c linux
858
#
Andrei Paskevich's avatar
Andrei Paskevich committed
859 860 861
# 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
862
# 	$(MAKE) -C /users/demons/filliatr/www/why install
863
#
Andrei Paskevich's avatar
Andrei Paskevich committed
864 865
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
866
#
Andrei Paskevich's avatar
Andrei Paskevich committed
867 868 869 870 871 872
# 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
873 874
#
# tarball-for-framac:
875
# 	$(MAKE) tarball
Andrei Paskevich's avatar
Andrei Paskevich committed
876
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
877 878
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
879 880
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
881
# 	$(MAKE) export/$(NAME).tar.gz
882
#
Andrei Paskevich's avatar
Andrei Paskevich committed
883
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
884
#
Andrei Paskevich's avatar
Andrei Paskevich committed
885 886
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
887
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
888
# 	echo "*** faire make all dans $(WWW)/examples ***"
889
#
Andrei Paskevich's avatar
Andrei Paskevich committed
890 891 892 893 894 895
# 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
896
#
Andrei Paskevich's avatar
Andrei Paskevich committed
897 898 899 900 901 902 903 904
# 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)
905
#
Andrei Paskevich's avatar
Andrei Paskevich committed
906
# OSTYPE  ?= linux
907
#
Andrei Paskevich's avatar
Andrei Paskevich committed
908
# BINARYNAME = $(NAME)-$(OSTYPE)
909
#
Andrei Paskevich's avatar
Andrei Paskevich committed
910
# linux: binary
911 912 913
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
914 915 916 917 918
# 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
919

920
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
921
# file headers
922 923
###############

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

928
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
929
# myself
930
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
931

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
932
Makefile: Makefile.in config.status
933
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
934

935
src/config.sh: src/config.sh.in config.status
936
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
937

938
src/config.ml: src/config.sh
939
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
940

Andrei Paskevich's avatar
Andrei Paskevich committed
941
doc/version.tex: doc/version.tex.in config.status
942
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
943 944

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
945 946 947
	./config.status --recheck

configure: configure.in
948
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
949

950
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
951
# clean and depend
952
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
953

954
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
955

956
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
957 958
	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
959

960 961 962 963
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
964 965 966 967 968 969 970
#################################################################
# 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:
971
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
972 973 974 975 976 977 978 979
# 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.