configure.in

AC_INIT([Flocq], [3.3.1],
        [Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
        [flocq])

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

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)

AX_VERSION_GE([$coq_version], 8.11,
  [PRIM_FLOAT="IEEE754/PrimFloat.v"],
  [PRIM_FLOAT="IEEE754/SpecFloatCopy.v"])
AC_SUBST(PRIM_FLOAT)

AX_VERSION_GE([$coq_version], 8.11,
  [SPEC_FLOAT_MODULE="Coq.Floats.SpecFloat"],
  [SPEC_FLOAT_MODULE="SpecFloatCopy"])
AC_SUBST(SPEC_FLOAT_MODULE)

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_ARG_VAR(COQEXTRAFLAGS, [extra flags passed to Coq compiler [empty]])

AC_ARG_VAR(COQUSERCONTRIB, [installation directory [`$COQC -where`/user-contrib]])

if test -z "$COQUSERCONTRIB"; then
  COQUSERCONTRIB="`$COQC -where | tr -d '\r' | tr '\\\\' '/'`/user-contrib"
fi

AC_ARG_VAR(REMAKE, [Remake [vendored version]])

if test -z "$REMAKE"; then
AC_PROG_CXX

AC_MSG_NOTICE([building remake...])
case `$CXX -v 2>&1 | grep -e "^Target:"` in
*mingw*)
	$CXX -Wall -O2 -o remake.exe remake.cpp -lws2_32
	if test $? != 0; then AC_MSG_FAILURE([failed]); fi
	REMAKE=./remake.exe
	;;
*)
	$CXX -Wall -O2 -o remake remake.cpp
	if test $? != 0; then AC_MSG_FAILURE([failed]); fi
	REMAKE=./remake
	;;
esac
fi

AC_CONFIG_FILES([Remakefile src/Version.v src/IEEE754/SpecFloatCompat.v])
AC_OUTPUT