Remakefile.in

FILES = \
	Interval_tactic \
	Tactic \
	Eval/Eval \
	Eval/Prog \
	Eval/Reify \
	Eval/Tree \
	Float/Basic \
	Float/Generic \
	Float/Generic_ops \
	Float/Generic_proof \
	Float/Specific_bigint \
	Float/Specific_ops \
	Float/Specific_sig \
	Float/Specific_stdz \
	Float/Sig \
	Integral/Bertrand \
	Integral/Integral \
	Integral/Priority \
	Integral/Refine \
	Interval/Interval \
	Interval/Interval_compl \
	Interval/Float \
	Interval/Float_full \
	Interval/Transcend \
	Interval/Univariate_sig \
	Missing/Coquelicot \
	Missing/MathComp \
	Missing/Stdlib \
	Poly/Basic_rec \
	Poly/Bound \
	Poly/Bound_quad \
	Poly/Datatypes \
	Poly/Taylor_model \
	Poly/Taylor_model_sharp \
	Poly/Taylor_poly \
	Real/Taylor \
	Real/Xreal \
	Real/Xreal_derive \
	Tactic_float \
	@PRIM_FLOAT@

VFILES  = $(addprefix src/,$(addsuffix .v,$(FILES)))
VOFILES = $(addprefix src/,$(addsuffix .vo,$(FILES)))
GLOBS   = $(addprefix src/,$(addsuffix .glob,$(FILES)))

.PHONY: all check clean dist install

all: $(VOFILES)

clean: src/clean testsuite/clean

check: testsuite/check

Remakefile: Remakefile.in config.status
	./config.status Remakefile

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

src/Tactic_float.v: src/Tactic_bignum.v src/Tactic_primfloat.v Remakefile
	cp @PRIM_FLOAT_TAC@ src/Tactic_float.v

%.vo: %.v | src/Tactic_float.v
	@COQDEP@ -R src Interval $< | @REMAKE@ -r $@
	@COQC@ -R src Interval $<

src/clean:
	rm -f $(VOFILES) $(GLOBS)
	for d in src/*/; do \
	  rm -f $d/.coq-native/*.o $d/.coq-native/*.cm*; done
	find src -type d -name ".coq-native" -empty -prune -exec rmdir "{}" \;

testsuite/check: src/Tactic.vo
	set +e
	cd testsuite
	logfile="failures-`date '+%Y-%m-%d'`.log"
	cat /dev/null > log.tmp
	cat /dev/null > "$logfile"
	rm -f check_tmp.v
	for f in *.v; do
	  cp "$f" check_tmp.v
	  @COQC@ -R ../src Interval check_tmp.v > output.tmp 2>&1
	  return_code=$?
	  if [ ${return_code} -ne 0 ]; then
	    (echo "*** $f exited with error code ${return_code}"; cat output.tmp; echo) >> "$logfile"
	    echo "$f exited with error code ${return_code}" >> log.tmp
	  fi
	  rm -f check_tmp.v check_tmp.vo check_tmp.glob .check_tmp.aux output.tmp
	  rm -f .coq-native/N*check_tmp.o .coq-native/N*check_tmp.cm*
	done
	return_code=0
	if [ -s log.tmp ]; then
	  echo "*** Failures:"
	  cat log.tmp
	  return_code=1
	else
	  rm "$logfile"
	fi
	rm log.tmp
	exit ${return_code}

testsuite/clean:
	rm -f testsuite/failures-*.log

deps.dot: $(VFILES)
	(echo "digraph interval_deps {" ;
	echo "node [shape=ellipse, style=filled, URL=\"html/Interval.\N.html\", color=black];";
	(cd src ; @COQDEP@ -R . Interval $(addsuffix .v,$(FILES))) |
	  sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
	  while read src dst; do
	    color=$$(echo "$src" | sed -e 's,Real.*,turquoise,;s,Interval[.].*,plum,;s,Integral.*,lightcoral,;s,Poly.*,yellow,;s,Float.*,cornflowerblue,;s,Eval.*,green,;s,[A-Z].*,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

html/index.html: $(VOFILES)
	rm -rf html
	mkdir -p html
	@COQDOC@ -toc -interpolate -utf8 -html -g -R src Interval -d html \
	  --coqlib http://coq.inria.fr/distrib/current/stdlib \
	  --external https://math-comp.github.io/htmldoc mathcomp \
	  --external http://flocq.gforge.inria.fr/html Flocq \
	  --external http://coquelicot.saclay.inria.fr/html Coquelicot \
	  $(VFILES)
	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

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:
	prefix=@prefix@
	exec_prefix=@exec_prefix@
	mkdir -p @libdir@
	for d in Eval Float Integral Interval Missing Poly Real; do mkdir -p @libdir@/$d; done
	for f in $(FILES); do cp src/$f.vo @libdir@/$f.vo; done
	( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )

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