Rocq Call 2025 05 06 - rocq-prover/rocq GitHub Wiki

• 2025-05-06, 4pm UTC+2 (Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• 9.1? (RM,...) (core team)
• stdlib CI & status (Andres)
• Welcome Sylvain

Roles

• Chairman: Matthieu / Nicolas
• Secretary: Enrico
• Attending: Andres, Matthieu, PMP, Gaetan, Romain, Sylvain, Pierre Roux, Nicolas, Theo

Notes

• Release 9.1: Gaëtan Gilbert (RM), Pierre-Marie Pédrot (rolling co-RM)

  • scripts to handle opam package upload: MS updates it
  • blockers:
    • there is a known proof of false
  • non blockers:
    • "elimination constraints" on universes
  • branch time:
    • "around" Rocq'n share

• Stdlib:

  • CI PR needs reviewer
  • last time:
    • Cyril wants to write a first roadmap for the Rocq'n share, then iterate, then call for contributors
    • contributing policy more relaxed than Rocq's one, eg self-merge PRs
  • overlays that are backward compatible can be merged ASAP
  • CI status:
    • Jasmin disables in math-comp CI, should be disable in stdlib as well (temporarily)
    • MetaCoq problem is a nix race condition, should go away
    • nix-toolbox should receive some care at the Rocq'n share

• Sylvain:

  • Inria eng in Sophia working on the Rocq Platform (3 years)
  • see what can be done with nix in the Rocq Platform (currently opam based) at the Rocq'n share
  • onboarding starts now with the platform for 9.0 kicking off

• Coq-club:

  • move to discourse by the summer
  • if we need more than 5 moderators, we need to switch plan (to a more expensive one)