Coq Call 2022 02 09 - coq/coq GitHub Wiki

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

Topics

• Status of the mind_finite field of inductive types (reflect the keyword use at definition time or tell if the type is really non-recursive, independently of the keyword) see e.g. #8226 [HH]
• Unifying the name of functions for destructing sequences of lambda/prod and letins (#15582) [HH]
• Satisfied with intermediate status of parametricity-based implementation of Boolean equality (#15527)?
• Need an assignee for https://github.com/coq/coq/pull/15549 (Ali)
• Display git hash in non-release versions: https://github.com/coq/coq/pull/15639 (Ali)
  • Pros: Easy to copy and paste for users of opam master etc. Makes debugging "version master" from ancient issues easier. Everybody else does it.
  • Cons: Not clear how to make reproducible. Depends on git. Messes up build order.
• If Emilio is present, what to do about https://github.com/coq/coq/pull/15645 (Ali)
• Making Ltac2 independent (Ali)
  • Would be nice for HoTT to use the Ltac2 library without any of the stdlib.
• Hackathon: (Ali)
  • We have some more requested sessions, any takers? https://github.com/coq/coq/wiki/CoqWG-2022-02#requested

Notes

• [mind_finite] Decision to have the flag reflect the actual recursivity but keeping compatibility as much as possible.
• PR 15582: let's continue uniformizing the names
• https://github.com/coq/coq/pull/15527: would need more manpower to go beyond, but a good first step.