Makefile.in 25.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 39 40
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 67 68 69
ifeq (@ENABLE_PROFILING@,yes)
OFLAGS += -g -p
STRIP = true
endif

70 71
# external libraries common to all binaries

Andrei Paskevich's avatar
Andrei Paskevich committed
72
ifeq (@enable_plugins@,yes)
73
  DYNLINK = dynlink
74
else
75
  DYNLINK =
76 77
endif

78

79 80 81
EXTLIBS = str unix nums $(DYNLINK)
EXTCMA	= $(addsuffix .cma,$(EXTLIBS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83 84 85
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86

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

89
.PHONY: byte opt clean depend all install
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91
#############
92
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94

95
LIBGENERATED = src/util/rc.ml \
96 97 98 99
	       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
100

101
LIB_UTIL = exn_printer pp loc print_tree hashweak hashcons util sysutil rc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102

103
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
104

105
LIB_PARSER = ptree parser lexer denv typing
106

107
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
108
	     whyconf
109

110 111
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
		inlining split_conjunction split_goal \
112
		eliminate_definition eliminate_algebraic \
113
		eliminate_inductive eliminate_let eliminate_if \
114
		encoding_enumeration encoding encoding_decorate_mono \
115
		libencoding encoding_decorate encoding_bridge \
116
		encoding_explicit encoding_simple2 \
117
		encoding_instantiate simplify_array filter_trigger
118

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
119
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
120

121 122 123 124 125 126
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)) \
127
	      $(addprefix src/printer/, $(LIB_PRINTER))
128

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

132 133
ifeq (@enable_hypothesis_selection@,yes)
	LIB_TRANSFORM += hypothesis_selection
134
	INCLUDES += -I +ocamlgraph
MARCHE Claude's avatar
MARCHE Claude committed
135
	LIBINCLUDES += -I +ocamlgraph
136 137 138 139
	EXTLIBS += ocamlgraph/graph
endif


140 141 142 143
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
144

145
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
146
$(LIBCMX): OFLAGS += -for-pack Why
147

148
# build targets
149

150 151
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152

153
src/why.cma: src/why.cmo
154 155
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

156
src/why.cmxa: src/why.cmx
157 158
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

159 160
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
161

162 163 164 165
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
166

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
167 168
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
169
.depend.lib: src/config.ml $(LIBGENERATED)
170
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171 172 173

depend: .depend.lib

174 175
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
176
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
177 178 179 180 181 182 183 184
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
185
	rm -f .depend.lib
186

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
187
##################
188
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190 191 192 193
##################

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

194
bin/why.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
195 196
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
197 198
	$(STRIP) $@

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

203 204
src/main.cmo: src/why.cmo
src/main.cmx: src/why.cmx
205

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
206
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
207
	rm -f src/main.cm[iox] src/main.annot src/main.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
208
	rm -f bin/why.byte bin/why.opt
209

210 211 212 213
install::
	mkdir -p $(BINDIR)
	cp -f bin/why.@OCAMLBEST@ $(BINDIR)/why3

214 215 216
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
217

218
PGMGENERATED = src/programs/pgm_parser.mli    src/programs/pgm_parser.ml \
219
	       src/programs/pgm_parser.output src/programs/pgm_lexer.ml
Francois Bobot's avatar
Francois Bobot committed
220

221
PGM_FILES = pgm_ttree pgm_ptree  pgm_parser pgm_lexer pgm_effect \
222
	    pgm_env   pgm_typing pgm_wp pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223

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

226 227 228 229 230 231 232 233
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
234

235 236
byte: bin/whyml.byte
opt:  bin/whyml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
237

238
bin/whyml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
239 240
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241 242
	$(STRIP) $@

243
bin/whyml.byte: src/why.cma $(PGMCMO) src/main.cmo
244 245 246 247
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248 249

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
254 255 256
depend: .depend.programs

clean::
257 258 259
	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
