Interactive Development Environments for Coq

This page contains instructions on how to set-up interactive development environments for Coq developments, with a specific attention to running the proofs from article Distant decimals of π.

Using coqide

coqide is the tool provided by the Coq development team to run Coq proofs. It can be installed in the following manner:

Via opam, if opam is installed you simply have to type
```
opam install coqide
```
When observing the files on the Bailey-Borwein-Plouffe formula, it is better to go that directory and call coqide in the following manner:
```
coqide -R . Plouffe <the-file>
```
For the files on the arithmetic geometric mean, the call should be:
```
coqide -R . agm <the-file>
```

Using Emacs and proof general

If you want to use Emacs and proof general, you should install Emacs by the usual approach suited to your system and proof general following the instructions from the following site. You should then add the following lines to a file named dot-emacs.el (in the directory Plouffe-...)

(load "~/.emacs.d/lisp/PG/generic/proof-site")
(custom-set-variables
  '(coq-prog-args (quote ("-emacs" "-R" "." "Plouffe"))))

and similarly you should have the following content in a file dot-emacs.el (in the directory pi-agm-...

(load "~/.emacs.d/lisp/PG/generic/proof-site")
(custom-set-variables
  '(coq-prog-args (quote ("-emacs" "-R" "." "agm"))))

In each of the development directory, you can run emacs with proof general by typing

emacs -q -l dot-emacs.el <the-file>

Edited on April 6, 2017