Makefile.in 20.5 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

Andrei Paskevich's avatar
Andrei Paskevich committed
22
ifeq (@enable_verbose_make@,yes)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23 24 25 26 27 28 29 30 31
 QUIET = 
else    
 QUIET = yes
endif

# where to install the binaries
DESTDIR =
prefix=@prefix@
exec_prefix=@exec_prefix@
Andrei Paskevich's avatar
Andrei Paskevich committed
32
datarootdir=@datarootdir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33 34
BINDIR=$(DESTDIR)@bindir@
LIBDIR=$(DESTDIR)@libdir@
Andrei Paskevich's avatar
Andrei Paskevich committed
35 36
DATADIR=$(DESTDIR)@datadir@
MANDIR=$(DESTDIR)@mandir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
37

Andrei Paskevich's avatar
Andrei Paskevich committed
38
# OS specific stuff
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39 40 41 42 43 44 45 46 47 48 49 50 51
EXE=@EXE@
STRIP=@STRIP@

# other variables
OCAMLC   = @OCAMLC@ 
OCAMLOPT = @OCAMLOPT@ 
OCAMLDEP = @OCAMLDEP@
OCAMLLEX = @OCAMLLEX@
OCAMLYACC= @OCAMLYACC@
OCAMLDOC = @OCAMLDOC@
OCAMLLIB = @OCAMLLIB@
OCAMLBEST= @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
Andrei Paskevich's avatar
Andrei Paskevich committed
52 53 54
#CAMLP4   = @CAMLP4O@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
55

Andrei Paskevich's avatar
Andrei Paskevich committed
56
ifeq (@enable_plugins@,yes)
57 58
DYNLINKCMA  = dynlink.cma
DYNLINKCMXA = dynlink.cmxa
59
else
Andrei Paskevich's avatar
Andrei Paskevich committed
60
DYNLINKCMA  = 
61
DYNLINKCMXA = 
62 63
endif

Andrei Paskevich's avatar
Andrei Paskevich committed
64 65
BFLAGS = -w Aelz -dtypes -g $(INCLUDES)
OFLAGS = -w Aelz -dtypes    $(INCLUDES)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
67
# external libraries common to all binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69 70
EXTCMA = str.cma unix.cma nums.cma $(DYNLINKCMA)
EXTCMXA = $(EXTCMA:.cma=.cmxa)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
71

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
72 73 74
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80 81 82
#############
# Why library 
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83

MARCHE Claude's avatar
MARCHE Claude committed
84
LIBGENERATED = src/config.ml src/userconf/rc.ml \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85 86 87
          src/parser/parser.mli src/parser/parser.ml src/parser/parser.output \
            src/parser/lexer.ml src/driver/driver_lexer.ml \
            src/driver/driver_parser.mli src/driver/driver_parser.ml \
Andrei Paskevich's avatar
Andrei Paskevich committed
88
	    src/driver/driver_parser.output
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90
depend: $(LIBGENERATED)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91

