Coq Call 2025 01 14 - rocq-prover/rocq GitHub Wiki

• 2025-01-14, 4pm UTC+2 (Paris time zone offset)
• https://rendez-vous.renater.fr/coq-call

Topics

• adding dependency on yojson (for https://github.com/coq/coq/pull/18816, Gaëtan, 15min)
  • see also https://github.com/coq/coq/issues/17169
• getting rid of dunestrap (c.f., somewhat off topic discussion starting at https://github.com/coq/coq/pull/19975#issuecomment-2587644297, Pierre, 20 min)
• do we need a 8.20.1 release (Pierre, 10 min)

Roles

• Chairman: Pierre-Marie Pédrot
• Secretary: Matthieu Sozeau
• Audience: T. Zimmermann, E. Tassi, E. J. G. Arias, A. Erbsen, P.M. Pédrot, P. Roux, G. Gilbert, M. Sozeau, Y. Bertot

Notes

• Dep on yojson. Not decided yet, PMP and Gaëtan have to agree on a solution. A rocq-dev-tools package "option" like native could work to avoid rocq-runtime depending on yojson unconditionally (PMP fears difficulties with adding a new dep).
• Ok to move dunestrap to a backup method promotve back the disabled dune files. Remove the +async jobs testing only corelib now
• 8.20.1, Yes. But close milestone and stop backporting right now. There will be no 8.20.2