Ali Caglayan (Feb 15 2022 at 14:33): Ali Caglayan (Feb 15 2022 at 14:33):https://github.com/coq/coq/tree/master/dev/doc
Karl Palmskog (Feb 16 2022 at 09:01):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
Karl Palmskog (Feb 16 2022 at 09:09):and the super high level architectural summary by Andrej Bauer: http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=23
Enrico Tassi (Feb 16 2022 at 09:16):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)
Karl Palmskog (Feb 16 2022 at 09:30):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 (coqdoc), etc.
Karl Palmskog (Feb 16 2022 at 09:31):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: Jun 11 2023 at 00:30 UTC