configure.in

AC_INIT([Interval], [3.4.2],
        [Guillaume Melquiond <guillaume.melquiond@inria.fr>],
        [interval])

m4_divert_push(99)
if test "$ac_init_help" = "long"; then
  ac_init_help=short
fi
m4_divert_pop(99)

m4_divert_push([HELP_ENABLE])
Fine tuning of the installation directory:
AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Interval@:>@])
m4_divert_pop([HELP_ENABLE])

AC_PROG_CXX

AC_DEFUN([AX_VERSION_GE], [AS_VERSION_COMPARE([$1],[$2],[$4],[$3],[$3])])

AC_ARG_VAR(COQBIN, [path to Coq executables [empty]])
if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi

AC_ARG_VAR(COQC, [Coq compiler command [coqc]])
AC_MSG_CHECKING([for coqc])
if test ! "$COQC"; then
   COQC=`which ${COQBIN}coqc`
   if test ! "$COQC"; then
      AC_MSG_RESULT([not found])
      AC_MSG_ERROR([missing Coq compiler])
   fi
fi
AC_MSG_RESULT([$COQC])

AC_MSG_CHECKING([Coq version])
coq_version=`$COQC -v | grep version | sed -e 's/^.*version \([[0-9.]]*\).*$/\1/'`
AX_VERSION_GE([$coq_version], 8.7, [],
  [AC_MSG_ERROR([must be at least 8.7 (you have version $coq_version).])])
AC_MSG_RESULT($coq_version)

AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_MSG_CHECKING([for coqdep])
if test ! "$COQDEP"; then
   COQDEP=`which ${COQBIN}coqdep`
   if test ! "$COQDEP"; then
      AC_MSG_RESULT([not found])
      AC_MSG_ERROR([missing Coq dependency analyzer])
   fi
fi
AC_MSG_RESULT([$COQDEP])

AC_ARG_VAR(COQDOC, [Coq documentation generator command [coqdoc]])
AC_MSG_CHECKING([for coqdoc])
if test ! "$COQDOC"; then
   COQDOC=`which ${COQBIN}coqdoc`
   if test ! "$COQDOC"; then
      AC_MSG_RESULT([not found])
   fi
fi
AC_MSG_RESULT([$COQDOC])

AC_MSG_CHECKING([for Flocq])
AS_IF(
  [ echo "Require Import Flocq.Version BinNat." \
         "Goal (30100 <= Flocq_version)%N. easy. Qed." > conftest.v
    $COQC conftest.v 2> conftest.err ],
  [ AC_MSG_RESULT([yes]) ],
  [ AC_MSG_RESULT([no])
    AC_MSG_ERROR([ *** Unable to find library Flocq >= 3.1 (http://flocq.gforge.inria.fr/)])])
rm -f conftest.v conftest.vo conftest.err

AC_MSG_CHECKING([for primitive floats])
AX_VERSION_GE([$coq_version], 8.11,
  [prim_float=yes],
  [prim_float=no])
AS_IF(
  [ echo "Require Import Flocq.Version BinNat." \
         "Goal (30300 <= Flocq_version)%N. easy. Qed." > conftest.v
    $COQC conftest.v 2> conftest.err ],
  [], [prim_float=no])
rm -f conftest.v conftest.vo conftest.err
AC_MSG_RESULT([$prim_float])

AC_MSG_CHECKING([for Ssreflect])
AS_IF(
  [ echo "Require Import mathcomp.ssreflect.ssreflect." > conftest.v
    $COQC conftest.v 2> conftest.err ],
  [ AC_MSG_RESULT([yes]) ],
  [ AC_MSG_RESULT([no])
    AC_MSG_ERROR([ *** Unable to find library mathcomp.ssreflect >= 1.6 (http://math-comp.github.io/math-comp/)])])
rm -f conftest.v conftest.vo conftest.err

AC_MSG_CHECKING([for Coquelicot])
AS_IF(
  [ echo "Require Import Coquelicot.Coquelicot." \
         "Check (RInt (V := R_CompleteNormedModule))." > conftest.v
    $COQC conftest.v > conftest.err 2>&1 ],
  [ AC_MSG_RESULT([yes]) ],
  [ AC_MSG_RESULT([no])
    AC_MSG_ERROR([ *** Unable to find library Coquelicot (http://coquelicot.saclay.inria.fr/)])])
rm -f conftest.v conftest.vo conftest.err

AC_MSG_CHECKING([for Bignums])
AS_IF(
  [ echo "Require Import Bignums.BigZ.BigZ." > conftest.v
    $COQC conftest.v 2> conftest.err ],
  [ AC_MSG_RESULT([yes]) ],
  [ AC_MSG_RESULT([no])
    AC_MSG_ERROR([ *** Unable to find library Bignums (https://github.com/coq/bignums/)])])
rm -f conftest.v conftest.vo conftest.err

if test "$libdir" = '${exec_prefix}/lib'; then
  libdir="`$COQC -where | tr -d '\r' | tr '\\\\' '/'`/user-contrib/Interval"
fi

if test "$prim_float" = "yes"; then
   PRIM_FLOAT=Float/Primitive_ops
   PRIM_FLOAT_TAC=src/Tactic_primfloat.v
else
   PRIM_FLOAT=
   PRIM_FLOAT_TAC=src/Tactic_bignum.v
fi
AC_SUBST(PRIM_FLOAT)
AC_SUBST(PRIM_FLOAT_TAC)

AC_MSG_NOTICE([building remake...])
case `uname -s` in
MINGW*)
	$CXX -Wall -O2 -o remake.exe remake.cpp -lws2_32
	if test $? != 0; then AC_MSG_FAILURE([failed]); fi
	AC_SUBST([REMAKE], [./remake.exe])
	;;
*)
	$CXX -Wall -O2 -o remake remake.cpp
	if test $? != 0; then AC_MSG_FAILURE([failed]); fi
	AC_SUBST([REMAKE], [./remake])
	;;
esac

AC_CONFIG_FILES(Remakefile)
AC_OUTPUT