Makefile.in 28.1 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
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
126
		inlining 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 close_epsilon lift_epsilon
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
d    
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))

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

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

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

MARCHE Claude's avatar
d    
MARCHE Claude committed
399
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 
400
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
MARCHE Claude's avatar
d    
MARCHE Claude committed
401
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
402

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

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

# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

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

MARCHE Claude's avatar
d    
MARCHE Claude committed
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483

###############
# IDE WITH DB
###############

DB_FILES = gconfig scheduler db gdbmain

DBMODULES = $(addprefix src/ide/, $(DB_FILES))

DBML  = $(addsuffix .ml,  $(DBMODULES))
DBMLI = $(addsuffix .mli, $(DBMODULES))
DBCMO = $(addsuffix .cmo, $(DBMODULES))
DBCMX = $(addsuffix .cmx, $(DBMODULES))

$(DBCMO) $(DBCMX): INCLUDES += -I src/ide -I +sqlite3

# build targets

ifeq (@enable_ide@,yes)
byte: bin/whydb.byte 
opt:  bin/whydb.opt 
endif

bin/whydb.opt bin/whydb.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
bin/whydb.opt bin/whydb.byte: EXTOBJS += gtkThread
bin/whydb.opt bin/whydb.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3

bin/whydb.opt: src/why.cmxa $(PGMCMX) $(DBCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/whydb.byte: src/why.cma $(PGMCMO) $(DBCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets

include .depend.db

.depend.db:
	$(OCAMLDEP) -slash -I src -I src/ide $(DBML) $(DBMLI) > $@

depend: .depend.db

clean::
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
	rm -f bin/whydb.byte bin/whydb.opt
	rm -f .depend.db

install_no_local::
	cp -f bin/whydb.@OCAMLBEST@ $(BINDIR)/why3db

484
485
486
487
##############
# Coq plugin
##############

488
489
490
491
492
493
494
495
496
497
498
499
500
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))

501
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
502

Andrei Paskevich's avatar
Andrei Paskevich committed
503
ifeq (@enable_coq_support@,yes)
504
505
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
506
endif
507

508
509
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
510

511
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
512
513
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

514
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
515
516
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

517
518
519
520
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
521

522
ifeq (@enable_coq_support@,yes)
523
524
525
526
527
528
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
529
endif
530
531
532
533
534
535
536
537

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

538
539
540
541
########
# Tptp2why
########

542
543
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
544

545
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
546

547
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
548
549
550
551
552
553

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

554
555
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
556
557
558

# build targets

559
ifeq (@enable_whytptp@,yes)
560
561
byte: bin/whytptp.byte
opt:  bin/whytptp.opt
562
563
564
565
endif

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

567
bin/whytptp.opt: src/why.cmxa $(TPTPCMX) src/main.cmx
568
	$(if $(QUIET), @echo 'Linking  $@' &&) \
569
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
570
571
	$(STRIP) $@

572
bin/whytptp.byte: src/why.cma $(TPTPCMO) src/main.cmo
573
	$(if $(QUIET),@echo 'Linking  $@' &&) \
574
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
575
576
577

# depend and clean targets

578
ifeq (@enable_whytptp@,yes)
579
580
581
582
583
584
include .depend.tptp2why

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

depend: .depend.tptp2why
585
endif
586
587
588
589
590

