#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.4 ##
#############################################################################
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
#
# This Makefile was generated by the command line :
# coq_makefile AllFloat.v Closest2Plus.v Closest2Prop.v ClosestMult.v ClosestPlus.v ClosestProp.v Closest.v Digit.v Faux.v Fbound.v Fcomp.v Finduct.v Float.v Fmin.v Fnorm.v Fodd.v Fop.v FPred.v Fprop.v FroundMult.v FroundPlus.v FroundProp.v Fround.v Fsucc.v FSucc.v MSBProp.v MSB.v Option.v Paux.v RND.v Rpow.v sTactic.v Zdivides.v Zenum.v Ct2/FboundI.v Ct2/FnormI.v Expansions/EFast2Sum.v Expansions/Fast2Diff.v Expansions/Fast2Sum.v Expansions/Fexp2.v Expansions/FexpAdd.v Expansions/FexpDiv.v Expansions/FexpPlus.v Expansions/Fexp.v Expansions/ThreeSum2.v Expansions/ThreeSumProps.v Expansions/TwoSum.v FnElem/Axpy.v FnElem/DoubleRound.v FnElem/FArgReduct2.v FnElem/FArgReduct3.v FnElem/FArgReduct4.v FnElem/FArgReduct.v FnElem/FIA64elem.v FnElem/FmaErr2.v FnElem/FmaErrApprox2.v FnElem/FmaErrApprox.v FnElem/FmaErr.v FnElem/MinOrMax.v Others/AlgoPredSucc.v Others/DblRndOdd.v Others/Dekker.v Others/discriminant2.v Others/discriminant3.v Others/discriminant.v Others/Divnk.v Others/FmaEmul.v Others/FminOp.v Others/FroundDivSqrt.v Others/PradixE.v Others/Veltkamp.v
#
.DEFAULT_GOAL := all
#
# This Makefile may take arguments passed as environment variables:
# COQBIN to specify the directory where Coq binaries resides;
# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
# DSTROOT to specify a prefix to install path.
# Here is a hack to make $(eval $(shell works:
define donewline
endef
includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\n' '@'; })))
$(call includecmdwithout@,$(COQBIN)coqtop -config)
##########################
# #
# Libraries definitions. #
# #
##########################
COQLIBS?=-I . -I Ct2 -I Expansions -I FnElem -I Others
COQDOCLIBS?=
##########################
# #
# Variables definitions. #
# #
##########################
OPT?=
COQDEP?=$(COQBIN)coqdep -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
COQC?=$(COQBIN)coqc
GALLINA?=$(COQBIN)gallina
COQDOC?=$(COQBIN)coqdoc
COQCHK?=$(COQBIN)coqchk
##################
# #
# Install Paths. #
# #
##################
ifdef USERINSTALL
XDG_DATA_HOME?=$(HOME)/.local/share
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
COQLIBINSTALL=${COQLIB}user-contrib
COQDOCINSTALL=${DOCDIR}user-contrib
endif
######################
# #
# Files dispatching. #
# #
######################
VFILES:=AllFloat.v\
Closest2Plus.v\
Closest2Prop.v\
ClosestMult.v\
ClosestPlus.v\
ClosestProp.v\
Closest.v\
Digit.v\
Faux.v\
Fbound.v\
Fcomp.v\
Finduct.v\
Float.v\
Fmin.v\
Fnorm.v\
Fodd.v\
Fop.v\
FPred.v\
Fprop.v\
FroundMult.v\
FroundPlus.v\
FroundProp.v\
Fround.v\
Fsucc.v\
FSucc.v\
MSBProp.v\
MSB.v\
Option.v\
Paux.v\
RND.v\
Rpow.v\
sTactic.v\
Zdivides.v\
Zenum.v\
Ct2/FboundI.v\
Ct2/FnormI.v\
Expansions/EFast2Sum.v\
Expansions/Fast2Diff.v\
Expansions/Fast2Sum.v\
Expansions/Fexp2.v\
Expansions/FexpAdd.v\
Expansions/FexpDiv.v\
Expansions/FexpPlus.v\
Expansions/Fexp.v\
Expansions/ThreeSum2.v\
Expansions/ThreeSumProps.v\
Expansions/TwoSum.v\
FnElem/Axpy.v\
FnElem/DoubleRound.v\
FnElem/FArgReduct2.v\
FnElem/FArgReduct3.v\
FnElem/FArgReduct4.v\
FnElem/FArgReduct.v\
FnElem/FIA64elem.v\
FnElem/FmaErr2.v\
FnElem/FmaErrApprox2.v\
FnElem/FmaErrApprox.v\
FnElem/FmaErr.v\
FnElem/MinOrMax.v\
Others/AlgoPredSucc.v\
Others/DblRndOdd.v\
Others/Dekker.v\
Others/discriminant2.v\
Others/discriminant3.v\
Others/discriminant.v\
Others/Divnk.v\
Others/FmaEmul.v\
Others/FminOp.v\
Others/FroundDivSqrt.v\
Others/PradixE.v\
Others/Veltkamp.v
-include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES))
VOFILES:=$(VFILES:.v=.vo)
VOFILESINC=$(filter $(wildcard ./*),$(VOFILES))
GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)
#######################################
# #
# Definition of the toplevel targets. #
# #
#######################################
all: $(VOFILES)
spec: $(VIFILES)
gallina: $(GFILES)
html: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
gallinahtml: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
all.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
validate: $(VOFILES)
$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
beautify: $(VFILES:=.beautified)
for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
@echo 'Do not do "make clean" until you are sure that everything went well!'
@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
.PHONY: all opt byte archclean clean install userinstall depend html validate
####################
# #
# Special targets. #
# #
####################
byte:
$(MAKE) all "OPT:=-byte"
opt:
$(MAKE) all "OPT:=-opt"
userinstall:
+$(MAKE) USERINSTALL=true install
install:
install -d $(DSTROOT)$(COQLIBINSTALL)/$(INSTALLDEFAULTROOT); \
for i in $(VOFILESINC); do \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/$(INSTALLDEFAULTROOT)/`basename $$i`; \
done
install-doc:
install -d $(DSTROOT)$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/html
for i in html/*; do \
install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/$$i;\
done
clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- rm -rf html mlihtml
archclean:
rm -f *.cmx *.o
printenv:
@$(COQBIN)coqtop -config
@echo CAMLC = $(CAMLC)
@echo CAMLOPTC = $(CAMLOPTC)
@echo PP = $(PP)
@echo COQFLAGS = $(COQFLAGS)
@echo COQLIBINSTALL = $(COQLIBINSTALL)
@echo COQDOCINSTALL = $(COQDOCINSTALL)
###################
# #
# Implicit rules. #
# #
###################
%.vo %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
%.vi: %.v
$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
%.g: %.v
$(GALLINA) $<
%.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
%.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
%.g.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
%.g.html: %.v %.glob
$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@
%.v.d: %.v
$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
%.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING