Makefile.in 33 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
##########################################################################
#                                                                        #
3
#  Copyright (C) 2010-2011                                               #
4 5 6
#    François Bobot                                                      #
#    Jean-Christophe Filliâtre                                           #
#    Claude Marché                                                       #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7
#    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
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
ifeq (@enable_menhirlib@,yes)
60 61
  MENHIR    = @MENHIR@ --table
  MENHIRINC = -I @MENHIRLIB@
62 63
  MENHIRLIB = menhirLib
else
64
  MENHIR    = @MENHIR@
65 66 67 68
  MENHIRINC =
  MENHIRLIB =
endif

69 70
RUBBER = @RUBBER@

71
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
72
#PDFVIEWER = @PDFVIEWER@
73

74 75
BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aer-29 -dtypes    -I src $(INCLUDES)
76

77
ifeq (@enable_profiling@,yes)
78 79 80 81
OFLAGS += -g -p
STRIP = true
endif

82 83
# external libraries common to all binaries

84
EXTOBJS =
François Bobot's avatar
META  
François Bobot committed
85
EXTLIBS = str unix nums @META_DYNLINK@
86 87 88

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
89

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90 91 92
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93

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

96 97 98 99
ifeq (@enable_local@,yes)
all: install_local
endif

100 101
plugins: plugins.@OCAMLBEST@

102
.PHONY: byte opt clean depend all install install_local install_no_local
103
.PHONY: plugins plugins.byte plugins.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
#############
106
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

109
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
110 111
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
112
	       src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113

114
LIB_UTIL = stdlib exn_printer debug pp loc print_tree \
115
	   cmdline hashweak hashcons util sysutil rc plugin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116

117
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
118

119
LIB_PARSER = ptree denv typing parser lexer
120

121
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
122
	     whyconf autodetection
123

124
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
125
		inlining split_goal \
126
		eliminate_definition eliminate_algebraic \
127
		eliminate_inductive eliminate_let eliminate_if \
128 129
		libencoding discriminate protect_enumeration \
		encoding encoding_select \
130
		encoding_decorate encoding_twin \
François Bobot's avatar
François Bobot committed
131
		encoding_explicit encoding_guard encoding_sort \
132
		encoding_instantiate simplify_array filter_trigger \
133
		introduction abstraction close_epsilon lift_epsilon \
134
		eval_match instantiate_predicate smoke_detector
135

136
LIB_PRINTER = print_number alt_ergo why3printer smtv1 smtv2 \
François Bobot's avatar
François Bobot committed
137
		coq tptp simplify gappa cvc3 yices
138

139 140 141 142 143 144
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)) \
145
	      $(addprefix src/printer/, $(LIB_PRINTER))
146

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

150
ifeq (@enable_hypothesis_selection@,yes)
151 152 153
  LIB_TRANSFORM += hypothesis_selection
  INCLUDES += -I @OCAMLGRAPHLIB@
  EXTLIBS += graph
154 155
endif

156 157 158 159
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
160

161
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
162
$(LIBCMX): OFLAGS += -for-pack Why3
163

164
# build targets
165

166 167
byte: src/why3.cma
opt:  src/why3.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
168

169
src/why3.cma: src/why3.cmo
170 171
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

172
src/why3.cmxa: src/why3.cmx
173 174
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

175
src/why3.cmo: $(LIBCMO)
176
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
177

178
src/why3.cmx: $(LIBCMX)
179 180 181
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
182

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183 184
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
185
.depend.lib: src/config.ml $(LIBGENERATED)
186
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
187 188 189

depend: .depend.lib

190 191
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
192
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
193 194
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
195 196
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
197 198 199 200 201
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
202
	rm -f src/why3.cm[aiox] src/why3.[ao] src/why3.cmxa
203
	rm -f .depend.lib
204

205 206 207
###############
# installation
###############
208

209
install_no_local::
210
	mkdir -p $(BINDIR)
211
	mkdir -p $(LIBDIR)/why3
212
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
213
	mkdir -p $(DATADIR)/why3/emacs
214
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
215
	mkdir -p $(DATADIR)/why3/theories
216
	mkdir -p $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
