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

Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
You will need the Coq proof assistant (>= 8.4) with a Reals theory
5 6
compiled in.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
7 8 9
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
git, you will need autoconf (>= 2.59).
10 11 12 13 14 15 16


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

Ideally, you should just have to type:

Guillaume Melquiond's avatar
Guillaume Melquiond committed
17
  $ ./configure && ./remake && ./remake install
18

Guillaume Melquiond's avatar
Guillaume Melquiond committed
19 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".
Similarly, COQDEP can be used to specify the location of "coqdep". The
COQBIN environment variable can be used to set both variables at once.
23 24 25 26 27

The option "--libdir=DIR" can be set to the directory where the compiled
library files should be installed by "make install". By default, the
target directory is "`$COQC -where`/user-contrib/Flocq".

Guillaume Melquiond's avatar
Guillaume Melquiond committed
28
The files are compiled at a logical location starting with "Flocq".