Coq Call 2025 01 21 - rocq-prover/rocq GitHub Wiki

Topics

  • 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)

Roles

  • Chairman: Théo Zimmermann
  • Secretary: Matthieu Sozeau
  • Audience:

Notes

  • 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?