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

Notes