260
	rm -f bin/whyml.byte bin/whyml.opt
261
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
262

263 264 265
# test target

%: %.mlw bin/whyml.byte
266
	bin/whyml.byte -P alt-ergo $*.mlw
267

268 269 270 271
install::
	mkdir -p $(BINDIR)
	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/whyml3

MARCHE Claude's avatar
MARCHE Claude committed
272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329
###############
# IDE
###############

IDE_FILES = scheduler 
IDE_MAIN_FILE = gmain

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

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

IDEMAINML  = $(addsuffix .ml,  $(IDEMAIN))

$(IDECMO) $(IDECMX) $(addsuffix .cmx, $(IDEMAIN)) $(addsuffix .cmo, $(IDEMAIN)): INCLUDES = -thread -I src/ide -I +threads
# -I +sqlite3 

src/ide/gmain.cmo src/ide/gmain.cmx: INCLUDES += -I +lablgtk2

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

bin/gwhy.opt bin/gwhy.byte: INCLUDES = -thread -I +lablgtk2
# -I +sqlite3 

bin/gwhy.opt: src/why.cmxa $(PGMCMX) $(IDECMX) src/ide/gmain.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
	lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
	$(STRIP) $@
# sqlite3.cmxa 

bin/gwhy.byte: src/why.cma $(PGMCMO) $(IDECMO) src/ide/gmain.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
	lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
# sqlite3.cma 

# depend and clean targets

include .depend.ide

.depend.ide:
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) $(IDEMAINML) > $@

depend: .depend.ide

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330
###############
MARCHE Claude's avatar
MARCHE Claude committed
331
# rust prover
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332 333
###############

334
MNG_FILES = db scheduler
MARCHE Claude's avatar
MARCHE Claude committed
335
MNG_MAIN_FILES = test gmanager
336 337

MNGMODULES = $(addprefix src/manager/, $(MNG_FILES))
MARCHE Claude's avatar
MARCHE Claude committed
338
MNGMAINS = $(addprefix src/manager/, $(MNG_MAIN_FILES))
339 340 341 342 343 344

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

345 346
MNGMAINML  = $(addsuffix .ml,  $(MNGMAINS))

MARCHE Claude's avatar
MARCHE Claude committed
347
$(MNGCMO) $(MNGCMX) $(addsuffix .cmx, $(MNGMAINS)) $(addsuffix .cmo, $(MNGMAINS)): INCLUDES = -thread -I src/manager -I +sqlite3 -I +threads
348

MARCHE Claude's avatar
MARCHE Claude committed
349 350 351
src/manager/gmanager.cmo src/manager/gmanager.cmx: INCLUDES += -I +lablgtk2

ifeq (@enable_rust_prover@,yes)
MARCHE Claude's avatar
MARCHE Claude committed
352 353
byte: bin/manager-test.byte bin/why-ide.byte
opt:  bin/manager-test.opt bin/why-ide.opt
354
endif
355

MARCHE Claude's avatar
MARCHE Claude committed
356
bin/manager-test.opt bin/manager-test.byte: INCLUDES = -thread -I +sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
357

MARCHE Claude's avatar
MARCHE Claude committed
358
bin/manager-test.opt: src/why.cmxa $(MNGCMX) src/manager/test.cmx
359
	$(if $(QUIET), @echo 'Linking  $@' &&) \
MARCHE Claude's avatar
MARCHE Claude committed
360
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa sqlite3.cmxa $^
361
	$(STRIP) $@
MARCHE Claude's avatar
MARCHE Claude committed
362

MARCHE Claude's avatar
MARCHE Claude committed
363
bin/manager-test.byte: src/why.cma $(MNGCMO) src/manager/test.cmo
364
	$(if $(QUIET),@echo 'Linking  $@' &&) \
MARCHE Claude's avatar
MARCHE Claude committed
365
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma sqlite3.cma $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
366

