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.