The Coq mailing list

[Richard Ford <richardlford AT gmail.com>]

Thanks for the information. A related question is whether there is any kind of document that is a guide to Coq internals.

On Thu, Jul 3, 2014 at 3:45 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 04/07/2014 00:22, Richard Ford wrote:
> In order to understand Coq better I'd like to read it source code. Can you
> recommend a reading order, i.e. which directories to read first?

That is a complicated question, as most as complicated as the code of
Coq itself. It depends on what you plan to do. The tactics directory may
be a good start to get a high level of understanding of the user-side API.

After that, I would read parts of pretyping and kernel. Beware though,
as half of the pretyping directory is pure arcane devoted to the
unification, so you should not try to understand everything.

The most arcanesque code is to be found in parsing and interp, so you
may wish to overlook those directories. (Some parts of it remains
mysterious to me after three years of being a coq-dev, then...)

> I'd also like to be able to step through the Coq sources using the OCaml
> debugger though I've not gotten that to work yet.

Too difficult, I think. In particular, exception handling makes the
following of the control flow a real hell on earth. This is even worse
in trunk because of the quantity of CPS code used by the ltac
interpretation...

> Do you find that using Coq on Windows works well, or is Linux a preferred
> environment?

Officially, we support both, even though we clearly lack usable feedback
from windows users, as well as machines to debug ourselves.

PMP