MARCHE Claude's avatar
MARCHE Claude committed
367
bin/why-ide.opt bin/why-ide.byte: INCLUDES = -thread -I +sqlite3 -I +lablgtk2
MARCHE Claude's avatar
MARCHE Claude committed
368

MARCHE Claude's avatar
MARCHE Claude committed
369
bin/why-ide.opt: src/why.cmxa $(PGMCMX) $(MNGCMX) src/manager/gmanager.cmx
MARCHE Claude's avatar
MARCHE Claude committed
370 371 372 373 374
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
	lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx sqlite3.cmxa $^
	$(STRIP) $@

MARCHE Claude's avatar
MARCHE Claude committed
375
bin/why-ide.byte: src/why.cma $(PGMCMO) $(MNGCMO) src/manager/gmanager.cmo
MARCHE Claude's avatar
MARCHE Claude committed
376 377 378 379
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
	lablgtk.cma lablgtksourceview2.cma gtkThread.cmo sqlite3.cma $^

380
# depend and clean targets
MARCHE Claude's avatar
MARCHE Claude committed
381 382 383

include .depend.manager

384
.depend.manager:
385
	$(OCAMLDEP) -slash -I src -I src/manager $(MNGML) $(MNGMLI) $(MNGMAINML) > $@
MARCHE Claude's avatar
MARCHE Claude committed
386

387
depend: .depend.manager
MARCHE Claude's avatar
MARCHE Claude committed
388 389

