Coq Call 2024 08 27 - coq/coq GitHub Wiki
Topics
- 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 Coq
to From Stdlib
#19310 ready and needs an assignee (Pierre Roux, 5 min)
Roles
- Chairman: Matthieu Sozeau
- Secretary: Guillaume Melquiond
Notes
Coq Platform Docs
- 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
Handling of -compat
infrastructure
- #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?)
Changelog for 8.20
- #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
Rename From Coq
to From Stdlib
- #19310
- issue with inner modules named
Coq
- why rewrite the arguments of
-R
and -Q
? because of Dune
Removal of legacy mode for plugin loading
- #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?
Status of jsCoq
- is it maintained?
- still used for education, e.g., Pierre Rousselin (Villetaneuse), but stuck at 8.17