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 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)
Andrei Paskevich's avatar
Andrei Paskevich committed
60 61
  MENHIR    = @MENHIR@ --table
  MENHIRINC = -I @MENHIRLIB@
62 63
  MENHIRLIB = menhirLib
else
Andrei Paskevich's avatar
Andrei Paskevich committed
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 print_number \
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 137
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 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)
Andrei Paskevich's avatar
Andrei Paskevich committed
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)
Andrei Paskevich's avatar
Andrei Paskevich committed
211 212
	mkdir -p $(LIBDIR)/why3/plugins
	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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
246
##################
247
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248 249
##################

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

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

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

262 263 264
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

265 266
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
267

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

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

install_local: bin/why3
276

MARCHE Claude's avatar
MARCHE Claude committed
277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
##################
# 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
Andrei Paskevich's avatar
Andrei Paskevich committed
301
	rm -f bin/why3realize.byte bin/why3realize.opt bin/why3realize
MARCHE Claude's avatar
MARCHE Claude committed
302 303 304 305 306 307

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

install_local: bin/why3realize

308 309 310
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
311

312 313
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
314

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

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

322
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
323 324

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

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

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

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

338 339 340
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348 349 350
depend: .depend.programs

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

356 357
# test target

358 359
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
360

361 362
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
363

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

367 368
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
369

370 371 372
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

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

376
install_local: bin/why3ml
377

378 379 380 381
##########
# gallery
##########

382
# we export exactly the programs that have a why3session.xml file
383 384 385

.PHONY: gallery

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

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

417 418
byte: bin/why3config.byte
opt:  bin/why3config.opt
419

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

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

429 430 431
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

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

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

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

456
install_local: bin/why3config
457

MARCHE Claude's avatar
MARCHE Claude committed
458 459 460 461
###############
# IDE
###############

462 463
ifeq (@enable_ide@,yes)

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

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

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

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

475
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
476

477 478
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
479

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

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

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

493 494 495
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
496 497 498 499
# depend and clean targets

include .depend.ide

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

depend: .depend.ide

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

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

install_local: bin/why3ide
516

517
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
518

519

MARCHE Claude's avatar
MARCHE Claude committed
520 521 522 523
###############
# Replayer
###############

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

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
533
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
534 535 536 537 538 539

# build targets

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

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

545
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561
	$(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::
562
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
563 564 565 566 567 568 569 570 571 572
	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

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
###############
# 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

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 669 670 671 672
###############
# 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
673

674
###############
675
# Bench
676 677
###############

678 679
ifeq (@enable_bench@,yes)

680
BENCH_FILES = bench benchrc benchdb whybench
681 682 683

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

684
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
685 686 687 688 689 690

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

691
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
692 693 694

# build targets

695 696
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
697

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

701
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
702 703 704 705
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

706
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
707 708 709
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

710 711 712
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

713 714 715 716 717 718 719 720 721 722 723 724
# 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/*~
725
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
726 727 728
	rm -f .depend.bench

install_no_local::
729 730 731
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
732

733 734
endif

735 736 737
##############
# Coq plugin
##############
738

739
ifeq (@enable_coq_support@,yes)
740

741 742 743 744 745 746 747 748 749 750 751 752 753
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))

754
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
755

756 757
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
758

759 760
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
761

762
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
763 764
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

765
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
766 767
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

768 769 770 771
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
772

773 774 775 776 777 778 779 780 781 782 783 784 785 786
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

787
endif
788

789 790 791
########
# Tptp2why
########
792

793
ifeq (@enable_whytptp@,yes)
794

795 796
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
797

François Bobot's avatar
François Bobot committed
798
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
799

800
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
801 802 803 804 805 806

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

807 808
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
809 810 811

# build targets

Andrei Paskevich's avatar
Andrei Paskevich committed
812 813
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt  opt : lib/plugins/whytptp.cmxs
814

Andrei Paskevich's avatar
Andrei Paskevich committed
815 816
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
817

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

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

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

829 830 831 832 833 834 835 836 837 838 839
# 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)
840
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
841
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
842
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
Andrei Paskevich's avatar
Andrei Paskevich committed
843
	rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
844 845
	rm -f .depend.tptp2why

846
endif
847

848 849 850 851
#######
# tools
#######

852
TOOLS = bin/why3-cpulimit
853 854 855

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
856
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
857
	$(CC) -Wall -o $@ $^
858 859

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

862
install_no_local::
863
	cp -f bin/why3-cpulimit $(BINDIR)/why3-cpulimit
864

865 866 867 868
#########
# why3doc
#########

869 870
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
871 872 873 874 875 876 877 878 879 880 881 882 883 884 885

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

886
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
887 888 889 890
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

891
bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
892 893 894
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

895 896 897
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

898 899 900
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

901 902
# depend and clean targets

903 904
WHY3DOCGENERATED=src/why3doc/to_html.ml

905 906
include .depend.why3doc

907
.depend.why3doc: $(WHY3DOCGENERATED)
908 909 910 911 912
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
913
	rm -f $(WHY3DOCGENERATED)
914 915
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
916
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
917 918
	rm -f .depend.why3doc

919 920
install_local: bin/why3doc

921 922 923 924
########
# bench
########

François Bobot's avatar
François Bobot committed
925
.PHONY: bench test comp_bench_plugins
926

927 928
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
	$(MAKE) test-api
929
	sh bench/bench \
930 931
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
932

933
BENCH_PLUGINS_CMO := helloworld.cmo
934 935 936
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
937 938 939
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
940
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
941
# 	tests/test-jcf.why -T Test -G G
942
# 	bin/why3.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
François Bobot's avatar
François Bobot committed
943
# 	tests/test-jcf.why -T Test -G G
944 945

###############
946
# test targets
947
###############
948

949 950
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
951

952
test: bin/why3.byte plugins.byte $(TOOLS)
953
	mkdir -p output_why3
954 955 956 957 958
	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
959
	@printf "*** Checking Coq file generation ***\\n"
960
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
961
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
962 963
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
964
		floating_point.Test map.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
965
		; do \
966
	  printf "Generating Coq file for $$i\\n" && \
967
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
968
	@printf "*** Checking Coq compilation ***\\n"
969
	@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
970

971 972 973
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
974

975 976
testl-debug: bin/why3ml.opt
	bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
977

978 979
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
980

981 982
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
983

984 985
test-api: src/why3.cma
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \
MARCHE Claude's avatar
MARCHE Claude committed
986
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
987

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