Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq proof assistant. 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].
A presentation of the major concepts of the Flocq library is available on the following page: Flocq in a Nutshell. See below for links to the various files of the library.
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.
The library files are compiled at the logical location Flocq
.
The COQUSERCONTRIB
environment variable can be used to override
the physical location where the Flocq
directory containing these
files will be installed by ./remake install
. By default, the
target directory is `$COQC -where`/user-contrib
.
A presentation of the major concepts of the Flocq library is available on the following page: Flocq in a Nutshell.
The following graph shows the various files and their dependencies. A browsable version of the library can be accessed by clicking the nodes.