Coq Call 2024 10 08 - coq/coq GitHub Wiki

Topics

  • Way to prepend/append things when setting string options like Warnings (Pierre Roux, 10 minutes)
    for instance #[prepend] Set Warnings "-some-warn". when Warnings was +other-warns would lead to -some-warn,+other-warns
    (in fact I don't really need that, it's already append by default for Warnings)
  • CI policy: deadline #19562 (Pierre Roux, 15 minutes)
  • Stdlib repo #19530 (Andres Erbsen, 15 minutes?)
  • Clarifying status of projects developed / supported by the Coq team on the future Rocq website*. Moving projects developed by the Coq team to the Coq organization: Equations and VsCoq (+ Stdlib). (Théo, Matthieu, Nicolas, 15 minutes)
  • Rocq renaming update (Théo, 5 minutes)
  • github.dev support (5 mins, Emilio)

Moved from last week:

*Projects developed by the Coq team: Coq, Stdlib, Platform, Platform Docs, VsCoq, Equations, coqbot, opam. Projects strongly supported by the Coq team, but not (yet) developed directly by the Coq team: Elpi, MetaCoq, coq-lsp / jsCoq, Alectryon, Trocq, Iris, MathComp.

Roles

  • Chairman: Nicolas
  • Secretary: Nicolas

Notes

  • Rocq renaming update: Pierre did a pass on mentions to 8.21 release to replace with Rocq 9.0
  • CI policy: make clearer that a PR needs to provide a clear guideline on how to port the code (ideally with a bit of automation) and then leave one week to maintainers. Also make clear that if an issue is found in porting the code, the deadline will be extended. In case a library/plugin is not ported after 1 week, we disable it in the CI, but don't remove it.
  • StdLib will stay in the Coq organization. Make sure that the new compilation with nix works fine or replace it. We need to discuss more on how to take the opportunity offered by the splitting to generate more contributions from outside. The StdLib maintainers should also provide a clear guideline for contributions, maybe linters ?
  • Projects developed / supported by the Coq team. Suggestion to integrate Equations even more deeply into the Coq/Rocq repo. Discussion about coq-lsp and elpi that could in a short term integrate the Coq/Rocq organization as well.