Book cover


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].

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

Building and Installing from Sources


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.

Dependency graph

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.