Rocq Call 2025 07 15

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

Topics

• opam packages for 9.1+rc1 (https://github.com/rocq-prover/rocq/issues/20742#issuecomment-3062402993) (Gaëtan, 10min)
• Use LetPatternStyle for irrefutable patterns by default https://github.com/rocq-prover/rocq/pull/20621 (Gaëtan, 5min)
• renaming opam repo (https://github.com/rocq-prover/opam/pull/3228 & co) (Gaëtan, 10min)
• discussion triggered by https://github.com/rocq-prover/rocq/pull/20700 Should we expose internals(ish) in the refman? Should we create an "internals" page with rocq dev html/pdf resources? (Pierre Rousselin, 10 min)
• status of trakt in CI? (Pierre Roux, 5 min)

Roles

• Chairman:
• Secretary:
• Attending:

Notes (forgot to appoint a secreatary, some remembrance after the fact)

• opam packages for 9.1+rc1
  • Guillaume volunteers
  • discussion on whether the RC package should be in rocq-prover/opam or ocaml/opam-repository -> up to who does it
• Use LetPatternStyle for irrefutable patterns by default
  • no strong opinion
  • ask PIM if he opposes it
  • option to control printing remains in the TODO list of the PR (Pierre Rousselin: this is important for teaching if we don't want to expose students to destructuring let)
• renaming opam repo
  • this is to circumvent a bug appearing in dune 3.14, thus making it possible to remove the restriction on dune version
  • only need to rename on gitlab mirror (not github repo)
  • and update coqbot after that
  • discussion on whether we still need the json generated by the CI?
  • question on whether the rocq-prover.org webstie uses it -> probably not
• status of trakt in CI? (Pierre Roux, 5 min)
  • the overlay was merged in master instead of coq-master: authors are notified
• indentation based bullet behavior RFC#108
  • mathcomp devs are against curly braces
  • they offer to do something that would only emit warnings (no focusing)
  • general opinion that it wouldn't bring anything compared to the, already optional, bullet behavior of the current proposal
• discussion about "internals" documentation in html/pdf
  • consensus on the fact that formatted documents are easier to read and would make internals documentation more detailed and better written. Documents in dev/doc are mentioned as examples of internals documentation which could be better structured/written.
  • "internals" alongside the refman is agreed to be a better solution (discoverability, easier links) than a separate web page/pdf document.
  • Théo Zimmermann thinks "contributing.md" is a better starting point than the refman's refman in https://github.com/rocq-prover/rocq/pull/20700
  • Pierre Rousselin proposes to add this "internals" part with an rst version of the contributing guide during the following week.