Makefile.in 26.4 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
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 126
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
		inlining split_conjunction 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

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

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

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

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

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

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

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

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) $<
171
	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
172 173
	sed -i $(LIB_PARSER_INTERFACE) src/parser/parser.mli

174
# build targets
175

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

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

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

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

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

# depend target
192

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

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

depend: .depend.lib

200 201
# clean target

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

215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
###############
# installation
###############

install::
	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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
230
##################
231
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232 233 234 235 236
##################

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

237
bin/why.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
238 239
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240 241
	$(STRIP) $@

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

246 247
src/main.cmo: src/why.cmo
src/main.cmx: src/why.cmx
248

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
250
	rm -f src/main.cm[iox] src/main.annot src/main.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251
	rm -f bin/why.byte bin/why.opt
252

253 254 255
install::
	cp -f bin/why.@OCAMLBEST@ $(BINDIR)/why3

256 257 258
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
259

260 261
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
	       src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
262

263 264
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
265

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

268 269 270 271 272
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

273
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
274 275

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

277 278
byte: bin/whyml.byte
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279

280
bin/whyml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
281 282
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
283 284
	$(STRIP) $@

285
bin/whyml.byte: src/why.cma $(PGMCMO) src/main.cmo
286 287 288 289
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
290 291

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
296 297 298
depend: .depend.programs

