Coq Call 2022 01 12

• January 12, 2022, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Winter Coq Working Group / Meetup https://github.com/coq/coq/wiki/CoqWG-2022-02
• https://github.com/coq/coq/pull/15220 (findlib plugins)
• usefulness of strengthening the fixpoint guard checker (https://github.com/coq/coq/pull/15434)
• https://github.com/coq/coq/pull/11327 (Ali) (Inherit implicit arguments in coercions)
• GitHub action for notifying maintainers/teams about issues with specific labels (Ali)
  • https://github.com/marketplace/actions/issue-label-notifier
  • https://github.com/coq/coq/issues/15235#issuecomment-1010489917

Notes

Working group:

• the health situation is pretty precarious and totally unpredictable
• we would really like to be able to meet in person
• choice between delaying one month [to Mars 14th] and try hybrid, or go fully online
• seems delaying is bad, consensus is stick to the original dates [Feb 15-17th]
• announcement to be done today
  • ask for registration
  • ask for program requests / contributions
• discussion on the diversity session
  • we lack a team that could lead that topic
  • direct contact was pretty unsuccessful for the 2020 Coq Workshop, so had to skip it
  • use the idea of ask / fulfill program
• program to be determined based on participants / interests
• attention to time zones / family constraints

findlib support

• Enrico asks what's blocking the PR, and what's the status
• Emilio just didn't have any time to work on it at all
• We revisit the situation with our current build system and its bad bus factor:
  • using (coq.theory ...) to build the stdlib is nice, but while it allows some advanced features, it is still too experimental, also, it doesn't allow to control build rules
  • we should default to coq_dune and remove all the cruft we have
  • however Enrico would like for things to go faster
  • Emilio will have time in Jan, not a lot, but some
• Using the compat layer could help unblock the PR, so Enrico may do this
• Dune still needs an update in 2.9.2
• Emilio will post his two working trees

usefulness of strengthening the fixpoint guard checker (https://github.com/coq/coq/pull/15434)

Hugo says that the guard condition is a bit boring. It's a bit boring not to claim that coq is not strongly normalizing.
PMP says we should check with metacoq. Matthieu says that this one is more correct no need to check old guard. Hugo is proposing the change the guard algorithm. Hugo proposing a second part formalizing a notion of an "inert subterm". Everybody seems unsure if this is useful. There is a proposed fix of the guard checking not checking guardedness of expressions before/after reducing leading to possible ill-defined terms.

Fixpoint foo (n : nat) :=
  let g := foo n in
  0. 
  
Eval cbv in (foo 5).

(* stackoverflow *)

Basically this is naughty, and Hugo is fixing it.

• GitHub action for notifying maintainers/teams about issues with specific labels (Ali)
  • https://github.com/marketplace/actions/issue-label-notifier
  • https://github.com/coq/coq/issues/15235#issuecomment-1010489917

Perhaps something like a weekly email which collects issues for maintainers who are not following the repo so closely.