Coq Call 2023 10 03

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

Topics

• ensuring Coq remains safe for async interruptions (Emilio, 15min)

  • see also https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Situation.20of.20async.20interruptions
  • https://github.com/coq/coq/pull/17638
  • https://github.com/coq/coq/issues/17760

  The problem is well-known, basically any code:

    try foo () with
    | _ -> false
  

  is wrong, as it will consider foo () to return false even when actually what happened is an async exception. This is a problem in practice. At some point I had a PR trying to make some progress on that issue, but likely not the right way https://github.com/coq/coq/pull/15937

• check on progress for completing the items in the roadmap (Théo, 5-10min)

• support for extruding uniform parameters (the standard failure with map not in a section, PR #17986) (Hugo, 30 mns but also depending on time available)

Roles

• Chairman: Nicolas Tabareau
• Secretary: ?

Notes

• Roadmap :
  • Primitive Projections: the plan is to remove the compatibility layer
  • LTac2 : the plan is to deprecate LTac, before that, better support for SSReflect is needed.
  • Retiring the STM: Gaetan Gilbert will do the code reviewing
• Emilio posted this comment OCaml upstream about trying to improve detection of suspicious exn try catch all: https://github.com/ocaml/ocaml/issues/12241#issuecomment-1745153446
• Guard Condition: agreement that the guard condition needs more theoretical justifications before going further. One possibility is to do a formal treatment in MetaCoq. One possibility is also to add a safe guard condition as default (recursive calls on direct subterms)