Rocq Call 2025 03 25 - rocq-prover/rocq GitHub Wiki

• 2025-03-11, 4pm UTC+1 (Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• planning for dune using rocq (Gaëtan)
• https://github.com/coq/coq/pull/20379 (registered refs in constr syntax, Gaëtan, 15min)
• _RocqProject? (Gaëtan, if there is time left)

Roles

• Chairman: Matthieu Sozeau
• Secretary: Pierre-Marie Pédrot
• Attending: Pierre Roux, Rodoplhe Lepigre, Janno, Théo Zimmermann, Guillaume Melquiond

Notes

• Renaming: a workaround was found to rename the organization. There are still some expected problems with the repository renaming, Matthieu has to run a script before. The Coq Zulip is expected to be renamed imminently. Some breakage expected with bots / webhooks / docker but we'll have to wait for the dust to settle down.

• Dune: annoying situation with Coq dune rules having to live upstream, we have to live on the bleeding edge if we want to add new build features. It doesn't seem to be a problem with the OCaml compiler though. Dunestrap works fine but it doesn't play well with composed builds and it thus means maintaining two compilation paths. Janno mentions weird corner cases with the current setting. There is an API for dynamic plugin loading in Dune it seems. Dune doesn't know how to handle timing info, this is critical for the bench infrastructure but looks hard to achieve. We should investigate the plugin API to move back the build rules to the Rocq side. Task force: PMP, Rodolphe?

• Reference quotation: we want this. As for the parsing, should we use lib:, or some more complex grammar like lib:()? What prefix do we use? Let's start a poll on Zulip.

• RocqProject: editors should be able to support both names for project files for the foreseeable future.