clean::
390 391
	rm -f src/manager/*.cm[iox] src/manager/*.o
	rm -f src/manager/*.annot src/manager/*~
MARCHE Claude's avatar
MARCHE Claude committed
392
	rm -f bin/manager.byte bin/manager.opt
393
	rm -f .depend.manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
394

MARCHE Claude's avatar
MARCHE Claude committed
395

396 397 398 399
##############
# Coq plugin
##############

400 401 402 403 404 405 406 407 408 409 410 411 412 413 414
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
415
ifeq (@enable_coq_support@,yes)
416 417
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
418
endif
419

420 421
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
422

423
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
424 425
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

426
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
427 428
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

429 430 431 432
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
433

434
ifeq (@enable_coq_support@,yes)
435 436 437 438 439 440
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
441
endif
442 443 444 445 446 447 448 449

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

450 451 452 453
########
# Tptp2why
########

454
MENHIR=@MENHIR@
455

456 457
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
458

459
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
460 461 462 463 464 465 466 467 468
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))

469
$(TPTPCMO) $(TPTPCMX): INCLUDES = -I $(TPTP_DIR) -I src/core/
470 471 472

# build targets

473
ifeq (@enable_tptp2why_support@,yes)
474 475
byte: bin/tptp2why.byte
opt:  bin/tptp2why.opt
476
endif
477

478
src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli: OCAMLYACC = $(MENHIR)
479

480
bin/tptp2why.opt: src/why.cmxa $(TPTPCMX) src/main.cmx
481
	$(if $(QUIET), @echo 'Linking  $@' &&) \
482
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
483 484
	$(STRIP) $@

485
bin/tptp2why.byte: src/why.cma $(TPTPCMO) src/main.cmo
486
	$(if $(QUIET),@echo 'Linking  $@' &&) \
487
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
488 489 490

# depend and clean targets

491
ifeq (@enable_tptp2why_support@,yes)
492 493 494 495 496 497
include .depend.tptp2why

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

depend: .depend.tptp2why
Andrei Paskevich's avatar
Andrei Paskevich committed
498
endif
499 500 501 502 503 504 505 506

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

507 508 509 510
#######
# tools
#######

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
511
TOOLS = bin/why3-cpulimit
512 513 514

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
515
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
516
	$(CC) -Wall -o $@ $^
517 518

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

521 522 523 524
install::
	mkdir -p $(BINDIR)
	cp -f bin/why3-cpulimit $(BINDIR)

525 526 527 528 529 530
########
# bench
########

.PHONY: bench test

531
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
532
	sh bench/bench \
533
	    "bin/why.@OCAMLBEST@" \
534
	    "bin/whyml.@OCAMLBEST@"
535

536
BENCH_PLUGINS_CMO := helloworld.cmo
537 538 539 540
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)
541
	bin/why.byte -D bench/plugins/helloworld.drv \
542
	tests/test-jcf.why -T Test -G G
543
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
544
	tests/test-jcf.why -T Test -G G
545 546

###############
547
# test targets
548
###############
549

550 551 552
test2: bin/why.byte $(TOOLS)
	bin/why.byte tests/test-jcf.why

553
test: bin/why.byte $(TOOLS)
554
	mkdir -p output_why3
555
	bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
556 557 558
	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
559
	echo bin/why.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
560
	@printf "*** Checking Coq file generation ***\\n"
561
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
562
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
563 564
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
565
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
566
		; do \
567
	  printf "Generating Coq file for $$i\\n" && \
568
	  	bin/why.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
569
	@printf "*** Checking Coq compilation ***\\n"
570
	@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
571

572
testl: bin/whyml.byte
573
	ocamlrun -bt bin/whyml.byte --debug tests/test-pgm-jcf.mlw
574
	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
575 576

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

579
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
580
# installation
581
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
582

583 584 585 586 587 588
install::
	mkdir -p $(LIBDIR)/why3
	cp -f --parents theories/*.why theories/*/*.why $(LIBDIR)/why3/
	cp -f --parents drivers/*.drv $(LIBDIR)/why3/
	cp -f why.conf $(LIBDIR)/why3/

589 590 591 592
## install: install-binary install-lib install-man
##
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST)
##
Andrei Paskevich's avatar
Andrei Paskevich committed
593 594
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
595
## install-binary:
Andrei Paskevich's avatar
Andrei Paskevich committed
596 597 598 599 600
## 	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
601 602
##
## install-lib:
Andrei Paskevich's avatar
Andrei Paskevich committed
603
## 	mkdir -p $(LIBDIR)/why/why
604
##
Andrei Paskevich's avatar
Andrei Paskevich committed
605 606 607
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
608
##
Andrei Paskevich's avatar
Andrei Paskevich committed
609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624
## 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
625
##
Andrei Paskevich's avatar
Andrei Paskevich committed
626 627 628 629 630 631 632 633
## 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 ======"
634
##
Andrei Paskevich's avatar
Andrei Paskevich committed
635 636 637 638 639
## 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
640 641
##
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte
Andrei Paskevich's avatar
Andrei Paskevich committed
642 643 644 645 646 647
## 	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
648
##
Andrei Paskevich's avatar
Andrei Paskevich committed
649
## local: install
650
##
Andrei Paskevich's avatar
Andrei Paskevich committed
651 652
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
653
##
Andrei Paskevich's avatar
Andrei Paskevich committed
654 655
## 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
656

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
657 658 659
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
660

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
665
doc/manual.pdf: doc/manual.tex doc/version.tex
666
	$(MAKE) -C doc manual.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
667 668

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
671
clean::
672
	$(MAKE) -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
673

674
##########
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
675
# API DOC
676
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
677

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
678 679
.PHONY: apidoc

680
apidoc:
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
681
	mkdir -p apidoc
Simon Cruanes's avatar
Simon Cruanes committed
682
	$(OCAMLDOC) -d apidoc -html -keep-code -I src $(LIBINCLUDES) -I +sqlite3 \
683
	    $(LIBML) $(LIBMLI) $(MNGML) $(MNGMLI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
684

685 686
clean::
	rm -f apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
687

688
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
689
# generic rules
690
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
691

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

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

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

701
%.cmxs: %.ml
702
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
703

Andrei Paskevich's avatar
Andrei Paskevich committed
704
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
705 706
	$(OCAMLLEX) $<

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
719 720 721 722 723 724 725 726
# 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
727 728 729 730 731 732 733 734 735 736 737

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
738
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
739 740 741 742
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
743
	      "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
744 745 746 747
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

otags:
748 749
	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
750

751 752 753 754 755
# 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
756
wc:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
757
	ocamlwc -p src/*.ml* src/*/*.ml*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
