Coq Call 2024 10 29 - coq/coq GitHub Wiki

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)

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