217 218
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
219
	cp -f modules/*.mlw $(DATADIR)/why3/modules
220
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
221 222
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
223
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
224 225
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

MARCHE Claude's avatar
MARCHE Claude committed
226 227
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
228
	cp -f src/why3.cm* $(OCAMLLIB)/why3
229
	cp -f META $(OCAMLLIB)/why3
230
	if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
231

232 233 234 235 236
ifeq (@enable_local@,yes)
install install-lib:
	@echo "Why is configured in local installation mode."
	@echo "To install Why, run ./configure --disable-local ; make ; make install"
else
237
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
238
install-lib: install_no_local_lib
239 240
endif

MARCHE Claude's avatar
MARCHE Claude committed
241 242
install-all: install install-lib

243

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
244
##################
245
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
246 247
##################

248 249
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250

251
bin/why3.opt: src/why3.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
252 253
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
254 255
	$(STRIP) $@

256
bin/why3.byte: src/why3.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
257 258
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
259

260 261 262
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

263 264
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
265

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
266
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
267
	rm -f src/main.cm[iox] src/main.annot src/main.o
268
	rm -f bin/why3.byte bin/why3.opt bin/why3
269

270
install_no_local::
271 272 273
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3

install_local: bin/why3
274

MARCHE Claude's avatar
MARCHE Claude committed
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
##################
# Why realize binary
##################

byte: bin/why3realize.byte
opt:  bin/why3realize.opt

bin/why3realize.opt: src/why3.cmxa src/realize.cmx
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why3realize.byte: src/why3.cma src/realize.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

bin/why3realize: bin/why3realize.@OCAMLBEST@
	ln -sf why3realize.@OCAMLBEST@ $@

src/realize.cmo: src/why3.cma
src/realize.cmx: src/why3.cmxa

clean::
	rm -f src/realize.cm[iox] src/realize.annot src/realize.o
	rm -f bin/realize.byte bin/realize.opt bin/realize

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

install_local: bin/why3realize

306 307 308
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
309

310 311
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
	    pgm_module pgm_wp pgm_env pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312

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

315 316 317 318 319
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

320
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
321 322

# build targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
323

324 325
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326

327
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
328 329
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330 331
	$(STRIP) $@

332
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
333 334 335
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

336 337 338
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

339
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340 341

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

343
.depend.programs:
344
	$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346 347 348
depend: .depend.programs

clean::
349 350
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
351
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
352
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
353

354 355
# test target

356 357
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
358

359 360
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
361

362 363
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
364

365 366
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
367

368 369 370
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

371
install_no_local::
372
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
373

374
install_local: bin/why3ml
375

376 377 378 379
##########
# gallery
##########

380
# we export exactly the programs that have a why3session.xml file
381 382 383

.PHONY: gallery

384 385
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
386 387 388
	@for x in `find examples/programs/ -name why3session.xml`; do \
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
389 390 391
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
392 393 394 395
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	  cd examples/programs/; \
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
	  cd ../..; \
396
	done
397

398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414
########
# 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

415 416
byte: bin/why3config.byte
opt:  bin/why3config.opt
417

418
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
419 420 421 422
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

423
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
424 425 426
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

427 428 429
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

430 431 432 433 434 435 436 437 438 439 440 441 442
# 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
443
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
444 445 446
	rm -f .why.conf
	rm -f .depend.config

447 448
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
449
		--detect --conf_file why.conf
450

451
install_no_local::
452
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
453

454
install_local: bin/why3config
455

MARCHE Claude's avatar
MARCHE Claude committed
456 457 458 459
###############
# IDE
###############

460 461
ifeq (@enable_ide@,yes)

462
IDE_FILES = xml termcode session gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
463 464 465 466 467 468 469 470

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

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

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

473
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
474

475 476
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
477

478
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
479
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
480
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
481

482
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
483
	$(if $(QUIET), @echo 'Linking  $@' &&) \
484
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
485 486
	$(STRIP) $@

487
bin/why3ide.byte: src/why3.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
488
	$(if $(QUIET),@echo 'Linking  $@' &&) \
489
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
490

491 492 493
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
494 495 496 497
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
498
.depend.ide: src/ide/xml.ml
499
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
500 501 502 503

depend: .depend.ide

clean::
504
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
505 506
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
507
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
508 509
	rm -f .depend.ide

510
install_no_local::
511 512 513
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
514

515
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
516

517

MARCHE Claude's avatar
MARCHE Claude committed
518 519 520 521
###############
# Replayer
###############

MARCHE Claude's avatar
MARCHE Claude committed
522
REPLAYER_FILES = xml termcode session replay
MARCHE Claude's avatar
MARCHE Claude committed
523 524 525 526 527 528 529 530

REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES))

REPLAYERML  = $(addsuffix .ml,  $(REPLAYERMODULES))
REPLAYERMLI = $(addsuffix .mli, $(REPLAYERMODULES))
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))

531
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
532 533 534 535 536 537

# build targets

byte: bin/why3replayer.byte
opt:  bin/why3replayer.opt

538
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
539 540 541 542
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

543
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

bin/why3replayer: bin/why3replayer.@OCAMLBEST@
	ln -sf why3replayer.@OCAMLBEST@ $@

# depend and clean targets

include .depend.replayer

.depend.replayer: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@

depend: .depend.replayer

clean::
560
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
561 562 563 564 565 566 567 568 569 570 571
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
	rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
	rm -f .depend.replayer

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

install_local: bin/why3replayer


572
###############
573
# Bench
574 575
###############

576 577
ifeq (@enable_bench@,yes)

578
BENCH_FILES = bench benchrc benchdb whybench
579 580 581

BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))

582
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
583 584 585 586 587 588

BENCHML  = $(addsuffix .ml,  $(BENCHMODULES))
BENCHMLI = $(addsuffix .mli, $(BENCHMODULES))
BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))

589
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
590 591 592

# build targets

593 594
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
595

596
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
597
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
598

599
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
600 601 602 603
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

604
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
605 606 607
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

608 609 610
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

611 612 613 614 615 616 617 618 619 620 621 622
# depend and clean targets

include .depend.bench

.depend.bench:
	$(OCAMLDEP) -slash -I src -I src/bench -I src/ide $(BENCHML) $(BENCHMLI) > $@

depend: .depend.bench

clean::
	rm -f src/bench/*.cm[iox] src/bench/*.o
	rm -f src/bench/*.annot src/bench/*~
623
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
624 625 626
	rm -f .depend.bench

install_no_local::
627 628 629
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
630

631 632
endif

633 634 635
##############
# Coq plugin
##############
636

637
ifeq (@enable_coq_support@,yes)
638

639 640 641 642 643 644 645 646 647 648 649 650 651
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))

652
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
653

654 655
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
656

657 658
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
659

660
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
661 662
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

663
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
664 665
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

666 667 668 669
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
670

671 672 673 674 675 676 677 678 679 680 681 682 683 684
include .depend.coq

.depend.coq: $(COQGENERATED)
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

depend: .depend.coq

clean::
	rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
	rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
	rm -f src/coq-plugin/*.annot src/coq-plugin/*~
	rm -f $(COQGENERATED)
	rm -f .depend.coq

685
endif
686

687 688 689
########
# Tptp2why
########
690

691
ifeq (@enable_whytptp@,yes)
692

693 694
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
695

François Bobot's avatar
François Bobot committed
696
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
697

698
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
699 700 701 702 703 704

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

705 706
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
707 708 709

# build targets

François Bobot's avatar
François Bobot committed
710
plugins.byte byte: plugins/whytptp.cmo
711
plugins.opt  opt : plugins/whytptp.cmxs
712

François Bobot's avatar
François Bobot committed
713 714
plugins/whytptp.cmxs plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
plugins/whytptp.cmxs plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
715

716
plugins/whytptp.cmxs: $(TPTPCMX)
717
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
718
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
719

720
plugins/whytptp.cmo: $(TPTPCMO)
721
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
722 723
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
724
install_no_local::
725
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/
François Bobot's avatar
François Bobot committed
726

727 728 729 730 731 732 733 734 735 736 737
# depend and clean targets

include .depend.tptp2why

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

depend: .depend.tptp2why

clean::
	rm -f $(TPTPGENERATED)
738
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
739
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
740
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
741
	rm -f plugins/whytptp.cm* plugins/whytptp.o
742 743
	rm -f .depend.tptp2why

744
endif
745

746 747 748 749
#######
# tools
#######

750
TOOLS = bin/why3-cpulimit
751 752 753

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
754
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
755
	$(CC) -Wall -o $@ $^
756 757

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

760
install_no_local::
761
	cp -f bin/why3-cpulimit $(BINDIR)/why3-cpulimit
762

763 764 765 766
#########
# why3doc
#########

767 768
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
769 770 771 772 773 774 775 776 777 778 779 780 781 782 783

WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))

WHY3DOCML  = $(addsuffix .ml,  $(WHY3DOCMODULES))
WHY3DOCMLI = $(addsuffix .mli, $(WHY3DOCMODULES))
WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))

$(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc

# build targets

byte: bin/why3doc.byte
opt:  bin/why3doc.opt

784
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
785 786 787 788
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

789
bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
790 791 792
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

793 794 795
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

796 797 798
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

799 800
# depend and clean targets

801 802
WHY3DOCGENERATED=src/why3doc/to_html.ml

803 804
include .depend.why3doc

805
.depend.why3doc: $(WHY3DOCGENERATED)
806 807 808 809 810
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
811
	rm -f $(WHY3DOCGENERATED)
812 813
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
814
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
815 816
	rm -f .depend.why3doc

817 818
install_local: bin/why3doc

819 820 821 822
########
# bench
########

François Bobot's avatar
François Bobot committed
823
.PHONY: bench test comp_bench_plugins
824

825 826
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
	$(MAKE) test-api
827
	sh bench/bench \
828 829
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
830

831
BENCH_PLUGINS_CMO := helloworld.cmo
832 833 834
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

François Bobot's avatar
François Bobot committed
835 836 837
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
838
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
839
# 	tests/test-jcf.why -T Test -G G
840
# 	bin/why3.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
François Bobot's avatar
François Bobot committed
841
# 	tests/test-jcf.why -T Test -G G
842 843

###############
844
# test targets
845
###############
846

847 848
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
849

850
test: bin/why3.byte plugins.byte $(TOOLS)
851
	mkdir -p output_why3
852 853 854 855 856
	bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
	# bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
	# bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
	# bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
	echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
857
	@printf "*** Checking Coq file generation ***\\n"
858
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
859
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
860 861
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
862
		floating_point.Test map.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
863
		; do \
864
	  printf "Generating Coq file for $$i\\n" && \
865
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
866
	@printf "*** Checking Coq compilation ***\\n"
867
	@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
868

869 870 871
testl: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
	ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
872

873 874
testl-debug: bin/why3ml.opt
	bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
875

876 877
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
878

879 880
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
881

882 883
test-api: src/why3.cma
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \
884
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
885

MARCHE Claude's avatar
MARCHE Claude committed
886
test-shape: src/why3.cma src/ide/termcode.cmo
887
	ocaml -I src/ -I src/ide/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
MARCHE Claude's avatar
MARCHE Claude committed
888

889 890
bts12244: src/why3.cma
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/bts12244.ml
891

892 893

## Examples : Plugins ##
894

895
ifeq (@enable_plugins@,yes)
896

897 898 899 900 901 902 903 904 905 906 907 908 909 910 911
PLUGDIR = examples/plugins/
PLUG_FILES = genequlin

PLUGMODULES = $(addprefix $(PLUGDIR), $(PLUG_FILES))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES))

# ifeq (@enable_plug_support@,yes)
# byte: src/plug-plugin/whytac.cma
# opt:  src/plug-plugin/whytac.cmxs
# endif

912 913
# $(PLUGCMO):  src/why3.cma
# $(PLUGCMXS): src/why3.cmxa
914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934

.PHONY: examples_plugins.byte examples_plugins.opt

examples_plugins.byte : $(PLUGCMO)
examples_plugins.opt : $(PLUGCMXS)

# depend and clean targets

include .depend.plug

.depend.plug: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I $(PLUGDIR) $(PLUGML) | sed "s/cmx/cmxs/" > $@

depend: .depend.plug

clean::
	rm -f $(PLUGDIR)/*.cm[iox] $(PLUGDIR)/*.o
	rm -f $(PLUGDIR)/*.cma $(PLUGDIR)/*.cmxs
	rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~
	rm -f $(PLUGGENERATED)
	rm -f .depend.plug
935

936
endif
937

938 939 940
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
941

942 943 944 945 946
.PHONY: doc

ifeq (@enable_doc@,yes)

doc: doc/manual.pdf
MARCHE Claude's avatar
MARCHE Claude committed
947
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
948

949
BNF = qualid label constant operator term type formula theory why_file  \
950
      typev expr module whyml_file
951
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
952 953 954 955 956 957 958 959

doc/%_bnf.tex: doc/%.bnf doc/bnf
	doc/bnf $< > $@

doc/bnf: doc/bnf.mll
	$(OCAMLLEX) $<
	$(OCAMLOPT) -o $@ doc/bnf.ml

960 961 962 963
DOC = api glossary ide intro library macros manpages \
      manual starting syntax syntaxref version whyml

DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
964

965
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
966
	cd doc; $(RUBBER) -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
967

968 969
# 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
970

971
clean::
972 973 974 975 976 977 978
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
979

980
##########
MARCHE Claude's avatar
MARCHE Claude committed
981
# API DOC
982
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
983

MARCHE Claude's avatar
MARCHE Claude committed
984 985
.PHONY: apidoc

986
MODULESTODOC = util/util util/hashweak \
987
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
988
	core/env core/task \
989 990
	driver/whyconf driver/driver \
	ide/session
MARCHE Claude's avatar
MARCHE Claude committed
991 992
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
993 994 995

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

996
apidoc: $(FILESTODOC)
997
	mkdir -p doc/apidoc
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
998
	$(OCAMLDOC) -d doc/apidoc -html -keep-code $(INCLUDES) \
999
		$(LIBINCLUDES) -I src $(FILESTODOC)
1000
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
1001

1002
install_apidoc: apidoc
1003
	rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
1004

MARCHE Claude's avatar
MARCHE Claude committed
1005
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
1006
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
1007
		$(LIBINCLUDES) -I src $(FILESTODOC)
1008
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1009

1010
clean::
1011
	rm -f doc/apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1012

1013
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1014
# generic rules
1015
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1016

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

Francois Bobot's avatar
Francois Bobot committed
1020
%.cmo: %.ml
1021
	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1022

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

Andrei Paskevich's avatar