Flocq

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.

Building and Installing using OPAM

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

Building and Installing from Sources

Downloading

• version 3.3.1 (Coq 8.7 to 8.12),
• version 3.2.1 (Coq 8.7 to 8.12),
• version 3.1.0 (Coq 8.7 to 8.9),
• version 3.0.0 (Coq 8.7 & 8.8),
• version 2.6.1 (Coq 8.4 to 8.8),
• version 2.5.2 (Coq 8.4 to 8.6),
• version 2.4.0,
• version 2.3.0,
• version 2.2.2 (Coq 8.3 & 8.4)
• version 2.1.0,
• version 2.0.0,
• version 1.4.0,
• version 1.3,
• version 1.2,
• version 1.1,
• version 1.0.

This library is hosted on the Inria Gitlab server. It was mainly developed by Sylvie Boldo and Guillaume Melquiond.

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.

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.

Documentation

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.