Rocq Call 2026 01 20 - rocq-prover/rocq GitHub Wiki

Topics

Roles

  • Chairman: PMP
  • Secretary: none?
  • Attending: Gaëtan Gilbert, Yann Leray, Guillaume Melquiond, Pierre-Marie Pédrot, Pierre Roux, Matthieu Sozeau, Nicolas Tabareau

Notes

Perennial in CI

  • 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

Branching 9.2

  • yes