Coq Call 2023 05 16 - coq/coq GitHub Wiki

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

Topics

• CI for mathcomp-1 -> mathcomp-2 transition (Enrico, 20 minutes)
• printing of reverse coercions #17484 (Pierre, 20 minutes)

Roles

• Chairman: Nicolas Tabareau
• Secretary:

Notes

MC1 to MC2

• most devs are already ported to MC2, except jasmin but that shouldn't be a blocker
• main problem is that MC2 is too memory heavy for our machines (5GB peak)
• a Nix-based cache was mentioned but it probably won't work

Result: we put MC2 in CI separately from MC1 and see what happens

Reverse printing

• don't modify the kernel to support upper layers
• problem with multi-sorting?

Result: PR needs approval with some justification for outsiders and then can be merged