Makefile.in 37.9 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
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
57 58
COQC      = @COQC@
COQDEP    = @COQDEP@
59 60
CAMLP5O   = @CAMLP5O@

Andrei Paskevich's avatar
Andrei Paskevich committed
61
DEPFLAGS  = -slash -I src
62
ifeq (@OCAMLBEST@,opt)
Andrei Paskevich's avatar
Andrei Paskevich committed
63
DEPFLAGS += -native
64 65
endif

66 67
RUBBER = @RUBBER@

68
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
69
#PDFVIEWER = @PDFVIEWER@
70

71 72
BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aer-29 -dtypes    -I src $(INCLUDES)
73

74
ifeq (@enable_profiling@,yes)
75 76 77 78
OFLAGS += -g -p
STRIP = true
endif

79 80
# external libraries common to all binaries

81
EXTOBJS =
Andrei Paskevich's avatar
Andrei Paskevich committed
82
EXTLIBS = str unix nums dynlink
83 84 85

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
86

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87 88 89
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90

91
all: @OCAMLBEST@ plugins
Francois Bobot's avatar
Francois Bobot committed
92

93 94 95 96
ifeq (@enable_local@,yes)
all: install_local
endif

97 98
plugins: plugins.@OCAMLBEST@

99
.PHONY: byte opt clean depend all install install_local install_no_local
100
.PHONY: plugins plugins.byte plugins.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102
#############
103
# Why library
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
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
107 108
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
109
	       src/driver/driver_lexer.ml src/session/xml.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
110

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

114
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
115

116
LIB_PARSER = ptree denv typing parser lexer
117

118
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
119
	     whyconf autodetection
120

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

133
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs simplify gappa \
134
	      cvc3 yices
135

François Bobot's avatar
François Bobot committed
136 137
LIB_SESSION = xml termcode session session_tools session_scheduler

138
LIBMODULES = src/config \
139 140 141 142 143
	      $(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)) \
François Bobot's avatar
François Bobot committed
144 145
	      $(addprefix src/printer/, $(LIB_PRINTER)) \
	      $(addprefix src/session/, $(LIB_SESSION))
146

François Bobot's avatar
François Bobot committed
147
LIBDIRS = util core parser driver transform printer session
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

Andrei Paskevich's avatar
Andrei Paskevich committed
156
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
157 158
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
159

Andrei Paskevich's avatar
Andrei Paskevich committed
160
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
161
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
162
$(LIBCMX): OFLAGS += -for-pack Why3
163

164 165
$(LIBDEP): $(LIBGENERATED)

166
# build targets
167

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
183
# clean and depend
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
184

Andrei Paskevich's avatar
Andrei Paskevich committed
185 186 187
ifneq "$(MAKECMDGOALS)" "clean"
include $(LIBDEP)
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
188

189
depend: $(LIBDEP)
190

