Makefile.in 26.7 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 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
		introduction abstraction
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
MARCHE Claude committed
381
IDE_FILES = gconfig scheduler gmain
MARCHE Claude's avatar
MARCHE Claude committed
382 383 384 385 386 387 388 389

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

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

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

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

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

399 400 401 402 403
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
404

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

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

# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

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

432 433 434 435
##############
# Coq plugin
##############

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

449
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
450

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

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

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

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

465 466 467 468
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
469

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

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

486 487 488 489
########
# Tptp2why
########

490 491
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
492

493
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
494

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

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

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

# build targets

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

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

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

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

# depend and clean targets

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

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

depend: .depend.tptp2why
533
endif
534 535 536 537 538

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

543 544 545 546
#######
# tools
#######

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

byte opt: $(TOOLS)

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

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

557
install_no_local::
558 559
	cp -f bin/why3-cpulimit $(BINDIR)

560 561 562 563 564 565
########
# bench
########

.PHONY: bench test

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

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

###############
582
# test targets
583
###############
584

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

733
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
734
# generic rules
735
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
736

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

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

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

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

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

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

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

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

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

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

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

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

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

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

otags:
793 794
	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
795

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
808 809 810
# distrib
#########

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

918
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
919
# file headers
920 921
###############

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

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

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

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

936
src/config.ml: src/config.sh
937
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
938

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

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

configure: configure.in
946
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
947

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

952
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
953

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

958 959 960 961
depend:
	rm -f $^
	$(MAKE) $^

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