clean::
299 300 301
	rm -f $(PGMGENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
302
	rm -f src/programs/*.output src/programs/*.automaton
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
303
	rm -f bin/whyml.byte bin/whyml.opt
304
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
305

306 307 308
# test target

%: %.mlw bin/whyml.byte
309
	bin/whyml.byte -P alt-ergo $*.mlw
310

311
install::
312
	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
313

314 315 316 317 318 319 320 321 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

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

install::
	cp -f bin/whyconfig.@OCAMLBEST@ $(BINDIR)/why3config


MARCHE Claude's avatar
MARCHE Claude committed
368 369 370 371
###############
# IDE
###############

MARCHE Claude's avatar
MARCHE Claude committed
372
IDE_FILES = gconfig scheduler gmain
MARCHE Claude's avatar
MARCHE Claude committed
373 374 375 376 377 378 379 380

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

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

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

383
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
384 385

ifeq (@enable_ide@,yes)
386 387
byte: bin/whyide.byte
opt:  bin/whyide.opt
MARCHE Claude's avatar
MARCHE Claude committed
388 389
endif

390 391 392 393 394
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2
# -I +sqlite3
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2
# sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
395

396
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
397
	$(if $(QUIET), @echo 'Linking  $@' &&) \
398
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
399 400
	$(STRIP) $@

401
bin/whyide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
402
	$(if $(QUIET),@echo 'Linking  $@' &&) \
403
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
404 405 406 407 408 409

# depend and clean targets

include .depend.ide

.depend.ide:
410
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
411 412 413 414 415 416

depend: .depend.ide

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

420 421 422
install::
	cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide

423 424 425 426
##############
# Coq plugin
##############

427 428 429 430 431 432 433 434 435 436 437 438 439
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))

440
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
441

Andrei Paskevich's avatar
Andrei Paskevich committed
442
ifeq (@enable_coq_support@,yes)
443 444
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
445
endif
446

447 448
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
449

450
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
451 452
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

453
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
454 455
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

456 457 458 459
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
460

461
ifeq (@enable_coq_support@,yes)
462 463 464 465 466 467
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
468
endif
469 470 471 472 473 474 475 476

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

477 478 479 480
########
# Tptp2why
########

481 482
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
483

484
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
485

486
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
487 488 489 490 491 492

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

493 494
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
495 496 497

# build targets

498
ifeq (@enable_whytptp@,yes)
499 500
byte: bin/whytptp.byte
opt:  bin/whytptp.opt
501 502 503 504
endif

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

506
bin/whytptp.opt: src/why.cmxa $(TPTPCMX) src/main.cmx
507
	$(if $(QUIET), @echo 'Linking  $@' &&) \
508
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
509 510
	$(STRIP) $@

511
bin/whytptp.byte: src/why.cma $(TPTPCMO) src/main.cmo
512
	$(if $(QUIET),@echo 'Linking  $@' &&) \
513
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
514 515 516

# depend and clean targets

517
ifeq (@enable_whytptp@,yes)
518 519 520 521 522 523
include .depend.tptp2why

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

depend: .depend.tptp2why
524
endif
525 526 527 528 529

clean::
	rm -f $(TPTPGENERATED)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
530
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
531
	rm -f bin/whytptp.byte bin/whytptp.opt
532 533
	rm -f .depend.tptp2why

534 535 536 537
#######
# tools
#######

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
538
TOOLS = bin/why3-cpulimit
539 540 541

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
542
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
543
	$(CC) -Wall -o $@ $^
544 545

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

548 549 550
install::
	cp -f bin/why3-cpulimit $(BINDIR)

551 552 553 554 555 556
########
# bench
########

.PHONY: bench test

MARCHE Claude's avatar
MARCHE Claude committed
557
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
558
	sh bench/bench \
559
	    "bin/why.@OCAMLBEST@" \
560
	    "bin/whyml.@OCAMLBEST@"
561

562
BENCH_PLUGINS_CMO := helloworld.cmo
563 564 565 566
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)
567
	bin/why.byte -D bench/plugins/helloworld.drv \
568
	tests/test-jcf.why -T Test -G G
569
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
570
	tests/test-jcf.why -T Test -G G
571 572

###############
573
# test targets
574
###############
575

576 577 578
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

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

598
testl: bin/whyml.byte
599
	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
600
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
601 602

testl-type: bin/whyml.byte
603
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
604

MARCHE Claude's avatar
MARCHE Claude committed
605 606 607 608
test-api: src/why.cma
	ocaml unix.cma str.cma nums.cma dynlink.cma ocamlgraph/graph.cma \
		src/why.cma -I src examples/use_api.ml

609

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
678 679 680
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
681

MARCHE Claude's avatar
MARCHE Claude committed
682 683
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
684

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

MARCHE Claude's avatar
MARCHE Claude committed
687 688 689
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
690 691

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
694
clean::
695
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696

697
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
698
# API DOC
699
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
701 702
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
703 704 705 706 707 708
MODULESTODOC = core/ident core/ty core/term core/decl core/theory \
	core/env core/task \
	driver/whyconf driver/driver 

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

709
apidoc:
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
710
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
711 712 713 714 715 716 717 718
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 

doc/apidoc.tex:
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
719

720 721
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
722

723
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
724
# generic rules
725
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
726

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

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

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

736
%.cmxs: %.ml
737
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
738

Andrei Paskevich's avatar
Andrei Paskevich committed
739
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
740 741
	$(OCAMLLEX) $<

742
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
743 744
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
754 755 756 757 758 759 760 761
# 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
762 763 764 765 766 767 768 769 770 771 772

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
773
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774 775 776 777
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
778
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
779 780 781 782
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
783 784
	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
785

786 787 788 789 790
# 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
791
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
792
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
793

794
dep: depend
795
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
796
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
797

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
798 799 800
# distrib
#########

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

908
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
909
# file headers
910 911
###############

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

916
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
917
# myself
918
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
919

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
920
Makefile: Makefile.in config.status
921
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
922

923
src/config.sh: src/config.sh.in config.status
924
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
925

926
src/config.ml: src/config.sh
927
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
928

Andrei Paskevich's avatar
Andrei Paskevich committed
929
doc/version.tex: doc/version.tex.in config.status
930
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
931 932

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
933 934 935
	./config.status --recheck

configure: configure.in
936
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
937

938
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
939
# clean and depend
940
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
941

942
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
943

944
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
945 946
	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
947

948 949 950 951
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
952 953 954 955 956 957 958
#################################################################
# 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:
959
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
960 961 962 963 964 965 966 967
# 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.