Andrei Paskevich's avatar
Andrei Paskevich committed
191
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
192 193
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
194 195
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
196
	   $(addsuffix /*.dep, $(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

204 205 206
###############
# installation
###############
207

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

MARCHE Claude's avatar
MARCHE Claude committed
225 226
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
227
	cp -f src/why3.cm* $(OCAMLLIB)/why3
228
	cp -f META $(OCAMLLIB)/why3
229
	if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
MARCHE Claude's avatar
MARCHE Claude committed
230
	if test -f src/why3.o; then cp -f src/why3.o $(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 244 245 246
##################
# Why plugins
##################

Andrei Paskevich's avatar
Andrei Paskevich committed
247 248
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli
249 250

PLUG_PARSER = genequlin
251
PLUG_PRINTER = tptpfof
252
PLUG_TRANSFORM =
Andrei Paskevich's avatar
Andrei Paskevich committed
253
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer
254

Andrei Paskevich's avatar
Andrei Paskevich committed
255
PLUGINS = genequlin tptpfof tptp
256

Andrei Paskevich's avatar
Andrei Paskevich committed
257
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
Andrei Paskevich's avatar
Andrei Paskevich committed
258

Andrei Paskevich's avatar
Andrei Paskevich committed
259 260
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
261 262 263

PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
264
	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
265
	      $(TPTPMODULES)
266

Andrei Paskevich's avatar
Andrei Paskevich committed
267
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
268 269 270
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
271
PLUGDIRS = parser printer transform tptp
272 273
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
274
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
275 276
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)

277 278
$(PLUGDEP): $(PLUGGENERATED)

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
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 $@ $<

Andrei Paskevich's avatar
Andrei Paskevich committed
306
lib/plugins/tptp.cmxs: $(TPTPCMX)
Andrei Paskevich's avatar
Andrei Paskevich committed
307
	$(if $(QUIET), @echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
308
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
309

Andrei Paskevich's avatar
Andrei Paskevich committed
310
lib/plugins/tptp.cmo: $(TPTPCMO)
Andrei Paskevich's avatar
Andrei Paskevich committed
311
	$(if $(QUIET),@echo 'Linking  $@' &&) \
Andrei Paskevich's avatar
Andrei Paskevich committed
312
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
313 314 315 316 317 318

PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
	    $(addsuffix /*.annot, $(PLUGSDIRS)) \
	    $(addsuffix /*.output, $(PLUGSDIRS)) \
	    $(addsuffix /*.automaton, $(PLUGSDIRS)) \
Andrei Paskevich's avatar
Andrei Paskevich committed
319
	    $(addsuffix /*.dep, $(PLUGSDIRS)) \
320 321 322
	    $(addsuffix /*.o, $(PLUGSDIRS)) \
	    $(addsuffix /*~, $(PLUGSDIRS))

Andrei Paskevich's avatar
Andrei Paskevich committed
323 324 325 326 327 328
# depend and clean targets

ifneq "$(MAKECMDGOALS)" "clean"
include $(PLUGDEP)
endif

329
depend: $(PLUGDEP)
Andrei Paskevich's avatar
Andrei Paskevich committed
330

331 332 333 334 335 336 337 338
clean::
	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
	rm -f lib/plugins/*

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

339

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340
##################
341
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342 343
##################

344 345
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346

347
bin/why3.opt: src/why3.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
348 349
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350 351
	$(STRIP) $@

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

356 357 358
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

359 360
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
361

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
362
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
363
	rm -f src/main.cm[iox] src/main.annot src/main.o
364
	rm -f bin/why3.byte bin/why3.opt bin/why3
365

366
install_no_local::
367
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
368 369

install_local: bin/why3
370

371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403
########
# Whyml (new API)
########

MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module mlw_typing mlw_main

MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))

MLWDEP = $(addsuffix .dep, $(MLWMODULES))
MLWCMO = $(addsuffix .cmo, $(MLWMODULES))
MLWCMX = $(addsuffix .cmx, $(MLWMODULES))

$(MLWDEP): DEPFLAGS += -I src/whyml
$(MLWCMO) $(MLWCMX): INCLUDES += -I src/whyml

# build targets

byte: $(MLWCMO)
opt:  $(MLWCMX)

# depend and clean targets

ifneq "$(MAKECMDGOALS)" "clean"
include $(MLWDEP)
endif

depend: $(MLWDEP)

clean::
	rm -f src/whyml/*.cm[iox] src/whyml/*.o
	rm -f src/whyml/*.annot src/whyml/*.dep src/whyml/*~
#	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml

404 405 406
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407

408
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
Andrei Paskevich's avatar
Andrei Paskevich committed
409
	    pgm_module pgm_wp pgm_typing pgm_ocaml pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410

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

Andrei Paskevich's avatar
Andrei Paskevich committed
413
PGMDEP = $(addsuffix .dep, $(PGMMODULES))
414 415 416
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
417
$(PGMDEP): DEPFLAGS += -I src/programs
418
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
419 420

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

422 423
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424

425
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) src/main.cmx
426 427
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
428 429
	$(STRIP) $@

430
bin/why3ml.byte: src/why3.cma $(PGMCMO) $(MLWCMO) src/main.cmo
431 432 433
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

434 435 436
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

437
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438

Andrei Paskevich's avatar
Andrei Paskevich committed
439 440 441
ifneq "$(MAKECMDGOALS)" "clean"
include $(PGMDEP)
endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
442

Andrei Paskevich's avatar
Andrei Paskevich committed
443
depend: $(PGMDEP)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
444 445

clean::
446
	rm -f src/programs/*.cm[iox] src/programs/*.o
Andrei Paskevich's avatar
Andrei Paskevich committed
447
	rm -f src/programs/*.annot src/programs/*.dep src/programs/*~
448
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
449

450 451
# test target

452 453
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
454

455 456
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
457

458 459
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
460

461 462
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
463

464 465 466
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

467
install_no_local::
468
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml$(EXE)
469

470
install_local: bin/why3ml
471

472 473 474 475
##########
# gallery
##########

476
# we export exactly the programs that have a why3session.xml file
477 478 479

.PHONY: gallery

480 481
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
482 483 484
	@for x in `find examples/programs/ -name why3session.xml`; do \
	  d=`dirname $$x`; \
	  f=`basename $$d`; \
485 486 487
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
488 489 490 491
	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
	  cd examples/programs/; \
	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
	  cd ../..; \
492
	done
493

494 495 496 497 498 499 500 501
########
# Config
########

CONFIG_FILES = whyconfig

CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))

Andrei Paskevich's avatar
Andrei Paskevich committed
502
CONFIGDEP = $(addsuffix .dep, $(CONFIGMODULES))
503 504 505
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
506
$(CONFIGDEP): DEPFLAGS += -I src/programs
507 508 509 510
$(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs

# build targets

511 512
byte: bin/why3config.byte
opt:  bin/why3config.opt
513

514
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
515 516 517 518
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

519
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
520 521 522
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

523 524 525
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

526 527
# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
528 529 530
ifneq "$(MAKECMDGOALS)" "clean"
include $(CONFIGDEP)
endif
531

Andrei Paskevich's avatar
Andrei Paskevich committed
532
depend: $(CONFIGDEP)
533 534 535

clean::
	rm -f src/config/*.cm[iox] src/config/*.o
Andrei Paskevich's avatar
Andrei Paskevich committed
536
	rm -f src/config/*.annot src/config/*.dep src/config/*~
537
	rm -f src/config/*.output src/config/*.automaton
538
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
539

540 541
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
542
		--detect --conf_file why.conf
543

544
install_no_local::
545
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
546

547
install_local: bin/why3config
548

MARCHE Claude's avatar
MARCHE Claude committed
549 550 551 552
###############
# IDE
###############

553 554
ifeq (@enable_ide@,yes)

François Bobot's avatar
François Bobot committed
555
IDE_FILES = gconfig gmain
MARCHE Claude's avatar
MARCHE Claude committed
556 557 558

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

Andrei Paskevich's avatar
Andrei Paskevich committed
559
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
560 561 562
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
563
$(IDEDEP): DEPFLAGS += -I src/ide
564
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
565

566
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
567

568 569
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
570

571
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
572
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
573
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
574

575
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
576
	$(if $(QUIET), @echo 'Linking  $@' &&) \
577
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
578 579
	$(STRIP) $@

580
bin/why3ide.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
581
	$(if $(QUIET),@echo 'Linking  $@' &&) \
582
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
583

584 585 586
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
587 588
# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
589 590 591
ifneq "$(MAKECMDGOALS)" "clean"
include $(IDEDEP)
endif
MARCHE Claude's avatar
MARCHE Claude committed
592

Andrei Paskevich's avatar
Andrei Paskevich committed
593
depend: $(IDEDEP)
MARCHE Claude's avatar
MARCHE Claude committed
594 595

clean::
596
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
597
	rm -f src/ide/*.cm[iox] src/ide/*.o
Andrei Paskevich's avatar
Andrei Paskevich committed
598
	rm -f src/ide/*.annot src/ide/*.dep src/ide/*~
599
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
600

601
install_no_local::
602
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE)
603 604

install_local: bin/why3ide
605

606
endif
MARCHE Claude's avatar
d  
MARCHE Claude committed
607

608

MARCHE Claude's avatar
MARCHE Claude committed
609 610 611 612
###############
# Replayer
###############

François Bobot's avatar
François Bobot committed
613
REPLAYER_FILES = replay
MARCHE Claude's avatar
MARCHE Claude committed
614 615 616

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

Andrei Paskevich's avatar
Andrei Paskevich committed
617
REPLAYERDEP = $(addsuffix .dep, $(REPLAYERMODULES))
MARCHE Claude's avatar
MARCHE Claude committed
618 619 620
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
621
$(REPLAYERDEP): DEPFLAGS += -I src/ide
Andrei Paskevich's avatar
Andrei Paskevich committed
622
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
623 624 625 626 627 628

# build targets

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

629
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
MARCHE Claude's avatar
MARCHE Claude committed
630 631 632 633
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

634
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
MARCHE Claude's avatar
MARCHE Claude committed
635 636 637 638 639 640 641 642
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

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

# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
643 644 645
ifneq "$(MAKECMDGOALS)" "clean"
include $(REPLAYERDEP)
endif
MARCHE Claude's avatar
MARCHE Claude committed
646

Andrei Paskevich's avatar
Andrei Paskevich committed
647
depend: $(REPLAYERDEP)
MARCHE Claude's avatar
MARCHE Claude committed
648 649 650 651 652

clean::
	rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer

install_no_local::
653
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
MARCHE Claude's avatar
MARCHE Claude committed
654 655 656

install_local: bin/why3replayer

657 658 659 660 661 662

###############
# Session
###############

SESSION_FILES = why3session_lib why3session_mod why3session_copy \
663
		why3session_info why3session_rm why3session
664 665 666

SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))

Andrei Paskevich's avatar
Andrei Paskevich committed
667
SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
668 669 670
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
671
$(SESSIONDEP): DEPFLAGS += -I src/why3session
672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session

# build targets

byte: bin/why3session.byte
opt:  bin/why3session.opt

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

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

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

# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
693 694 695
ifneq "$(MAKECMDGOALS)" "clean"
include $(SESSIONDEP)
endif
696

Andrei Paskevich's avatar
Andrei Paskevich committed
697
depend: $(SESSIONDEP)
698 699

clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
700 701
	rm -f src/why3session/*.cm[iox] src/why3session/*.o
	rm -f src/why3session/*.annot src/why3session/*.dep src/why3session/*~
702 703 704 705 706 707 708
	rm -f bin/why3session.byte bin/why3session.opt bin/why3session

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

install_local: bin/why3session

709 710 711 712
###############
# Stats
###############

François Bobot's avatar
François Bobot committed
713
STATS_FILES = stats
714 715 716

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

Andrei Paskevich's avatar
Andrei Paskevich committed
717
STATSDEP = $(addsuffix .dep, $(STATSMODULES))
718 719 720
STATSCMO = $(addsuffix .cmo, $(STATSMODULES))
STATSCMX = $(addsuffix .cmx, $(STATSMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
721
$(STATSDEP): DEPFLAGS += -I src/ide
722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742
$(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

Andrei Paskevich's avatar
Andrei Paskevich committed
743 744 745
ifneq "$(MAKECMDGOALS)" "clean"
include $(STATSDEP)
endif
746

Andrei Paskevich's avatar
Andrei Paskevich committed
747
depend: $(STATSDEP)
748 749 750 751 752 753 754 755 756

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

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

install_local: bin/why3stats

757 758 759 760
###############
# Html
###############

François Bobot's avatar
François Bobot committed
761
HTML_FILES = html_session
762 763 764

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

Andrei Paskevich's avatar
Andrei Paskevich committed
765
HTMLDEP = $(addsuffix .dep, $(HTMLMODULES))
766 767 768
HTMLCMO = $(addsuffix .cmo, $(HTMLMODULES))
HTMLCMX = $(addsuffix .cmx, $(HTMLMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
769
$(HTMLDEP): DEPFLAGS += -I src/ide
770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790
$(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

Andrei Paskevich's avatar
Andrei Paskevich committed
791 792 793
ifneq "$(MAKECMDGOALS)" "clean"
include $(HTMLDEP)
endif
794

Andrei Paskevich's avatar
Andrei Paskevich committed
795
depend: $(HTMLDEP)
796 797 798 799 800 801 802 803 804

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

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

install_local: bin/why3html

MARCHE Claude's avatar
MARCHE Claude committed
805

806
###############
807
# Bench
808 809
###############

810 811
ifeq (@enable_bench@,yes)

812
BENCH_FILES = worker db bench benchrc benchdb whybench
813 814 815

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

Andrei Paskevich's avatar
Andrei Paskevich committed
816
BENCHDEP = $(addsuffix .dep, $(BENCHMODULES))
817 818 819
BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
820
$(BENCHDEP): DEPFLAGS += -I src/bench
821
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/bench -I @SQLITE3LIB@
822 823 824

# build targets

825 826
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
827

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

831
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
832 833 834 835
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

836
bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
837 838 839
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

840 841 842
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

843 844
# depend and clean targets

Andrei Paskevich's avatar
Andrei Paskevich committed
845 846 847
ifneq "$(MAKECMDGOALS)" "clean"
include $(BENCHDEP)
endif
848

Andrei Paskevich's avatar
Andrei Paskevich committed
849
depend: $(BENCHDEP)
850 851 852

clean::
	rm -f src/bench/*.cm[iox] src/bench/*.o
Andrei Paskevich's avatar
Andrei Paskevich committed
853
	rm -f src/bench/*.annot src/bench/*.dep src/bench/*~
854
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
855 856

install_no_local::
857
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
858 859

install_local: bin/why3bench
860

861 862
endif

863 864 865
##############
# Coq plugin
##############
866

867
ifeq (@enable_coq_plugin@,yes)
868

869 870 871 872 873 874
COQGENERATED = src/coq-plugin/g_whytac.ml

COQ_FILES = whytac g_whytac

COQMODULES = $(addprefix src/coq-plugin/, $(COQ_FILES))

Andrei Paskevich's avatar
Andrei Paskevich committed
875
COQDEP = $(addsuffix .dep, $(COQMODULES))
876 877 878 879 880 881
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))

Andrei Paskevich's avatar
Andrei Paskevich committed
882
$(COQDEP): DEPFLAGS += -I src/coq-plugin
883
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
884

885 886
$(COQDEP): $(COQGENERATED)

887 888
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
889

890 891
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
892

893
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
894 895
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

896
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
897 898
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

899 900 901 902
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
903

Andrei Paskevich's avatar
Andrei Paskevich committed
904 905 906
ifneq "$(MAKECMDGOALS)" "clean"
include $(COQDEP)
endif
907

908
depend: $(COQDEP)
909 910 911 912

clean::
	rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
	rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
Andrei Paskevich's avatar
Andrei Paskevich committed
913
	rm -f src/coq-plugin/*.annot src/coq-plugin/*.dep src/coq-plugin/*~
914
	rm -f $(COQGENERATED)
915 916 917 918 919 920 921 922 923

endif

####################
# Coq realizations
####################

ifeq (@enable_coq_libs@,yes)

924
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
925 926
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))

927
COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
928 929
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))

930 931 932 933 934
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding Single Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
935 936

COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
937 938 939

COQV  = $(addsuffix .v,  $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
940
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))