Coq Call 2023 05 09 - coq/coq GitHub Wiki

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

Topics

• Early feedback about deterministic timeouts and memory limits: https://github.com/coq/coq/pull/17266 (gadmm & Gaëtan, 15 min)
• What to do about https://github.com/coq/coq/pull/17432 (reinfer univ inconsistency when explanation is missing) (Gaëtan, 15min)
• bikeshed syntax for https://github.com/coq/coq/pull/17509 (rewrite_strat fixpoint operator) (Gaëtan, 15min)

Roles

• Chairman: Ali Caglayan
• Secretary: PMP

Notes

Deterministic timeouts

• GADMM: this is pending on support in OCaml 5.0 and requires an OCaml version higher than the Coq lower bound.
• GADMM: Is it solving the Coq reliability issue? (Unclear).
• PMP: should be put as an optional dependency
• EJGA: this seems to make asynchronous exceptions possible, so nice to polish
• PMP: maybe worth staging into a plugin

Result: Status quo, let's wait to see whether OCaml 5.0 makes the implementation of this library possible.

What to do with PR17432

• GG: performance concerns.
• AC: maybe guard with a flag, produce a different error and cleanly document the behaviour
• Discussion about annotating NotConvertible with the missing constraints instead

Result: Status quo, let's discuss more in the PR.

Bikeshed PR17509

• GG: various problems with parsing
• PMP: don't introduce a different syntax for bound fix variables and do the check at runtime instead
• Discussion about an Ltac2 API
• AC: well-parenthesize the fix node with end