Coq Call 2024 10 29

• October 29th 2024, 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• should commands that take a tactic (eg Solve Obligations, Hint Extern) hardcode ltac1? cf https://github.com/coq/coq/pull/19690 (Gaëtan, 15min)
• should we do some sort of "rocq sharing days" (like https://github.com/math-comp/math-comp/wiki/MathcompSharingDays) (Gaëtan, 15min)
• Integration of https://github.com/coq-community/reduction-effects into the Coq main repo (Michael Soegtrop, 10 Minutes)
• rocq cli point (https://github.com/coq/coq/pull/19764) (Gaëtan, 15min)

Roles

• Chairman: Theo
• Secretary: Enrico

Minutes

1. reduction-effects into the Coq main repo (Michael Soegtrop, 10 Minutes)

   • no real gallina debugger, at least this one gives you "print".
   • history: the user facing language and the ocaml interface was not fully clear, hence a plugin instead of a merge.
   • licensing is likely not an issue, but needs to be clarified with the well known authors
   • integration improves distribution
   • no objection to the integration
   • who does the job ? Michael will open an issue, no volunteer decided

2. should commands that take a tactic (eg Solve Obligations, Hint Extern) hardcode ltac1?

   • a point is made that some languages don't have a proof mode, so basing it on that may look weird
   • still, if there is a current proof mode, it makes sense tactic names are resolved using its environment
   • conclusion: merge and experiment, main bug is about printing that does not yet tell you in which mode it prints

3. should we do some sort of "rocq sharing days"

   • what are they? also known as "office hours", you can go there and ask. most of the time people work on some task (e.g. a PR), if someone comes and asks he gets a hot line with some expert
   • maybe shorter than 1 day
   • Gaetan will organize one to see how it goes
   • Maybe 1 every month, but not on the same focus

4. rocq cli point

   • why a single binary:
     • size (static linking...)
     • single entry point for packages (eg Snap, appimage, Flatpak)
     • trendy UX (git, apt, nix, dune, opam, ...)
   • postponed