Commit a20da349 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added toplevel text files.

parent 34b32d56
Prerequisites
-------------
You will need the Coq proof assistant (>= 8.2) with a Reals theory
compiled in.
The .tar.gz file is distributed with a working set of configure files.
They are not in the SVN repository though. Consequently, if you are
building from SVN, you will need autoconf (>= 2.59) and automake (>= 1.8).
Configuring, compiling and installing
-------------------------------------
Ideally, you should just have to type:
$ ./configure && make && make install
The environment variable "COQC" can be set to the Coq compiler command.
The configure script defaults to "coqc".
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". This
default prefix can be removed with the "--disable-prefix" option.
Version 1.1:
- simplified effective rounding for negative reals
- proved monotonicity of exponent functions for common formats
Version 1.0:
- initial release
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>.
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