Commit a0f39c83 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Switch to markdown.

parent 71df7866
Prerequisites
-------------
You will need the Coq proof assistant (>= 8.4) with a Reals theory
compiled in.
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).
Configuring, compiling and installing
-------------------------------------
Ideally, you should just have to type:
$ ./configure && ./remake && ./remake install
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.
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".
The files are compiled at a logical location starting with "Flocq".
Installation instructions
=========================
Prerequisites
-------------
You will need the [Coq proof assistant](https://coq.inria.fr/) (>= 8.4)
with the `Reals` theory compiled in.
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).
Configuring, compiling and installing
-------------------------------------
Ideally, you should just have to type:
./configure && ./remake --jobs=2 && ./remake install
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.
The option `--libdir=DIR` can be set to the directory where the compiled
library files should be installed by `./remake install`. By default, the
target directory is `` `$COQC -where`/user-contrib/Flocq ``.
The files are compiled at a logical location starting with `Flocq`.
The Flocq library provides vernacular files formalizing multi-radix
multi-precision fixed- and floating-point arithmetic for the Coq proof
assistant.
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). Authors are Sylvie Boldo <sylvie.boldo@inria.fr> and Guillaume
Melquiond <guillaume.melquiond@inria.fr>.
FLOCQ
=====
The Flocq library provides vernacular files formalizing multi-radix
multi-precision fixed- and floating-point arithmetic for the
[Coq proof assistant](https://coq.inria.fr/).
PROJECT HOME
------------
Homepage: http://flocg.gforge.inria.fr/
Repository: https://gitlab.inria.fr/flocq/flocq
Bug tracker: https://gitlab.inria.fr/flocq/flocq/issues
COPYRIGHT
---------
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](COPYING) file). Authors are Sylvie Boldo <sylvie.boldo@inria.fr>
and Guillaume Melquiond <guillaume.melquiond@inria.fr>.
INSTALLATION
------------
See the file [INSTALL.md](INSTALL.md).
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