Rocq Call 2026 01 20
- 16:00 UTC+1:00 (CET, Paris time zone offset)
- https://rendez-vous.renater.fr/rocq-call
- Perennial and Rocq CI (https://github.com/rocq-prover/rocq/issues/21425) (Gaëtan, 10min)
- Release 9.2.0: discuss if we can branch after the call (Nicolas, 10min)
- Chairman: PMP
- Secretary: none?
- Attending: Gaëtan Gilbert, Yann Leray, Guillaume Melquiond, Pierre-Marie Pédrot, Pierre Roux, Matthieu Sozeau, Nicolas Tabareau
- having multiple copies of libraries for each of their reverse dependencies causes endless issues with CI and overlay preparation (which we theoretically shouldn't be doing, but since we tend to be overly nice we often end up doing)
- there are a few such cases already in the CI (namely Iris, Perennial, Fiat*, Cross-crypto), obviously if any such thing would came nowaday and request entry into CI, it would be a clear no
- explore idea of copying everything in the CI (à la Debian), doing overlays only there and ask project maintainers to update whenever they want
- would make official the fact that we are the ones developing the overlays (project maintainers would likely rapidly stop supporting master since it would break in their CI)
- a few people rather against it
- conclusion: ask Perennial/Iris/Stdpp to fix their issue or remove Perennial from CI next times it breaks
- yes
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.