Coq Call 2025 01 21
- 2025-01-21, 4pm UTC+2 (Paris time zone offset)
- https://rendez-vous.renater.fr/coq-call
-
CoqPL presentation (Matthieu Sozeau, Nicolas Tabareau, 20min)
-
19824 (Provide a way to associate a name with a
Hint Extern) See here (Jim, 15 min) -
Need reviewer for 19761 (Refine Hint Opaque/Transparent documentation) (Jim, 10 min)
- Chairman: Théo Zimmermann
- Secretary: Matthieu Sozeau
- Audience:
-
CoqPL presentation. Use new font and color
- Clear disclaimer about renaming projects, left to user's preferences.
- Rocq Platform 2025.02 with Coq 8.20 (and 2024.10.1 with Coq 8.19)
- Rocq 9.0+rc1 (January 2025)
- Add position on Rocq Platform
- Doc Platform -> Platform Docs Link to Platform Docs contributions
- Stdlib : (now named "Stdlib") Make the Stdlib Standard Again.
- Check Coq occurrences
- Slide on docker rocq support (coqorg will remain to keep providing images for past Coq versions).
- Redirect coq.inria.fr to rocq-prover.org at the time of the 9.0 final release.
- Ask for contributions on links to lectures/podcasts/success stories.
- Next release: Template Poly is based on Sort Poly
- Living SProp
-
19824: new design decision: use a specific nametab, force each a (hint extern : database) to have a globally unique name. Warning on auto-generated names for hint externs (too fragile!), but still allow Remove Hint on them.
-
19761: Maybe Thomas Lamiaux can have a look?
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.