Coq Call 2023 09 26

• September 19th 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• process to finish writing up the Coq roadmap (https://github.com/coq/ceps/pull/69), setting a deadline?, and how to introduce roadmap updates at each Coq Call (Théo, 20 minutes)
• state of release summary for 8.18 and future releases (Théo, 10 minutes), see https://github.com/coq/coq/pull/17997
• a short proposal, CEP #73, to resolve the conflict between expanding (for typing) or not (for guard checking) aliases in pattern-matching (Hugo)
• ensuring Coq remains safe for async interruptions (Emilio)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Pierre-Marie Pédrot

Notes

Roadmap:

• few completed items currently
• listed points should have a description (push on the branch / open a PR)
• deadline: next week to fill up, the week after to wrap up
• Should we inform about the roadmap progress at beginning of calls?
• How do we handle evolution of the roadmap? Proposal: use the wiki?

Release of 8.18:

• Enrico wrote the changes because Matthieu was not available, delaying the release.
• What do we want in these changes? Some stuff is not directly related to the Coq release (e.g. opam / docker maintainers)
• Should we synchronize the release with credits somehow?
• TZ: update the release doc to easily find the relevant info

CEP 73:

• Proposal to expand the guard condition to handle dependent proofs on the term being matched.
• We don't know what the guard condition does already.
• Probably requires more research, discussion continued on Zulip / StackExchange.