Makefile.in 26.8 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 -I +sqlite3
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
	driver/whyconf driver/driver \
715
716
	transform/introduction \
	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
717
718
719

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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