758

759
dep: depend
760
	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
761
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
762

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
763 764 765
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
766 767
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
768
#
Andrei Paskevich's avatar
Andrei Paskevich committed
769 770 771
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
772
#
Andrei Paskevich's avatar
Andrei Paskevich committed
773
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
774 775 776 777 778
#       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
779 780 781 782 783 784 785
# 	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 \
786
#	bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
Andrei Paskevich's avatar
Andrei Paskevich committed
787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804
# 	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* \
805 806 807
#	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
808
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
809
#
Andrei Paskevich's avatar
Andrei Paskevich committed
810
# distrib export: source export-doc export-www export-examples export-examples-c linux
811
#
Andrei Paskevich's avatar
Andrei Paskevich committed
812 813 814
# 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
815
# 	$(MAKE) -C /users/demons/filliatr/www/why install
816
#
Andrei Paskevich's avatar
Andrei Paskevich committed
817 818
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
819
#
Andrei Paskevich's avatar
Andrei Paskevich committed
820 821 822 823 824 825
# 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
826 827
#
# tarball-for-framac:
828
# 	$(MAKE) tarball
Andrei Paskevich's avatar
Andrei Paskevich committed
829
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
830 831
#
# tarball:
Andrei Paskevich's avatar
Andrei Paskevich committed
832 833
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
834
# 	$(MAKE) export/$(NAME).tar.gz
835
#
Andrei Paskevich's avatar
Andrei Paskevich committed
836
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
837
#
Andrei Paskevich's avatar
Andrei Paskevich committed
838 839
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
840
# 	$(MAKE) -C $(WWW)/examples clean depend
Andrei Paskevich's avatar
Andrei Paskevich committed
841
# 	echo "*** faire make all dans $(WWW)/examples ***"
842
#
Andrei Paskevich's avatar
Andrei Paskevich committed
843 844 845 846 847 848
# 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
849
#
Andrei Paskevich's avatar
Andrei Paskevich committed
850 851 852 853 854 855 856 857
# 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)
858
#
Andrei Paskevich's avatar
Andrei Paskevich committed
859
# OSTYPE  ?= linux
860
#
Andrei Paskevich's avatar
Andrei Paskevich committed
861
# BINARYNAME = $(NAME)-$(OSTYPE)
862
#
Andrei Paskevich's avatar
Andrei Paskevich committed
863
# linux: binary
864 865 866
#
# ALLBINARYFILES = $(FILES) $(BINARYFILES)
#
Andrei Paskevich's avatar
Andrei Paskevich committed
867 868 869 870 871
# 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
872

873
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
874
# file headers
875 876
###############

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

881
#########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
882
# myself
883
#########
Andrei Paskevich's avatar
Andrei Paskevich committed
884

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
885
Makefile: Makefile.in config.status
886
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
887

888
src/config.sh: src/config.sh.in config.status
889
	./config.status chmod --file $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
890

891
src/config.ml: src/config.sh
892 893
	LIBDIR=$(LIBDIR) src/config.sh

Andrei Paskevich's avatar
Andrei Paskevich committed
894
doc/version.tex: doc/version.tex.in config.status
895
	./config.status chmod --file $@
Andrei Paskevich's avatar
Andrei Paskevich committed
896 897

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
898 899 900
	./config.status --recheck

configure: configure.in
901
	autoconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
902

903
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
904
# clean and depend
905
###################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
906

907
.PHONY: distclean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
908

909
distclean: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
910 911
	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
912

913 914 915 916
depend:
	rm -f $^
	$(MAKE) $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
917 918 919 920 921 922 923
#################################################################
# 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:
924
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
925 926 927 928 929 930 931 932
# 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.