Here is Emilio's summary of Coq internal datatypes at a high level: https://github.com/ejgallego/coq-serapi/blob/v8.13/FAQ.md#how-many-asts-does-coq-have
and the super high level architectural summary by Andrej Bauer: http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=23
This is a bit old, but still actual: https://raw.githubusercontent.com/wiki/coq/coq/files/cs1/intro-talk.pdf (see the slides with the rooster)
one thing we discussed briefly in the BBB: the Coq contribution guide is long, and the
dev/doc directory has tons of stuff. Maybe there is a need for contextual documentation, e.g., a short step-by-step guide for making changes to stdlib, one for fixing tool bugs (
clearly the bar for fixing a coqdoc issue should be (is) much lower than for hacking
kernel to add some metatheoretic extension, and the only difference emphasized in the contribution guide is "small" vs. "big".
Last updated: Jan 29 2023 at 15:02 UTC