Makefile.in 25.9 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
#  Copyright (C) 2010-                                                   #
#    Francois Bobot                                                      #
#    Jean-Christophe Filliatre                                           #
#    Johannes Kanig                                                      #
#    Andrei Paskevich                                                    #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8 9 10
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
11
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12 13 14 15 16 17 18 19
#  described in file LICENSE.                                            #
#                                                                        #
#  This software is distributed in the hope that it will be useful,      #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
#                                                                        #
##########################################################################

Andrei Paskevich's avatar
Andrei Paskevich committed
20
include Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

22 23 24 25 26 27
VERBOSEMAKE ?= @enable_verbose_make@

ifeq ($(VERBOSEMAKE),yes)
  QUIET =
else
  QUIET = yes
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28 29
endif

30
# install the binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31
DESTDIR =
32

33
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

557
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
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

605

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
674 675 676
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
677

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682
doc/manual.pdf: doc/manual.tex doc/version.tex
683
	$(MAKE) -C doc manual.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
684 685

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
688
clean::
689
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
690

691
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
692
# API DOC
693
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
694

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
695 696
.PHONY: apidoc

697
apidoc:
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
698
	mkdir -p apidoc
Simon Cruanes's avatar
Simon Cruanes committed
699
	$(OCAMLDOC) -d apidoc -html -keep-code -I src $(LIBINCLUDES) -I +sqlite3 \
700
	    $(LIBML) $(LIBMLI) $(MNGML) $(MNGMLI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
701

702 703
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
704

705
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
706
# generic rules
707
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
708

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

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

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

718
%.cmxs: %.ml
719
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
720

Andrei Paskevich's avatar
Andrei Paskevich committed
721
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
722 723
	$(OCAMLLEX) $<

724
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
725 726
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
736 737 738 739 740 741 742 743
# 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
744 745 746 747 748 749 750 751 752 753 754

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
755
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
756 757 758 759
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
760
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
761 762 763 764
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
765 766
	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
767

768 769 770 771 772
# 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
773
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
775

776
dep: depend
777
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
778
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
779

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
780 781 782
# distrib
#########

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

890
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
891
# file headers
892 893
###############

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

898
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
899
# myself
900
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
901

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
902
Makefile: Makefile.in config.status
903
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
904

905
src/config.sh: src/config.sh.in config.status
906
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
907

908
src/config.ml: src/config.sh
909
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
910

Andrei Paskevich's avatar
Andrei Paskevich committed
911
doc/version.tex: doc/version.tex.in config.status
912
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
913 914

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
915 916 917
	./config.status --recheck

configure: configure.in
918
	autoconf
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
# clean and depend
922
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
923

924
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
925

926
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
927 928
	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
929

930 931 932 933
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
934 935 936 937 938 939 940
#################################################################
# 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:
941
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
942 943 944 945 946 947 948 949
# 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.