Coq Call 2024 08 27
- August 27th, 4pm UTC+2 (Paris time zone offset)
- https://rdv2.rendez-vous.renater.fr/coq-call
- removing no longer used compat infrastructure, c.f., encouraging experiment in #19370 (Pierre Roux, 15 min)
- 8.20 changelog #19281 (Pierre Roux, 15 min)
- moving Coq Platform Docs to the Coq's or Coq Platform's organization (Thomas Lamiaux, 15 min)
- rename
From CoqtoFrom Stdlib#19310 ready and needs an assignee (Pierre Roux, 5 min)
- Chairman: Matthieu Sozeau
- Secretary: Guillaume Melquiond
- good progress on the documentation
- currently hosted in a personal repository
- move it under the Coq umbrella, so that it becomes available to other contributors (e.g., Iris)
- final request for comments about https://github.com/coq/ceps/pull/91
- otherwise, merge the CEP in two weeks
- #19370
- currently a bit tedious for release managers and not really usable due to the hard error on unrecognized versions
- proposal: stop removing files, and turn the error into a warning
- only add new trivial files (
Require Export NextVersion) when a meaningful file is added - silence deprecation warnings in the compatibility files (need a script?)
- #19281
- how to count closed bug reports and merged pull requests? look at the milestone
- what to do about the list of maintainers? replace it with the list of assignees and reviewers? merge it with the list of contributors?
- merge assignee and reviewer list and replace maintainer list with that
- this enables to highlight the particular work of reviewer
- also solves the issue that maintainer list contains name of people who are not longer active, but we have no objective criteria for this
- mention docker-keeper
- #19310
- issue with inner modules named
Coq - why rewrite the arguments of
-Rand-Q? because of Dune
- #18385
- no opposition, but people do not really understand what it entails
- what about plugins that are statically liked? is it the case for jsCoq?
- is it maintained?
- still used for education, e.g., Pierre Rousselin (Villetaneuse), but stuck at 8.17
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq 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.