Makefile.in 35.5 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
headers  
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
headers  
Jean-Christophe Filliâtre committed
11
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12 13 14 15 16 17 18 19
#  described in file LICENSE.                                            #
#                                                                        #
#  This software is distributed in the hope that it will be useful,      #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
#                                                                        #
##########################################################################

Andrei Paskevich's avatar
Andrei Paskevich committed
20
include Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

22 23 24 25 26 27
VERBOSEMAKE ?= @enable_verbose_make@

ifeq ($(VERBOSEMAKE),yes)
  QUIET =
else
  QUIET = yes
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28 29
endif

30
# install the binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31
DESTDIR =
32

33
prefix	    = @prefix@
34 35 36 37 38
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
39
DATADIR = $(DESTDIR)@datarootdir@
40
MANDIR  = $(DESTDIR)@mandir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
41

Andrei Paskevich's avatar
Andrei Paskevich committed
42
# OS specific stuff
43 44
EXE   = @EXE@
STRIP = @STRIP@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45 46

# other variables
47
CC        = @CC@
48 49 50 51 52 53 54 55 56 57
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@

58 59
CAMLP5O   = @CAMLP5O@

60
ifeq (@enable_menhirlib@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
61 62
  MENHIR    = @MENHIR@ --table
  MENHIRINC = -I @MENHIRLIB@
63 64
  MENHIRLIB = menhirLib
else
Andrei Paskevich's avatar
Andrei Paskevich committed
65
  MENHIR    = @MENHIR@
66 67 68 69
  MENHIRINC =
  MENHIRLIB =
endif

70 71
RUBBER = @RUBBER@

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

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

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

83 84
# external libraries common to all binaries

85
EXTOBJS =
Andrei Paskevich's avatar
Andrei Paskevich committed
86
EXTLIBS = str unix nums dynlink
87 88 89

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
90

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

95
all: @OCAMLBEST@ plugins
Francois Bobot's avatar
Francois Bobot committed
96

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

101 102
plugins: plugins.@OCAMLBEST@

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

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

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

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

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

120
LIB_PARSER = ptree denv typing parser lexer
121

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

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

137
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
138
	      cvc3 yices
139

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

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

151
ifeq (@enable_hypothesis_selection@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
152 153 154
  LIB_TRANSFORM += hypothesis_selection
  INCLUDES += -I @OCAMLGRAPHLIB@
  EXTLIBS += graph
155 156
endif

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

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

165
# build targets
166

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

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

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

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

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

# depend target
183

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

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

depend: .depend.lib

191 192
# clean target

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

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

206 207 208
###############
# installation
###############
209

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

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

234 235 236 237 238
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
239
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
240
install-lib: install_no_local_lib
241 242
endif

MARCHE Claude's avatar
MARCHE Claude committed
243 244
install-all: install install-lib

245 246 247 248 249 250 251
##################
# Why plugins
##################

PLUGGENERATED =

PLUG_PARSER = genequlin
252
PLUG_PRINTER = tptpfof
253 254
PLUG_TRANSFORM =

255
PLUGINS = genequlin tptpfof
256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 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

PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGMLI = $(addsuffix .mli, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

PLUGDIRS = parser printer transform
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

plugins.byte: $(addsuffix .cmo, $(addprefix lib/plugins/, $(PLUGINS)))
plugins.opt : $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

lib/plugins/%.cmxs: plugins/parser/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/parser/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

lib/plugins/%.cmxs: plugins/printer/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/printer/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

lib/plugins/%.cmxs: plugins/transform/%.cmx
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

lib/plugins/%.cmo: plugins/transform/%.cmo
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

include .depend.plugins

.depend.plugins: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I plugins $(PLUGINCLUDES) \
		$(PLUGML) $(PLUGMLI) > $@

depend: .depend.plugins

PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
	    $(addsuffix /*.annot, $(PLUGSDIRS)) \
	    $(addsuffix /*.output, $(PLUGSDIRS)) \
	    $(addsuffix /*.automaton, $(PLUGSDIRS)) \
	    $(addsuffix /*.o, $(PLUGSDIRS)) \
	    $(addsuffix /*~, $(PLUGSDIRS))

clean::
	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
	rm -f lib/plugins/*
	rm -f .depend.plugins

install_no_local::
	mkdir -p $(LIBDIR)/why3/plugins
	cp -f lib/plugins/* $(LIBDIR)/why3/plugins

323

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324
##################
325
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326 327
##################

328 329
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330

331
bin/why3.opt: src/why3.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
332 333
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334 335
	$(STRIP) $@

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

340 341 342
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

343 344
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
345

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
347
	rm -f src/main.cm[iox] src/main.annot src/main.o
348
	rm -f bin/why3.byte bin/why3.opt bin/why3
349

350
install_no_local::
351 352 353
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3

install_local: bin/why3
354

355 356 357
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
358

359 360
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
361

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

364 365 366 367 368
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

369
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
370 371

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

373 374
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
375

376
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
377 378
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
379 380
	$(STRIP) $@

381
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
382 383 384
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

385 386 387
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

388
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389 390

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
395 396 397
depend: .depend.programs

clean::
398 399
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
400
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
401
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402

403 404
# test target

405 406
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
407

408 409
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
410

411 412
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
413

414 415
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
416

417 418 419
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

420
install_no_local::
421
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
422

423
install_local: bin/why3ml
424

425 426 427 428
##########
# gallery
##########

429
# we export exactly the programs that have a why3session.xml file
430 431 432

.PHONY: gallery

433 434
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
435 436 437
	@for x in `find examples/programs/ -name why3session.xml`; do \
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
438 439 440
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
441 442 443 444
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	  cd examples/programs/; \
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
	  cd ../..; \
445
	done
446

447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
########
# 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

464 465
byte: bin/why3config.byte
opt:  bin/why3config.opt
466

467
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
468 469 470 471
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

472
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
473 474 475
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

476 477 478
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

479 480 481 482 483 484 485 486 487 488 489 490 491
# 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
492
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
493 494
	rm -f .depend.config

495 496
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
497
		--detect --conf_file why.conf
498

499
install_no_local::
500
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
501

502
install_local: bin/why3config
503

MARCHE Claude's avatar
MARCHE Claude committed
504 505 506 507
###############
# IDE
###############

508 509
ifeq (@enable_ide@,yes)

510
IDE_FILES = xml termcode session gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
511 512 513 514 515 516 517 518

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

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

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

521
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
522

523 524
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
525

526
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
527
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
528
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
529

530
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
531
	$(if $(QUIET), @echo 'Linking  $@' &&) \
532
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
533 534
	$(STRIP) $@

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

539 540 541
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
542 543 544 545
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
546
.depend.ide: src/ide/xml.ml
547
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
548 549 550 551

depend: .depend.ide

clean::
552
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
553 554
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
555
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
556 557
	rm -f .depend.ide

558
install_no_local::
559 560 561
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
562

563
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
564

565

MARCHE Claude's avatar
MARCHE Claude committed
566 567 568 569
###############
# Replayer
###############

MARCHE Claude's avatar
MARCHE Claude committed
570
REPLAYER_FILES = xml termcode session replay
MARCHE Claude's avatar
MARCHE Claude committed
571 572 573 574 575 576 577 578

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
579
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
580 581 582 583 584 585

# build targets

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

586
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
587 588 589 590
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

591
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607
	$(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::
608
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
609 610 611 612 613 614 615 616 617 618
	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

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 659 660 661 662 663 664 665 666 667 668
###############
# Stats
###############

STATS_FILES = xml termcode session session_ro stats

STATSMODULES = $(addprefix src/ide/, $(STATS_FILES))

STATSML  = $(addsuffix .ml,  $(STATSMODULES))
STATSMLI = $(addsuffix .mli, $(STATSMODULES))
STATSCMO = $(addsuffix .cmo, $(STATSMODULES))
STATSCMX = $(addsuffix .cmx, $(STATSMODULES))

$(STATSCMO) $(STATSCMX): INCLUDES += -I src/ide

# build targets

byte: bin/why3stats.byte
opt:  bin/why3stats.opt

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

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

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

# depend and clean targets

include .depend.stats

.depend.stats: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(STATSML) $(STATSMLI) > $@

depend: .depend.stats

clean::
	rm -f bin/why3stats.byte bin/why3stats.opt bin/why3stats
	rm -f .depend.stats

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

install_local: bin/why3stats

669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718
###############
# Html
###############

HTML_FILES = xml termcode session session_ro html_session

HTMLMODULES = $(addprefix src/ide/, $(HTML_FILES))

HTMLML  = $(addsuffix .ml,  $(HTMLMODULES))
HTMLMLI = $(addsuffix .mli, $(HTMLMODULES))
HTMLCMO = $(addsuffix .cmo, $(HTMLMODULES))
HTMLCMX = $(addsuffix .cmx, $(HTMLMODULES))

$(HTMLCMO) $(HTMLCMX): INCLUDES += -I src/ide

# build targets

byte: bin/why3html.byte
opt:  bin/why3html.opt

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

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

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

# depend and clean targets

include .depend.html

.depend.html: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(HTMLML) $(HTMLMLI) > $@

depend: .depend.html

clean::
	rm -f bin/why3html.byte bin/why3html.opt bin/why3html
	rm -f .depend.html

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

install_local: bin/why3html

MARCHE Claude's avatar
MARCHE Claude committed
719

720
###############
721
# Bench
722 723
###############

724 725
ifeq (@enable_bench@,yes)

726
BENCH_FILES = bench benchrc benchdb whybench
727 728 729

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

730
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
731 732 733 734 735 736

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

737
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
738 739 740

# build targets

741 742
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
743

Andrei Paskevich's avatar
Andrei Paskevich committed
744
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
745
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
746

747
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
748 749 750 751
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

752
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
753 754 755
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

756 757 758
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

759 760 761 762 763 764 765 766 767 768 769 770
# 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/*~
771
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
772 773 774
	rm -f .depend.bench

install_no_local::
775 776 777
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
778

779 780
endif

781 782 783
##############
# Coq plugin
##############
784

785
ifeq (@enable_coq_support@,yes)
786

787 788 789 790 791 792 793 794 795 796 797 798 799
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))

800
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
801

802 803
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
804

805 806
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
807

808
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
809 810
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

811
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
812 813
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

814 815 816 817
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
818

819 820 821 822 823 824 825 826 827 828 829 830 831 832
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

833
endif
834

835 836 837
########
# Tptp2why
########
838

839
ifeq (@enable_whytptp@,yes)
840

841 842
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
843

François Bobot's avatar
François Bobot committed
844
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
845

846
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
847 848 849 850 851 852

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

853 854
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
855 856 857

# build targets

Andrei Paskevich's avatar
Andrei Paskevich committed
858 859
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt  opt : lib/plugins/whytptp.cmxs
860

Andrei Paskevich's avatar
Andrei Paskevich committed
861 862
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
863

Andrei Paskevich's avatar
Andrei Paskevich committed
864
lib/plugins/whytptp.cmxs: $(TPTPCMX)
865
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
866
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
867

Andrei Paskevich's avatar
Andrei Paskevich committed
868
lib/plugins/whytptp.cmo: $(TPTPCMO)
869
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
870 871
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
872
install_no_local::
Andrei Paskevich's avatar
Andrei Paskevich committed
873
	cp -f lib/plugins/whytptp.cm* $(LIBDIR)/why3/plugins/
François Bobot's avatar
François Bobot committed
874

875 876 877 878 879 880 881 882 883 884 885
# 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)
886
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
887
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
888
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
Andrei Paskevich's avatar
Andrei Paskevich committed
889
	rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
890 891
	rm -f .depend.tptp2why

892
endif
893

894 895 896 897
#######
# tools
#######

898
TOOLS = bin/why3-cpulimit
899 900 901

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
902
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
903
	$(CC) -Wall -o $@ $^
904 905

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

908
install_no_local::
909
	cp -f bin/why3-cpulimit $(BINDIR)/why3-cpulimit
910

911 912 913 914
#########
# why3doc
#########

915 916
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
917 918 919 920 921 922 923 924 925 926 927 928 929 930 931

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

932
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
933 934 935 936
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

937
bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
938 939 940
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

941 942 943
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

944 945 946
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

947 948
# depend and clean targets

949 950
WHY3DOCGENERATED=src/why3doc/to_html.ml

951 952
include .depend.why3doc

953
.depend.why3doc: $(WHY3DOCGENERATED)
954 955 956 957 958
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
959
	rm -f $(WHY3DOCGENERATED)
960 961
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
962
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
963 964
	rm -f .depend.why3doc

965 966
install_local: bin/why3doc

967 968 969 970
########
# bench
########

971
.PHONY: bench test
972

973 974
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
	$(MAKE) test-api
975
	sh bench/bench \
976 977
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
978 979

###############
980
# test targets
981
###############
982

983 984
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
985

986
test: bin/why3.byte plugins.byte $(TOOLS)
987
	mkdir -p output_why3
988 989 990 991 992
	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
993
	@printf "*** Checking Coq file generation ***\\n"
994
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
995
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
996 997
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
998
		floating_point.Test map.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
999
		; do \
1000
	  printf "Generating Coq file for $$i\\n" && \
1001
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
1002
	@printf "*** Checking Coq compilation ***\\n"
1003
	@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
1004

1005 1006 1007
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
1008

1009 1010
testl-debug: bin/why3ml.opt
	bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
1011

1012 1013
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
1014

1015 1016
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
1017

1018 1019
test-api: src/why3.cma