Commit 673c1c36 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added dependency check for Flocq.

parent 196249b1
Prerequisites
-------------
You will need to have the Coq proof assistant (>= 8.1) with a Reals theory
compiled in.
You will need the Coq proof assistant (>= 8.2) with a Reals theory compiled
in. You will need the Flocq library (http://flocq.gforge.inria.fr/) to be
installed too.
The .tar.gz file is distributed with a working set of configure files. They
are not in the GIT repository though. Consequently, if you are building from
......
Version 0.12:
- added a dependency on the Flocq library
Version 0.11:
- removed i_nocheck parameter as computations are no longer done at Qed time.
- removed i_nocheck parameter as computations are no longer done at Qed time
......@@ -6,12 +6,6 @@ This package is free software; you can redistribute it and/or modify it
under the terms of GNU Lesser General Public License (see the COPYING
file). Author is Guillaume Melquiond <guillaume.melquiond@inria.fr>.
As this library relies on the fast integer library, version 8.2 of Coq
is expected for compiling it. By modifying the first lines of the
tactics.v file and removing the offending files, the library might be
usable with older versions of Coq. The library can be compiled by
issuing the command "make".
I. Invocation
-------------
......
......@@ -20,6 +20,15 @@ AC_CHECK_TOOL(COQC, coqc)
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_CHECK_TOOL(COQDEP, coqdep)
AC_MSG_CHECKING([for Flocq])
AS_IF(
[ echo "Require Fcore Fcalc_digits." > conftest.v
"$COQC" conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find the Flocq library (http://flocq.gforge.inria.fr/)])])
rm -f conftest.v conftest.vo conftest.err
if test "$libdir" = '${exec_prefix}/lib'; then
libdir='`$(COQC) -where`/user-contrib/Interval'
fi
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment