INSTALL 1.17 KB
Newer Older
1 2 3
Prerequisites
-------------

4
You will need the Coq proof assistant (>= 8.4) with a Reals theory compiled
Guillaume Melquiond's avatar
Guillaume Melquiond committed
5 6 7
in. You will also need the Flocq library (>= 2.4, http://flocq.gforge.inria.fr/)
and the Ssreflect and Mathematical Components libraries
(http://ssr.msr-inria.inria.fr/).
8 9

The .tar.gz file is distributed with a working set of configure files. They
10 11
are not in the git repository though. Consequently, if you are building from
git, you will need autoconf (>= 2.59).
12 13 14 15 16 17 18


Configuring, compiling and installing
-------------------------------------

Ideally, you should just have to type:

19
  $ ./configure && ./remake && ./remake install
20

21 22
The environment variable COQC can be passed to the configure script in order
to set the Coq compiler command. The configure script defaults to "coqc".
Guillaume Melquiond's avatar
Guillaume Melquiond committed
23 24
Similarly, COQDEP can be used to specify the location of "coqdep". The
COQBIN environment variable can be used to set both variables at once.
25

26 27 28
Option "--libdir=DIR" sets the directory where the compiled library files
should be installed by "./remake install". By default, the target directory
is "`$COQC -where`/user-contrib/Interval".
29

30
The files are compiled at a logical location starting with "Interval".