Makefile.in 23.2 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 34 35 36 37 38 39 40

prefix 	    = @prefix@
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
DATADIR = $(DESTDIR)@datadir@
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
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
60
#PDFVIEWER = @PDFVIEWER@
61

62 63
BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -dtypes    -I src $(INCLUDES)
64 65 66

# external libraries common to all binaries

Andrei Paskevich's avatar
Andrei Paskevich committed
67
ifeq (@enable_plugins@,yes)
68
  DYNLINK = dynlink
69
else
70
  DYNLINK =
71 72
endif

73 74 75
EXTLIBS = str unix nums $(DYNLINK)
EXTCMA	= $(addsuffix .cma,$(EXTLIBS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77 78 79
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
81
all: @OCAMLBEST@
Francois Bobot's avatar
Francois Bobot committed
82

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83
.PHONY: byte opt clean depend all
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
#############
86
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88

89
LIBGENERATED = src/util/rc.ml \
90 91 92 93
	       src/parser/parser.mli src/parser/parser.ml \
	       src/parser/parser.output src/parser/lexer.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
	       src/driver/driver_parser.output src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94

Andrei Paskevich's avatar
Andrei Paskevich committed
95
LIB_UTIL = pp loc print_tree hashweak util hashcons sysutil rc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96

97
LIB_CORE = ident ty term pattern decl theory task pretty trans env
98

99
LIB_PARSER = ptree parser lexer denv typing
100

101 102
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
	     register prover whyconf
103

104 105
LIB_TRANSFORM = simplify_recursive_definition inlining \
		split_conjunction encoding_decorate \
106
		eliminate_definition eliminate_algebraic \
107
		eliminate_inductive eliminate_let eliminate_if
108

109
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp
110

111 112 113 114 115 116
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)) \
117
	      $(addprefix src/printer/, $(LIB_PRINTER))
118

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

122 123 124 125
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
126

127 128
$(LIBCMO) $(LIBCMX): INCLUDES = $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why
129

130
# build targets
131

132 133
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134

135
src/why.cma: src/why.cmo
136 137
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

138
src/why.cmxa: src/why.cmx
139 140
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

141 142
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
143

144 145 146 147
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
148

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
149 150
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
151
.depend.lib: src/config.ml $(LIBGENERATED)
152
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
153 154 155

depend: .depend.lib