MARCHE Claude's avatar
MARCHE Claude committed
92
LIBDIRS=core util parser transform driver printer userconf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93 94 95 96
LIBCLEAN=$(addprefix src/, $(LIBDIRS))
LIBCLEAN:=$(addsuffix /*.cm[iox], $(LIBCLEAN)) \
          $(addsuffix /*.annot, $(LIBCLEAN)) \
          $(addsuffix /*.o, $(LIBCLEAN)) 
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
clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED) 
	rm -f why.cm[iox] why.a why.o $(LIBCMA) $(LIBCMXA)
101

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102
CORE_CMO := ident.cmo ty.cmo term.cmo pattern.cmo decl.cmo theory.cmo\
Francois Bobot's avatar
Francois Bobot committed
103
	task.cmo pretty.cmo trans.cmo env.cmo register.cmo
104
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
105

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106
UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
MARCHE Claude's avatar
MARCHE Claude committed
107
            sysutil.cmo hashweak.cmo 
108 109
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))

110
PARSER_CMO := ptree.cmo parser.cmo lexer.cmo denv.cmo typing.cmo 
111 112
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))

Francois Bobot's avatar
 
Francois Bobot committed
113
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
114
	split_conjunction.cmo encoding_decorate.cmo\
115
	remove_logic_definition.cmo eliminate_inductive.cmo\
116
	compile_match.cmo eliminate_algebraic.cmo\
117
	eliminate_let.cmo eliminate_definition.cmo
118 119
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))

Andrei Paskevich's avatar
Andrei Paskevich committed
120
DRIVER_CMO := driver_ast.cmo call_provers.cmo \
MARCHE Claude's avatar
MARCHE Claude committed
121
              driver_parser.cmo driver_lexer.cmo driver.cmo  
122
DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
123

MARCHE Claude's avatar
MARCHE Claude committed
124
PRINTER_CMO := print_real.cmo alt_ergo.cmo why3.cmo smt.cmo coq.cmo
125
PRINTER_CMO := $(addprefix src/printer/,$(PRINTER_CMO))
126

MARCHE Claude's avatar
MARCHE Claude committed
127 128 129
USERCONF_CMO := rc.cmo whyconf.cmo
USERCONF_CMO := $(addprefix src/userconf/,$(USERCONF_CMO))

130
LIBCMO = src/config.cmo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
MARCHE Claude's avatar
MARCHE Claude committed
131
         $(TRANSFORM_CMO) $(PRINTER_CMO) $(USERCONF_CMO)
132 133
LIBCMX = $(LIBCMO:.cmo=.cmx)

Andrei Paskevich's avatar
Andrei Paskevich committed
134
LIBINCLUDES = -I src $(addprefix -I src/, $(LIBDIRS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135
$(LIBCMO) $(LIBCMX): INCLUDES=$(LIBINCLUDES)
136 137
$(LIBCMX): OFLAGS+=-for-pack Why

Francois Bobot's avatar
Francois Bobot committed
138
LIBCMI  = why.cmi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139 140
LIBCMA  = why.cma
LIBCMXA = why.cmxa
141

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142 143 144 145
byte: $(LIBCMA)
opt: $(LIBCMA) $(LIBCMXA)

$(LIBCMA): why.cmo
146 147
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148
$(LIBCMXA): why.cmx
149 150 151 152
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $(LIBCMO)
153

154 155
$(LIBCMI) : why.cmo why.cmx
	@echo -n
Francois Bobot's avatar
Francois Bobot committed
156

157 158 159
why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(INCLUDES) -pack -o $@ $(LIBCMX)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160 161 162 163 164 165 166 167 168 169 170 171 172 173
include .depend.lib

.depend.lib: $(LIBGENERATED)
	$(OCAMLDEP) -slash $(LIBINCLUDES) $(LIBCMO:.cmo=.ml) $(LIBCMO:.cmo=.mli) > $@

depend: .depend.lib

##################
# why binary
##################

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

Francois Bobot's avatar
Francois Bobot committed
174 175
src/main.cmx : $(LIBCMI)

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
185 186 187
clean::
	rm -f src/main.cm[iox] src/main.annot
	rm -f bin/why.byte bin/why.opt
188

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190 191 192 193
##########
# whyml
##########

PGM_GENERATED = src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \
Francois Bobot's avatar
Francois Bobot committed
194 195 196 197
	        src/programs/pgm_parser.output src/programs/pgm_parser.ml

PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_typing.cmo pgm_main.cmo\
	   pgm_ttree.cmo pgm_ptree.cmo
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198 199 200 201 202

PGM_CMO := $(addprefix src/programs/, $(PGM_CMO))
PGM_CMX = $(PGM_CMO:.cmo=.cmx)

$(PGM_CMO) $(PGM_CMX): INCLUDES=-I src/programs/
Francois Bobot's avatar
Francois Bobot committed
203
$(PGM_CMO) $(PGM_CMX): $(LIBCMI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
204

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
205 206 207 208 209
opt:  bin/whyml.opt
byte: bin/whyml.byte

bin/whyml.opt: $(LIBCMXA) $(PGM_CMX) 
	$(if $(QUIET), @echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
210 211
	$(STRIP) $@

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212 213 214 215
bin/whyml.byte: $(LIBCMA) $(PGM_CMO) 
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
217 218
.depend.programs: $(PGM_GENERATED)
	$(OCAMLDEP) -slash -I src/programs/ $(PGM_CMO:.cmo=.ml) $(PGM_CMO:.cmo=.mli) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
219

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220 221 222 223 224 225 226 227
depend: .depend.programs

clean::
	rm -f $(PGM_GENERATED)
	rm -f src/programs/*.cm[iox] src/programs/*.o src/programs/*.annot
	rm -f bin/whyml.byte bin/whyml.opt

###############
228
# proof manager
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
229 230
###############

MARCHE Claude's avatar
whyrc  
MARCHE Claude committed
231
MANAGER_CMO := db.cmo test.cmo
MARCHE Claude's avatar
MARCHE Claude committed
232 233
MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))

MARCHE Claude's avatar
whyrc  
MARCHE Claude committed
234
$(MANAGER_CMO): INCLUDES=-I src/manager -I +sqlite3 -I +threads
Francois Bobot's avatar
Francois Bobot committed
235
$(MANAGER_CMO): $(LIBCMI)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236 237

bin/manager.byte: $(LIBCMA) $(MANAGER_CMO)
MARCHE Claude's avatar
MARCHE Claude committed
238
	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) \
MARCHE Claude's avatar
MARCHE Claude committed
239 240 241 242 243 244 245 246 247 248 249 250
		-I +sqlite3 $(EXTCMA) sqlite3.cma -o $@ $^

include .depend.manager

.depend.manager: 
	$(OCAMLDEP) -slash -I src/manager/ $(MANAGER_CMO:.cmo=.ml) $(MANAGER_CMO:.cmo=.mli) > $@

depend: .depend.programs

clean::
	rm -f src/manager/*.cm[iox] src/manager/*.o src/manager/*.annot
	rm -f bin/manager.byte bin/manager.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251 252 253 254 255 256 257 258

# graphical interface
#####################

IDE_CMO := ide_main.cmo
IDE_CMO := $(addprefix src/ide/,$(IDE_CMO))
IDE_CMX = $(IDE_CMO:.cmo=.cmx)

Andrei Paskevich's avatar
Andrei Paskevich committed
259
$(IDE_CMO) $(IDE_CMX): INCLUDES=-I src/ide/ -I +lablgtk2 -I +threads
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
260

Andrei Paskevich's avatar
Andrei Paskevich committed
261 262 263 264
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt:  bin/whyide.opt
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265 266

bin/whyide.opt: $(LIBCMXA) $(IDE_CMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
267 268 269 270
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
	    lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
	$(STRIP) $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
271 272

bin/whyide.byte: $(GCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
273 274 275
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
	    lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
276 277 278 279 280 281 282 283 284 285 286

include .depend.ide

.depend.ide:
	$(OCAMLDEP) -slash -I src/ide/ $(IDE_CMO:.cmo=.ml) $(IDE_CMO:.cmo=.mli) > $@

depend: .depend.ide

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

288 289 290 291
##############
# Coq plugin
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
292 293 294 295
ifeq (@enable_coq_support@,yes)
byte: src/coq-plugin/whytac.cmo
opt:  src/coq-plugin/whytac.cmxs
endif
296 297

COQSUBTREES = kernel lib interp parsing proofs pretyping tactics library
Andrei Paskevich's avatar
Andrei Paskevich committed
298

299 300 301 302 303 304 305
src/coq-plugin/whytac.cmo src/coq-plugin/whytac.cmxs: INCLUDES=$(COQSUBTREES:%=-I @COQLIB@/%) 
src/coq-plugin/whytac.cmo: BFLAGS+=-rectypes
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes

src/coq-plugin/whytac.cmxs: $(LIBCMXA) src/coq-plugin/whytac.ml
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

306 307 308
# test targets
##############

Francois Bobot's avatar
Francois Bobot committed
309
test: bin/why.byte  $(TOOLS)
310
	mkdir -p output_why3
311 312 313 314 315 316 317 318 319 320
	ocamlrun -bt bin/why.byte -I theories/ -D drivers/why3.drv \
		-o output_why3 src/test.why
	bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		src/test.why -t Test -g G
	bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		--timeout 3 --prove src/test.why -t Test -g G
	bin/why.byte -D drivers/coq.drv -I theories/ \
		src/test.why -t Test -g G 
	echo bin/why.byte -D drivers/alt_ergo.drv -I theories/ \
		--timeout 1 --prove theories/real.why 
MARCHE Claude's avatar
MARCHE Claude committed
321
	@printf "*** Checking Coq file generation ***\\n"
322
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
323
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
324 325
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
MARCHE Claude's avatar
MARCHE Claude committed
326
		floating_point.Test array.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
327
		; do \
MARCHE Claude's avatar
MARCHE Claude committed
328
	  printf "Generating Coq file for $$i\\n" && bin/why.byte \
329 330
		-D drivers/coq.drv -I theories/ \
		-o output_coq -t $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
331
	@printf "*** Checking Coq compilation ***\\n"
332
	@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
333

334 335
testl: bin/whyml.byte
	ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw
336

337 338
examples/programs/%: bin/whyml.byte
	bin/whyml.byte -I theories examples/programs/$*.mlw
339

Francois Bobot's avatar
Francois Bobot committed
340 341 342
#tools
######

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343 344 345 346
TOOLS = bin/why-cpulimit

byte opt: $(TOOLS)

Francois Bobot's avatar
Francois Bobot committed
347 348 349
bin/why-cpulimit: src/tools/@CPULIMIT@.c
	$(CC) -o $@ $^

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350 351 352
clean::
	rm -f bin/why-cpulimit

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
353
# bench
354
#######
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355 356 357

.PHONY: bench test

Andrei Paskevich's avatar
Andrei Paskevich committed
358
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359
	sh bench/bench "bin/why.@OCAMLBEST@ -I theories/" "bin/whyml.@OCAMLBEST@ -I theories"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360

Francois Bobot's avatar
 
Francois Bobot committed
361
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
362 363 364
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

Francois Bobot's avatar
Francois Bobot committed
365 366
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
	$(TOOLS)
367 368 369 370 371 372
	bin/why.byte -D bench/plugins/helloworld.drv -I theories/ \
        src/test.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv -I theories/ \
        src/test.why -t Test -g G
	bin/why.$(OCAMLBEST) -D bench/plugins/simplify_array.drv -I theories/ \
        src/test.why -t Test_simplify_array -g G
373

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
374 375 376
# installation
##############

Andrei Paskevich's avatar
Andrei Paskevich committed
377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
## install: install-binary install-lib install-man 
## 
## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST) 
## 
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of why-ide, even when lablgtk2 is not installed
## install-binary: 
## 	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
## 
## install-lib: 
## 	mkdir -p $(LIBDIR)/why/why
## 
## install-man:
## 	mkdir -p $(MANDIR)/man1
## 	cp -f doc/*.1 $(MANDIR)/man1
## 
## 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
## 
## 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 ======"
## 
## 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
## 
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte 
## 	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
## 
## local: install
## 
## win: why.nsi
## 	"/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
## 
## 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
444

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
445 446 447
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
449
DOC=doc/manual.pdf doc/manual.html 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
450 451 452

doc:: $(DOC)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
453 454
doc/manual.pdf: doc/manual.tex doc/version.tex
	make -C doc manual.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
455 456 457 458

doc/manual.html: doc/manual.tex doc/version.tex
	make -C doc manual.html

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459 460
clean::
	make -C doc clean
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
461

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
462
# API DOC
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
463 464
##############

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
465 466 467
APIDOCSRC = $(UTIL_CMO:.cmo=.mli) $(CORE_CMO:.cmo=.mli) \
	src/driver/call_provers.mli \
	src/driver/driver.mli \
MARCHE Claude's avatar
more db  
MARCHE Claude committed
468
	src/manager/db.mli
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
469

MARCHE Claude's avatar
API doc  
MARCHE Claude committed
470 471 472 473 474 475
.PHONY: apidoc

apidoc: $(APIDOCSRC)
	rm -f apidoc/* 
	mkdir -p apidoc
	$(OCAMLDOC) -d apidoc -html -I src/util -I src/core -I src/driver \
MARCHE Claude's avatar
more db  
MARCHE Claude committed
476
			-I +sqlite3 $(APIDOCSRC)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
477 478 479 480 481


# generic rules
###############

Francois Bobot's avatar
Francois Bobot committed
482
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs .output
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483

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

Andrei Paskevich's avatar
Andrei Paskevich committed
487
%.cmo %.cmi: %.ml
488
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
489

Andrei Paskevich's avatar
Andrei Paskevich committed
490
%.cmx %.o: %.ml
491
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
492

Francois Bobot's avatar
 
Francois Bobot committed
493
%.cmxs: %.ml %.cmx
494
	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
495

Andrei Paskevich's avatar
Andrei Paskevich committed
496
%.ml: %.mll
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
497 498
	$(OCAMLLEX) $<

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
511 512 513 514 515 516 517 518
# 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
519 520 521 522 523 524 525 526 527 528 529

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

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

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

tags:
Francois Bobot's avatar
 
Francois Bobot committed
530
	find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
531 532 533 534 535 536 537 538 539 540 541 542
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
545 546
dep: 
	$(MAKE) depend
547
	cat .depend | ocamldot | dot -Tpdf > dep.pdf
Andrei Paskevich's avatar
Andrei Paskevich committed
548
#	$(PDFVIEWER) dep.pdf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
549

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
550 551 552
# distrib
#########

Andrei Paskevich's avatar
Andrei Paskevich committed
553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658
# NAME=why-$(VERSION)
# EXPORT=export/$(NAME)
# 
# WWW = /users/www-perso/projets/why
# FTP = $(WWW)/download
# WWWKRAKATOA = /users/www-perso/projets/krakatoa
# 
# FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
#        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 \
# 	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 \
#         bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \
# 	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* \
#         frama-c-plugin/Makefile frama-c-plugin/configure \
# 	frama-c-plugin/*.ml* frama-c-plugin/share/jessie/*.h 
# 
# # ne pas distribuer ces tests-la	frama-c-plugin/tests/jessie/*.c
# 
# distrib export: source export-doc export-www export-examples export-examples-c linux
# 
# 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
# 	make -C /users/demons/filliatr/www/why install
# 
# source: export/$(NAME).tar.gz
# 	cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
# 
# 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
# 
# tarball-for-framac: 
# 	make tarball
# 	cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
# 
# tarball: 
# 	mkdir -p export
# 	cd export; rm -rf $(NAME) $(NAME).tar.gz
# 	make export/$(NAME).tar.gz
# 
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
# 
# export-examples:
# 	cp --parents $(EXFILES) $(WWW)
# 	make -C $(WWW)/examples clean depend
# 	echo "*** faire make all dans $(WWW)/examples ***"
# 
# 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
# 
# 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)
# 
# OSTYPE  ?= linux
# 
# BINARYNAME = $(NAME)-$(OSTYPE)
# 
# linux: binary
# 
# ALLBINARYFILES = $(FILES) $(BINARYFILES) 
# 
# 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
659 660 661 662

# file headers
##############
headers:
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
663
	headache -c misc/headache_config.txt -h misc/header.txt \
Andrei Paskevich's avatar
Andrei Paskevich committed
664
	    Makefile.in configure.in */*.ml */*/*.ml */*/*.ml[ily4]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
665 666 667

# myself
########
Andrei Paskevich's avatar
Andrei Paskevich committed
668

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
669
Makefile: Makefile.in config.status
Andrei Paskevich's avatar
Andrei Paskevich committed
670 671 672 673
	./config.status --file $@

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

Andrei Paskevich's avatar
Andrei Paskevich committed
675 676 677 678
doc/version.tex: doc/version.tex.in config.status
	./config.status --file $@

config.status: configure Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
679 680 681 682 683 684 685 686 687
	./config.status --recheck

configure: configure.in
	autoconf 

# clean and depend
##################

clean::
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
688
	rm -f *~ */*~ */*/*~
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
689

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
690
distclean:: clean
Andrei Paskevich's avatar
Andrei Paskevich committed
691 692
	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
693 694 695 696 697 698 699 700

#################################################################
# 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:
701
# 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
702 703 704 705 706 707 708 709
# 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.