Remakefile.in

FILES = \
	Version.v \
	Core/Raux.v \
	Core/Zaux.v \
	Core/Defs.v \
	Core/Digits.v \
	Core/Float_prop.v \
	Core/FIX.v \
	Core/FLT.v \
	Core/FLX.v \
	Core/FTZ.v \
	Core/Generic_fmt.v \
	Core/Round_pred.v \
	Core/Round_NE.v \
	Core/Ulp.v \
	Core/Core.v \
	Calc/Bracket.v \
	Calc/Div.v \
	Calc/Operations.v \
	Calc/Round.v \
	Calc/Sqrt.v \
	Prop/Div_sqrt_error.v \
	Prop/Mult_error.v \
	Prop/Plus_error.v \
	Prop/Relative.v \
	Prop/Sterbenz.v \
	Prop/Round_odd.v \
	Prop/Double_rounding.v \
	Prop/Emulated_succ_pred.v \
	@PRIM_FLOAT@ \
	IEEE754/SpecFloatCompat.v \
	IEEE754/BinarySingleNaN.v \
	IEEE754/Binary.v \
	IEEE754/Bits.v \
	Pff/Pff.v \
	Pff/Pff2FlocqAux.v \
	Pff/Pff2Flocq.v

OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))

EXAMPLES = \
	Average.v \
	Compute.v \
	Double_rounding_odd_radix.v \
	Homogen.v

MORE_EXAMPLES = \
	Cody_Waite.v \
	Division_u16.v \
	Sqrt_sqr.v \
	Triangle.v

EOBJS = $(addprefix examples/,$(addsuffix o,$(EXAMPLES)))
MOBJS = $(addprefix examples/,$(addsuffix o,$(MORE_EXAMPLES)))

.PHONY: all check check-more clean dist doc install

all: $(OBJS)

check: $(EOBJS)

check-more: $(MOBJS)

CONFIGURED_FILES = Remakefile src/Version.v src/IEEE754/SpecFloatCompat.v

$(CONFIGURED_FILES): %: %.in config.status
	./config.status $@

configure config.status: configure.in
	autoconf
	./config.status --recheck

%.vo: %.v | src/IEEE754/SpecFloatCompat.v
	@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
	@COQC@ @COQEXTRAFLAGS@ -R src Flocq $<

examples/%.vo: examples/%.v
	@COQDEP@ -R src Flocq -R examples FlocqEx $< | @REMAKE@ -r $@
	@COQC@ -R src Flocq -R examples FlocqEx $<

clean:
	rm -f $(OBJS) $(EOBJS) $(MOBJS) src/*.glob examples/*.glob
	for d in src src/Core src/Calc src/Prop src/Pff src/IEEE754 examples; do \
	  rm -f $d/.coq-native/*.o $d/.coq-native/*.cm*; done
	find . -type d -name ".coq-native" -empty -prune -exec rmdir "{}" \;

html/index.html: $(OBJS)
	rm -rf html
	mkdir -p html
	@COQDOC@ -toc -interpolate -utf8 -html -g -R src Flocq -d html \
	  --coqlib http://coq.inria.fr/distrib/current/stdlib \
	  $(addprefix src/,$(FILES))
	for f in html/*.html; do
	  sed -e 's;<a href="index.html">Index</a>;Go back to the <a href="../index.html">Main page</a> or <a href="index.html">Index</a>.;' -i $f
	done


deps.dot: $(addprefix src/,$(FILES)) Remakefile.in
	(echo "digraph flocq_deps { pack=true; rank=max;"
	echo "node [shape=ellipse, style=filled, URL=\"html/Flocq.\N.html\", color=black];"
	echo '{ rank=same; "Core.Zaux"; "Core.Raux"; }'
	echo '{ rank=same; "Core.FLX"; "Core.FIX"; "Core.Round_NE"; "Calc.Operations"; }'
	echo '{ rank=same; "Core.FLT"; "Core.FTZ"; }'
	echo '{ rank=same; "Core.Generic_fmt"; "Core.Ulp"; }'
	echo '{ rank=same; "IEEE754.Binary"; "IEEE754.BinarySingleNaN"; }'
	(cd src ; @COQDEP@ -R . Flocq $(FILES)) |
	  sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
	  while read src dst; do
	    color=$$(echo "$src" | sed -e 's,Core.*,turquoise,;s,Calc.*,plum,;s,Prop.*,lightcoral,;s,Pff.*,yellow,;s,IEEE754.*,cornflowerblue,;s,Version.*,white,')
	    echo "\"$src\" [fillcolor=$color];"
	    for d in $dst; do
	      echo "\"$src\" -> \"${d%.vo}\" ;"
	    done
	  done;
	echo "}") | tred > $@

deps.png: deps.dot
	dot -T png deps.dot > deps.png

deps.map: deps.dot
	dot -T cmap deps.dot | sed -e 's,>$,/>,' > deps.map

doc: html/index.html

public: deps.png deps.map html/index.html
	mkdir -p public
	sed -e '/#include deps.map/r deps.map' misc/template.html > public/index.html
	cp -r html deps.png public/

install:
	dir="${DESTDIR}@COQUSERCONTRIB@/Flocq"
	mkdir -p $dir
	for d in Core Calc Prop IEEE754 Pff; do mkdir -p $dir/$d; done
	for f in $(OBJS); do cp $f $dir/${f#src/}; done
	for f in $(FILES); do cp src/$f $dir/$f; done
	( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "$dir/{}" \; )

EXTRA_DIST = \
	configure

dist: $(EXTRA_DIST)
	PACK=@PACKAGE_TARNAME@-@PACKAGE_VERSION@
	rm -f $PACK.tar.gz
	git archive --format=tar --prefix=$PACK/ -o $PACK.tar HEAD
	tar rf $PACK.tar --transform="s,^,$PACK/," --mtime="`git show -s --format=%ci`" $(EXTRA_DIST)
	gzip -n -f --best $PACK.tar