Rocq Call 2025 05 13
- 2025-05-13, 4pm UTC+2 (Paris time zone offset)
- https://rendez-vous.renater.fr/rocq-call
- #20601 (error on ambiguous Require) (Pierre, 20 min)
- https://github.com/rocq-prover/rocq/pull/20614 how to find schemes (Gaëtan, 15min)
- windows CI (https://github.com/rocq-prover/rocq/pull/20464) (Gaëtan, 10min)
- Chairman: Nicolas Tabareau
- Secretary: Matthieu Sozeau
- Attending: Yves Bertot, Pierre Roux, Emilio Jesus Gallego Arias, Théo Zimmermann
- Ambiguous Requires. Shadowing happens already between installed project A and recompiling the local
-R A theoriesfor example, we want to still allow this. Gaëtan will try the installed/local flags for ROCQPATH/user-contrib on one side and -R / -Q for local packages to have a hierarchy for detecting dangerous or harmless ambiguities. - Problem with emulating the previous strategy for finding schemes on inductives in Prop (dep or not dependent). To be investigated further by Gaëtan.
- Windows CI directly using opam setup. CoqIDE and test-suite hack questions. CoqIDE support can be delayed. test-suite hacks do not seem to worry Emilio and Gaëtan for now. The PR should be finished soon, after Emilio writes a bit of doc.
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.