This page contains links to the Coq sources for experiments we made to compute decimals of π. An article has been published on the subject, the preprint is available here.

Sources of the coq code can be gathered from the following git repository

Sources of the coq code can be gathered from the following git repository

Opam packages are also available for both developments, under the names
`coq-plouffe` and `coq-pi-agm`. Both packages are part of
the `coq-released` opam repository.

We submitted a paper "distant decimals of π" for a special issue of the
*Journal of Automated Reasoning*. The versions of the sources at
the time of submission are here:

- For the Bailey-Borwein-Plouffe formula. This development is compatible with both coq-8.5 and coq-8.6, Coquelicot 2.1.1 or 2.1.2, and mathcomp-ssreflect 1.6 or 1.6.1.
- For arithmetic-geometric means. This development is compatible only with coq-8.5, Coquelicot 2.1.1 or 2.1.2, and mathcomp-ssreflect 1.6 or 1.6.1

Minor improvements were later proposed, mostly to obtain versions that are compatible with more recent version of coq and Coquelicot (both archives made on April 6, 2017).

These developments are compatible with coq-8.6, Coquelicot 2.1.2 and mathcomp-ssreflect 1.6.1.

Another version is proposed for the Bailey-Borwein-Plouffe formula, which is compatible with Coquelicot version 3.0.0.

- If you are using
`opam`, versions of these developments compatible with the same version of coq (8.6) and Coquelicot (2.1.2) are available as opam packages`coq-plouffe.1.2.1`,`coq-pi-agm.1.1.0`. - If you don't know
`opam`but are willing to install it, Here is a summary of the necessary commands is (for instance for Debian).

sudo apt-get install opam opam init eval $(opam config env) opam repo add coq-released http://coq.inria.fr/opam/released opam install coq-8.6 coq-plouffe.1.2.1 coq-pi-agm.1.1.0

After tens of minutes of compilation,
this will create a sub-directory `.opam` in your home directory,
where `coq` commands and all the necessary packages are present.

Here is a link to more information on installing `coq` through `opam`
for other machines.

if want to run `coq` on your machine but are not willing to install `opam`,
information is available in the
following page for Linux machines
and in the following page for Windows machines.
We also hope to provide a page describing how to run the whole development using only a temporary directory to host
Coq and the compiled libraries.

Once the packages are installed, to load these developments in your version of Coq and display the statements of the main theorems, you should run the following commands.

Require Import Plouffe.CPlouffe Plouffe.Million agm.rounding_correct agm.alg2. Import rounding_big Reals. (* correctness statement for the 1000000 hexa-decimal. The computation has already been performed at installation time. *) About piDigit_1000000. (* correctness statement for arbitrary digit rank. *) About piDigit_correct. (* Correctness statement to compute one million digits. This does not launch the computation. *) About big_pi_osix. (* correctness statement for arbitrary sizes. *) About big_compute_eq. (* running computations. This is is less than a second. *) Eval native_compute in thousand_digit_pi. (* The next one is about 3 minutes. *) Eval native_compute in hundred_thousand_digit_pi.

If you want to run the computation for one million digit, you can replace
`hundred_thousand` with `million` in the last command above, this
computation will take around two hours.

If you want to run these proofs step-by-step, you need to re-compile them. For this follow the instructions from the previous section on installing, and then download the archives for plouffe and for the arithmetic-geometric mean extract them, and re-compile them.

(cd Plouffe-Submitted_article_version_nob; ./configure.sh; make) (cd pi-agm-submitted-article-version-8.6; coq_makefile -f _CoqProject -o Makefile; make)

You should now be able to one of the interactive editing tool, either `coqide`,
or Emacs with Proof general (follow this link
for instructions on how to install these programs).

Edited on April 6, 2017