Rocq Call 2026 09 15 - rocq-prover/rocq GitHub Wiki

• 16:00 Paris time (currently CEST or UTC+2:00)
• https://rendez-vous.renater.fr/rocq-call

Topics

• exception to ltac freeze https://github.com/rocq-prover/rocq/pull/22329 (10 Enrico)
• release 9.3 (10 Enrico)
• efficiency PRs: fixpoint refolding #22272 and conversion cache (#22309, #22319, #22396, #22401) (20-30 minutes, Hugo)

Roles

• Chairman:
• Secretary:
• Attending:

Notes

• Release 9.3.

PR to backport: https://github.com/rocq-prover/rocq/pull/22357 (ok) https://github.com/rocq-prover/rocq/pull/22456 (pas backportée)

How to backport changelogs? It seems what Enrico did was the right thing, i.e. backporting stuff by hand. The script is not adapted to the current situation, where we have several branches being released in parallel.

• PR #22329: no strong opposition, this is horrendous code already. The first to merge loses the game.

• Conversion cache PR: support from PMP. We need to ensure that it is really sound. Some cleanup needed, user-facing flags, and additional experiments to fine-tune the cache.

• Fixpoint refolding PR: probably unsound, we need the kernel to check for cumulativity and store this data. We also need to guard the behaviour behind a flag.