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