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.