Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Coq internals


view this post on Zulip Ali Caglayan (Feb 15 2022 at 14:33):

https://github.com/coq/coq/tree/master/dev/doc

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 15:02 UTC