clean::
	rm -f $(TPTPGENERATED)
	rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
	rm -f src/tptp2why/*.annot src/tptp2why/*~
591
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
592
	rm -f bin/whytptp.byte bin/whytptp.opt
593
594
	rm -f .depend.tptp2why

595
596
597
598
#######
# tools
#######

MARCHE Claude's avatar
gappa    
MARCHE Claude committed
599
TOOLS = bin/why3-cpulimit
600
601
602

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa    
MARCHE Claude committed
603
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
604
	$(CC) -Wall -o $@ $^
605
606

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

609
install_no_local::
610
611
	cp -f bin/why3-cpulimit $(BINDIR)

612
613
614
615
616
617
########
# bench
########

.PHONY: bench test

MARCHE Claude's avatar
MARCHE Claude committed
618
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
619
	sh bench/bench \
620
	    "bin/why.@OCAMLBEST@" \
621
	    "bin/whyml.@OCAMLBEST@"
622

623
BENCH_PLUGINS_CMO := helloworld.cmo
624
625
626
627
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)
628
	bin/why.byte -D bench/plugins/helloworld.drv \
629
	tests/test-jcf.why -T Test -G G
630
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
631
	tests/test-jcf.why -T Test -G G
632
633

###############
634
# test targets
635
###############
636

637
638
639
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

640
test: bin/why.byte $(TOOLS)
641
	mkdir -p output_why3
642
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
643
644
645
	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
646
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
647
	@printf "*** Checking Coq file generation ***\\n"
648
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
649
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
650
651
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
652
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
653
		; do \
654
	  printf "Generating Coq file for $$i\\n" && \
655
	  	bin/why.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
656
	@printf "*** Checking Coq compilation ***\\n"
657
	@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
658

659
testl: bin/whyml.byte
660
	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
661
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
662

663
664
665
testl-ide: bin/whyide.opt
	bin/whyide.opt tests/test-pgm-jcf.mlw

666
testl-type: bin/whyml.byte
667
	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
668

MARCHE Claude's avatar
MARCHE Claude committed
669
test-api: src/why.cma
670
	ocaml unix.cma str.cma nums.cma dynlink.cma \
MARCHE Claude's avatar
MARCHE Claude committed
671
672
		src/why.cma -I src examples/use_api.ml \
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
673

674
675
## install: install-binary install-lib install-man
##
676
## BINARYFILES = $(BINARY) bin/whyide.$(OCAMLBEST)
677
##
Andrei Paskevich's avatar
Andrei Paskevich committed
678
## # install-binary should not depend on $(BINARYFILES); otherwise it
679
## # enforces the compilation of whyide, even when lablgtk2 is not installed
680
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
681
682
## 	mkdir -p $(BINDIR)
## 	cp -f $(BINARY) $(BINDIR)/why$(EXE)
683
684
## 	if test -f bin/whyide.$(OCAMLBEST); then \
## 		cp -f bin/whyide.$(OCAMLBEST) $(BINDIR)/whyide-bin$(EXE); \
Andrei Paskevich's avatar
Andrei Paskevich committed
685
## 	fi
686
687
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
688
## 	mkdir -p $(LIBDIR)/why/why
689
##
Andrei Paskevich's avatar
Andrei Paskevich committed
690
691
692
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
693
##
Andrei Paskevich's avatar
Andrei Paskevich committed
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
## 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
710
##
Andrei Paskevich's avatar
Andrei Paskevich committed
711
712
713
714
715
716
717
718
## 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 ======"
719
##
Andrei Paskevich's avatar
Andrei Paskevich committed
720
721
722
723
724
## 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
725
##
726
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/whyide.$(OCAMLBEST) byte bin/whyide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
727
728
729
## 	cp $(BINARY) $$HOME/bin/why
## 	cp $(WHYCONFIG) $$HOME/bin/why
## 	cp $(JESSIE) $$HOME/bin/jessie
730
731
## 	if test -f bin/whyide.$(OCAMLBEST); then \
## 	  cp -f bin/whyide.$(OCAMLBEST) $$HOME/bin/whyide; \
Andrei Paskevich's avatar
Andrei Paskevich committed
732
## 	fi
733
##
Andrei Paskevich's avatar
Andrei Paskevich committed
734
## local: install
735
##
Andrei Paskevich's avatar
Andrei Paskevich committed
736
737
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
738
##
Andrei Paskevich's avatar
Andrei Paskevich committed
739
740
## 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
741

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
742
743
744
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
745

MARCHE Claude's avatar
MARCHE Claude committed
746
747
DOC = doc/manual.pdf
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
748

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

MARCHE Claude's avatar
MARCHE Claude committed
751
752
753
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
754
755

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
758
clean::
759
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
760

761
##########
MARCHE Claude's avatar
API doc    
MARCHE Claude committed
762
# API DOC
763
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
764

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
765
766
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
767
768
MODULESTODOC = core/ident core/ty core/term core/decl core/theory \
	core/env core/task \
769
	driver/whyconf driver/driver \
770
771
	transform/introduction \
	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
772
773
774

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

775
apidoc: $(FILESTODOC)
MARCHE Claude's avatar
API doc    
MARCHE Claude committed
776
	mkdir -p apidoc
MARCHE Claude's avatar
MARCHE Claude committed
777
778
779
780
	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 

MARCHE Claude's avatar
MARCHE Claude committed
781
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
782
783
784
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
		$(LIBINCLUDES) $(FILESTODOC)
# $(LIBML) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
785

786
787
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
788

789
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
790
# generic rules
791
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
792

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

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

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

802
%.cmxs: %.ml
803
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
804

Andrei Paskevich's avatar
Andrei Paskevich committed
805
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
806
807
	$(OCAMLLEX) $<

808
%.ml %.mli: %.mly
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
809
810
	$(OCAMLYACC) -v $<

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
820
821
822
823
824
825
826
827
# 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
828
829
830
831
832
833
834
835
836
837
838

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

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

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

tags:
Francois Bobot's avatar
   
Francois Bobot committed
839
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
840
841
842
843
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
844
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
845
846
847
848
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
849
850
	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
851

852
853
854
855
856
# 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
857
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
858
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
859

860
dep: depend
861
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
862
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
863

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
864
865
866
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
867
868
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
869
#
Andrei Paskevich's avatar
Andrei Paskevich committed
870
871
872
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
873
#
874
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/whyide.sh \
875
876
877
878
879
#       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
880
881
882
883
884
885
886
# 	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 \
887
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
# 	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* \
906
907
908
#	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
909
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
910
#
Andrei Paskevich's avatar
Andrei Paskevich committed
911
# distrib export: source export-doc export-www export-examples export-examples-c linux
912
#
Andrei Paskevich's avatar
Andrei Paskevich committed
913
914
915
# 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
916
# 	$(MAKE) -C /users/demons/filliatr/www/why install
917
#
Andrei Paskevich's avatar
Andrei Paskevich committed
918
919
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
920
#
Andrei Paskevich's avatar
Andrei Paskevich committed
921
922
923
924
925
926
# 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
927
928
#
# tarball-for-framac:
929
# 	$(MAKE) tarball
Andrei Paskevich's avatar
Andrei Paskevich committed
930
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
931
932
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
933
934
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
935
# 	$(MAKE) export/$(NAME).tar.gz
936
#
Andrei Paskevich's avatar
Andrei Paskevich committed
937
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
938
#
Andrei Paskevich's avatar
Andrei Paskevich committed
939
940
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
941
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
942
# 	echo "*** faire make all dans $(WWW)/examples ***"
943
#
Andrei Paskevich's avatar
Andrei Paskevich committed
944
945
946
947
948
949
# 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
950
#
Andrei Paskevich's avatar
Andrei Paskevich committed
951
952
953
954
955
956
957
958
# 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)
959
#
Andrei Paskevich's avatar
Andrei Paskevich committed
960
# OSTYPE  ?= linux
961
#
Andrei Paskevich's avatar
Andrei Paskevich committed
962
# BINARYNAME = $(NAME)-$(OSTYPE)
963
#
Andrei Paskevich's avatar
Andrei Paskevich committed
964
# linux: binary
965
966
967
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
968
969
970
971
972
# 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
973

974
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
975
# file headers
976
977
###############

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

982
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
983
# myself
984
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
985

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
986
Makefile: Makefile.in config.status
987
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
988

989
src/config.sh: src/config.sh.in config.status
990
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
991

992
src/config.ml: src/config.sh
993
	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
994

Andrei Paskevich's avatar
Andrei Paskevich committed
995
doc/version.tex: doc/version.tex.in config.status
996
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
997
998

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
999
1000
	./config.status --recheck

For faster browsing, not all history is shown. View entire blame