Coq Call 2023 07 11

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

Topics

• Reducing the STM (Emilio)
  • goal: reduce the surface Stm API, see what we can deprecate / remove, close bugs
  • vio2vo: is that used? Due to #4123 not likely
  • vio files: replaced in practice by vos?
  • query workers?
  • xml protocol: goals hints and evars are unused in coqide
  • stm: some parts of the error recovery code of 8.6 didn't work
  • classification: can we use the vernac_interp type to derive it?
  • coqc vs simple compiler?
• Issues pertaining to DMs (Emilio)
  • goal: quite a few wishlists about IDE / build system integration are open in Coq repos, however work happens outside Coq repos
  • examples:
    • https://github.com/coq/coq/issues/16363
    • https://github.com/coq/coq/issues/16273
    • https://github.com/coq/coq/issues/15763
    • https://github.com/coq/coq/issues/14110
  • What to do with them?
• Adding primitives to better control (i.e., force) reduction (Rodolphe, BedRock Systems)
  • This is something we discussed and came up with with PMP a while ago.
  • We have a draft PR, and would like feedback on whether something like this could eventually get in.

Roles

• Chairman: Théo
• Secretary: Hugo, then Emilio

Notes

• Reducing the STM (Emilio)

  • see list of features above questioned by Emilio
  • Emilio suggests some lightening and refactoring of the STM
  • Théo proposes that Emilio opens PR on which discussions can happen

• Issues pertaining to DMs (Emilio)

  • Théo suggests that it is not necessary that a solution to the various issues are given within the Coq repository
  • Emilio proposes to have specific discussions in September

• New reduction primitives:

  [Presentation by Rodolphe]:

  • Adding new primitives to Coq's kernel to have better control of reduction in proof by reflection.
  • Use in IRIS, problems with forcing reduction
  • An IRIS proposition is reified into a datatype
  • During Kernel type-checking there is no way to force reduction under binders
  • At QED time that's needed, likely to gain a factor of 2x
  • New primitive: let_lazy, like let, but body is typecheck with reduced version
  • But you need a way to stop that reduction at certain points
  • Usually the leaves of the reified Ast, which are "private"
  • Main question: how likely this gets in?
  • Pierre-Marie was optimistic.
  • Blocking primitives implemented but not pushed
  • Proposal still not enough for the IRIS use case

  [Discussion]:

  • Q: How does this compare to math-comp's unlock / lock?
  • A: AFAWCT math-comp cannot reduce under binders
  • Some discussion about how that would interact with existing system in math-comp, also more validation and documentation is needed.
  • Some more discussion about how the system does work
  • Q: Who to get in touch with to continue work on this?
  • A : In addition to Coq devs, G. Gonthier and Assia / Cyril may be good reviewers.
  • Q: Would it work to have a constructor that forces the term?
  • A: No because still the let is "CBN"
  • Q: current PR targets mainly non-users (internal)
  • A: Yes, for now (more discussion as to see more visible applications)

  [Conclusion]:

  • We agree this in an important feature to have
  • Next step: push implementation of blocking primitives, more testing / validation
  • Next step: discussion / review with other experts (mainly math-comp) => understand the relationship of IRIS and math-comp needs
  • Once it is ready we expect it to land in Coq