Coq Call 2023 09 26
Pierre-Marie Pédrot edited this page Sep 26, 2023
·
9 revisions
- September 19th 4pm UTC+2 (Paris time zone offset)
- https://rdv2.rendez-vous.renater.fr/coq-call
- 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)
- Chairman: Nicolas Tabareau
- Secretary: Pierre-Marie Pédrot
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.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.