Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.
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 in the archive).
The library was first mentioned in the article "Flocq: a Unified Library for Proving Floating-Point Algorithms in Coq" [DOI] [HAL]. A lot more details are given in the book "Computer Arithmetic and Formal Proofs" [Elsevier].
If you are managing your Coq installation using OPAM, you can install the library using the following command:
$ opam install --jobs=2 coq-flocq
Note that the coq-flocq package is hosted in the OPAM
repository dedicated to
Coq libraries.
So you have to type the following command beforehand, if your OPAM
installation does not yet know about this repository.
$ opam repo add coq-released https://coq.inria.fr/opam/released
This library is hosted on the Inria Gitlab server. It was mainly developed by Sylvie Boldo and Guillaume Melquiond.
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.
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/Flocq.
The files are compiled at a logical location starting with
Flocq.
This graph shows the various files of the Flocq library and their dependencies. Note that nodes may be clicked to access a browsable version of the library.
