FILES = \
	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 \
	@LANG_FILES@ \
	Missing/Coquelicot \
	Missing/MathComp@MATHCOMP_1_OR_2@ \
	Missing/MathComp1or2 \
	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 \
	Tactics/Integral_helper \
	Tactics/Interval_helper \
	Tactics/Plot_helper \
	Tactics/Root_helper \
	Tactic_float \
	@PLOT@ \
	@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

CONFIGURED_FILES = Remakefile src/Plot.v src/Missing/Int63Compat.v src/Missing/MathComp1or2.v

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

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

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

%.vo: %.v | src/Tactic_float.v src/Plot.v src/Missing/Int63Compat.v src/Missing/MathComp1or2.v
	@COQDEP@ -R src Interval $< | @REMAKE@ -r $@
	@COQC@ @COQEXTRAFLAGS@ -R src Interval $<

COQPKGS = clib engine kernel interp lib library parsing pretyping printing proofs tactics toplevel vernac plugins.ltac
PACKAGES = $(addprefix -package @COQROOT@., $(COQPKGS)) -package zarith

src/Plot/interval_plot.ml: src/Plot/plot.c Remakefile
	@CPP@ -DCOQVERSION=@COQVERSION@ -DPLOTPLUGIN=\"@PLOTPLUGIN@\" $< -o $@

src/Plot/interval_plot.cmo: src/Plot/interval_plot.ml
	@OCAMLFIND@ ocamlc -rectypes -thread $(PACKAGES) -c $< -o $@

src/Plot/interval_plot.cmxs: src/Plot/interval_plot.ml
	@OCAMLFIND@ ocamlopt -rectypes -thread $(PACKAGES) -shared $< -o $@

MLTARGETS = $(addprefix src/Plot/, @TACTIC_TARGETS@)

src/Plot.vo: src/Plot.v $(MLTARGETS)
	@COQC@ @COQEXTRAFLAGS@ @TACTIC_PARAM@ -R src Interval -I src/Plot $<

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

check: src/Tactic.vo src/Plot.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 -I ../src/Plot 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 picture.gnuplot
	  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@ -m Plot/META.coq-interval -R . Interval $(addsuffix .v,$(FILES))) |
	  sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
	  grep -v META |
	  while read src dst; do
	    color=$$(echo "$src" | sed -e 's,Real.*,turquoise,;s,Interval[.].*,plum,;s,Integral.*,lightcoral,;s,Poly.*,yellow,;s,Float.*,lightskyblue,;s,Eval.*,lawngreen,;s,Language.*,khaki,;s,Tactics.*,lightcyan,;s,Missing.*,lightgrey,;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_url https://coq.inria.fr/distrib/current/stdlib \
	  --external https://math-comp.github.io/htmldoc mathcomp \
	  --external https://flocq.gitlabpages.inria.fr/flocq/html Flocq \
	  --external https://coquelicot.gitlabpages.inria.fr/coquelicot 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:
	dir="${DESTDIR}@COQUSERCONTRIB@/Interval"
	mkdir -p $dir
	for d in Eval Float Integral Interval Language Missing Poly Real Tactics; do mkdir -p $dir/$d; done
	for f in $(FILES); do cp src/$f.vo $dir/$f.vo; done
	( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "$dir/{}" \; )
	dir="${DESTDIR}@COQINTERVALLIB@"
	mkdir -p $dir
	test -n "$(MLTARGETS)" && cp $(MLTARGETS) $dir/
	cat src/Plot/META.coq-interval | grep -v 'directory *=' > $dir/META

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`" --owner=0 --group=0 $(EXTRA_DIST)
	gzip -n -f --best $PACK.tar