156 157
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
158
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
159 160 161 162 163 164 165 166
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
	   $(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
167
	rm -f .depend.lib
168

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169
##################
170
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171 172 173 174 175
##################

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

176
bin/why.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
177 178
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
179 180
	$(STRIP) $@

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

185 186
src/main.cmo: src/why.cmo
src/main.cmx: src/why.cmx
187

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
188
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
189
	rm -f src/main.cm[iox] src/main.annot src/main.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
190
	rm -f bin/why.byte bin/why.opt
191

192 193 194
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
195

196 197
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
	       src/programs/pgm_parser.output src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
198

199
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
200

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

203 204 205 206 207 208 209 210
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

$(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212
byte: bin/whyml.byte
213
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214

215
bin/whyml.opt: src/why.cmxa $(PGMCMX)
216 217
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
218 219
	$(STRIP) $@

220
bin/whyml.byte: src/why.cma $(PGMCMO)
221 222 223 224
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225 226

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
231 232 233
depend: .depend.programs

clean::
234 235 236
	rm -f $(PGMGENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
237
	rm -f bin/whyml.byte bin/whyml.opt
238
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239 240

###############
241
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242 243
###############

244 245 246 247 248 249 250 251 252 253 254
MNG_FILES = db test

MNGMODULES = $(addprefix src/manager/, $(MNG_FILES))

MNGML  = $(addsuffix .ml,  $(MNGMODULES))
MNGMLI = $(addsuffix .mli, $(MNGMODULES))
MNGCMO = $(addsuffix .cmo, $(MNGMODULES))
MNGCMX = $(addsuffix .cmx, $(MNGMODULES))

$(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3

255
ifeq (@enable_proof_manager@,yes)
MARCHE Claude's avatar
MARCHE Claude committed
256 257
byte: bin/manager.byte
opt:  bin/manager.opt
258
endif
259

MARCHE Claude's avatar
MARCHE Claude committed
260 261
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3

262
bin/manager.opt: src/why.cmxa $(MNGCMX)
263
	$(if $(QUIET), @echo 'Linking  $@' &&) \
MARCHE Claude's avatar
MARCHE Claude committed
264
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^
265
	$(STRIP) $@
MARCHE Claude's avatar
MARCHE Claude committed
266

267
bin/manager.byte: src/why.cma $(MNGCMO)
268 269
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
270

271
# depend and clean targets
MARCHE Claude's avatar
MARCHE Claude committed
272 273 274

include .depend.manager

275
.depend.manager:
276
	$(OCAMLDEP) -slash -I src -I src/manager $(MNGML) $(MNGMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
277

278
depend: .depend.manager
MARCHE Claude's avatar
MARCHE Claude committed
279 280

clean::
281 282
	rm -f src/manager/*.cm[iox] src/manager/*.o
	rm -f src/manager/*.annot src/manager/*~
MARCHE Claude's avatar
MARCHE Claude committed
283
	rm -f bin/manager.byte bin/manager.opt
284
	rm -f .depend.manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
285

286
#####################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287 288 289
# graphical interface
#####################

290
IDE_FILES = ide_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
291

292 293 294 295 296 297 298 299 300 301
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))

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

$(IDECMO) $(IDECMX): INCLUDES = -I src/ide -I +lablgtk2 -I +threads

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

Andrei Paskevich's avatar
Andrei Paskevich committed
303 304 305 306
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt:  bin/whyide.opt
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
307

MARCHE Claude's avatar
MARCHE Claude committed
308 309
bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads

310
bin/whyide.opt: src/why.cmxa $(IDE_CMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
311 312 313 314
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
	    lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
	$(STRIP) $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
315

MARCHE Claude's avatar
MARCHE Claude committed
316

317
bin/whyide.byte: src/why.cma $(IDE_CMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
318 319 320
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
	    lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321

322 323
# depend and clean targets

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324 325 326
include .depend.ide

.depend.ide:
327
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328 329 330 331

depend: .depend.ide

clean::
332 333
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334
	rm -f bin/whyide.byte bin/whyide.opt
335
	rm -f .depend.ide
MARCHE Claude's avatar
MARCHE Claude committed
336

337 338 339 340
##############
# Coq plugin
##############

341 342 343 344 345 346 347 348 349 350 351 352 353 354 355
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))

$(COQCMO) $(COQCMX): INCLUDES = $(COQINCLUDES)

Andrei Paskevich's avatar
Andrei Paskevich committed
356
ifeq (@enable_coq_support@,yes)
357 358
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
359
endif
360

361 362
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
363

364
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
365 366
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

367
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
368 369
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

370 371 372 373
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
374
ifeq (@enable_coq_support@,yes)
375
include .depend.coq
376
endif
377 378 379 380 381 382 383 384 385 386 387 388 389

.depend.coq: $(COQGENERATED)
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

depend: .depend.coq

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

390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444
########
# Tptp2why
########

# TODO : autoconf
MENHIR=/usr/bin/menhir

TPTPGENERATED = src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli \
				src/tptp2why/tptp_parser.output src/tptp2why/tptp_lexer.ml

TPTP_FILES = tptpTree tptp_parser tptp_lexer tptp2why
TPTP_DIR=src/tptp2why/

TPTPMODULES = $(addprefix $(TPTP_DIR), $(TPTP_FILES))

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

$(TPTPCMO) $(TPTPCMX): INCLUDES = -I $(TPTP_DIR)

# build targets

byte: bin/tptp2why.byte
opt:  bin/tptp2why.opt

src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli: src/tptp2why/tptpTree.cmi src/tptp2why/tptp_parser.mly
	cd $(TPTP_DIR) && $(MENHIR) --infer tptp_parser.mly

bin/tptp2why.opt: $(TPTPCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $^
	$(STRIP) $@

bin/tptp2why.byte: $(TPTPCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $^

# depend and clean targets

include .depend.tptp2why

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

depend: .depend.tptp2why

clean::
	rm -f $(TPTPGENERATED)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
	rm -f bin/tptp2why.byte bin/tptp2why.opt
	rm -f .depend.tptp2why

445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466
#######
# tools
#######

TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

bin/why-cpulimit: src/tools/@CPULIMIT@.c
	$(CC) -o $@ $^

clean::
	rm -f bin/why-cpulimit src/tools/*~

########
# bench
########

.PHONY: bench test

bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
	sh bench/bench \
467
	    "bin/why.@OCAMLBEST@" \
468 469 470 471 472 473 474
	    "bin/whyml.@OCAMLBEST@ -I theories"

BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
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)
475 476 477 478 479 480
	bin/why.byte -D bench/plugins/helloworld.drv \
	tests/test-jcf.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
	tests/test-jcf.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/simplify_array.drv \
	tests/test-jcf.why -t Test_simplify_array -g G
481 482

###############
483
# test targets
484
###############
485

486
test: bin/why.byte $(TOOLS)
487
	mkdir -p output_why3
488 489 490 491 492
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
	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
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
493
	@printf "*** Checking Coq file generation ***\\n"
494
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
495
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
496 497
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
498
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
499
		; do \
500 501
	  printf "Generating Coq file for $$i\\n" && \
	  	bin/why.byte -P coq -o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
502
	@printf "*** Checking Coq compilation ***\\n"
503
	@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
504

505
testl: bin/whyml.byte
506
	ocamlrun -bt bin/whyml.byte -I theories/ tests/test-pgm-jcf.mlw
507

508 509
examples/programs/%: bin/whyml.byte
	bin/whyml.byte -I theories examples/programs/$*.mlw
510

511
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
512
# installation
513
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
514

515 516 517 518
## install: install-binary install-lib install-man
##
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST)
##
Andrei Paskevich's avatar
Andrei Paskevich committed
519 520
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
521
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
522 523 524 525 526
## 	mkdir -p $(BINDIR)
## 	cp -f $(BINARY) $(BINDIR)/why$(EXE)
## 	if test -f bin/why-ide.$(OCAMLBEST); then \
## 		cp -f bin/why-ide.$(OCAMLBEST) $(BINDIR)/why-ide-bin$(EXE); \
## 	fi
527 528
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
529
## 	mkdir -p $(LIBDIR)/why/why
530
##
Andrei Paskevich's avatar
Andrei Paskevich committed
531 532 533
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
534
##
Andrei Paskevich's avatar
Andrei Paskevich committed
535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550
## 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
551
##
Andrei Paskevich's avatar
Andrei Paskevich committed
552 553 554 555 556 557 558 559
## 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 ======"
560
##
Andrei Paskevich's avatar
Andrei Paskevich committed
561 562 563 564 565
## 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
566 567
##
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
568 569 570 571 572 573
## 	cp $(BINARY) $$HOME/bin/why
## 	cp $(WHYCONFIG) $$HOME/bin/why
## 	cp $(JESSIE) $$HOME/bin/jessie
## 	if test -f bin/why-ide.$(OCAMLBEST); then \
## 	  cp -f bin/why-ide.$(OCAMLBEST) $$HOME/bin/why-ide; \
## 	fi
574
##
Andrei Paskevich's avatar
Andrei Paskevich committed
575
## local: install
576
##
Andrei Paskevich's avatar
Andrei Paskevich committed
577 578
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
579
##
Andrei Paskevich's avatar
Andrei Paskevich committed
580 581
## 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
582

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
583 584 585
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
586

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
591
doc/manual.pdf: doc/manual.tex doc/version.tex
592
	$(MAKE) -C doc manual.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
593 594

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
597
clean::
598
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
599

600
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
601
# API DOC
602
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
603

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
604 605
.PHONY: apidoc

606
apidoc:
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
607
	mkdir -p apidoc
608 609
	$(OCAMLDOC) -d apidoc -html -I src $(LIBINCLUDES) -I +sqlite3 \
	    $(LIBML) $(LIBMLI) $(MNGML) $(MNGMLI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
610

611 612
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
613

614
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
615
# generic rules
616
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
617

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

621
%.cmo %cmi: %.ml
622
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
623

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

627
%.cmxs: %.ml
628
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
629

Andrei Paskevich's avatar
Andrei Paskevich committed
630
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
631 632
	$(OCAMLLEX) $<

Andrei Paskevich's avatar
Andrei Paskevich committed
633
%.ml %.mli %.output: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
634 635
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
645 646 647 648 649 650 651 652
# 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
653 654 655 656 657 658 659 660 661 662 663

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
664
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
665 666 667 668
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
669
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
670 671 672 673 674 675 676
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
	otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml

wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
677
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
678

679
dep: depend
680
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
681
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
683 684 685
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
686 687
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
688
#
Andrei Paskevich's avatar
Andrei Paskevich committed
689 690 691
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
692
#
Andrei Paskevich's avatar
Andrei Paskevich committed
693
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
694 695 696 697 698
#       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
699 700 701 702 703 704 705
# 	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 \
706
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724
# 	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* \
725 726 727
#	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
728
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
729
#
Andrei Paskevich's avatar
Andrei Paskevich committed
730
# distrib export: source export-doc export-www export-examples export-examples-c linux
731
#
Andrei Paskevich's avatar
Andrei Paskevich committed
732 733 734
# 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
735
# 	$(MAKE) -C /users/demons/filliatr/www/why install
736
#
Andrei Paskevich's avatar
Andrei Paskevich committed
737 738
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
739
#
Andrei Paskevich's avatar
Andrei Paskevich committed
740 741 742 743 744 745
# 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
746 747
#
# tarball-for-framac:
748
# 	$(MAKE) tarball
Andrei Paskevich's avatar
Andrei Paskevich committed
749
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
750 751
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
752 753
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
754
# 	$(MAKE) export/$(NAME).tar.gz
755
#
Andrei Paskevich's avatar
Andrei Paskevich committed
756
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
757
#
Andrei Paskevich's avatar
Andrei Paskevich committed
758 759
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
760
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
761
# 	echo "*** faire make all dans $(WWW)/examples ***"
762
#
Andrei Paskevich's avatar
Andrei Paskevich committed
763 764 765 766 767 768
# 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
769
#
Andrei Paskevich's avatar
Andrei Paskevich committed
770 771 772 773 774 775 776 777
# 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)
778
#
Andrei Paskevich's avatar
Andrei Paskevich committed
779
# OSTYPE  ?= linux
780
#
Andrei Paskevich's avatar
Andrei Paskevich committed
781
# BINARYNAME = $(NAME)-$(OSTYPE)
782
#
Andrei Paskevich's avatar
Andrei Paskevich committed
783
# linux: binary
784 785 786
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
787 788 789 790 791
# 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
792

793
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
794
# file headers
795 796
###############

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

801
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
802
# myself
803
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
804

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
805
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
806 807 808 809
	./config.status --file $@

src/config.ml: src/config.ml.in config.status
	./config.status --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
810

Andrei Paskevich's avatar
Andrei Paskevich committed
811 812 813 814
doc/version.tex: doc/version.tex.in config.status
	./config.status --file $@

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
815 816 817
	./config.status --recheck

configure: configure.in
818
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
819

820
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
821
# clean and depend
822
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
823

824
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
825

826
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
827 828
	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
829

830 831 832 833
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
834 835 836 837 838 839 840
#################################################################
# 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:
841
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
842 843 844 845 846 847 848 849
# 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.