Rocq Call 2026 11 03 - rocq-prover/rocq GitHub Wiki

• 16:00 Paris time (currently CET or UTC+1:00)
• https://rendez-vous.renater.fr/rocq-call

Topics

• [parsing] moving forward on the removal of the recovery mechanism of rocqpp (deprecation warning level-tolerance since 9.2) (Pierre, 20 min)
• https://github.com/rocq-prover/rfcs/pull/42 (Theorem := etc) (Gaëtan, 15min)
• https://github.com/rocq-prover/rocq/pull/22509 (printing of raw univs) (Gaëtan, 5min)
• which experiments are we doing with the LLMs? So that we don't do them twice. Were to synchronize, etc (Enrico, 10m)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Matthieu Sozeau
• Attending: Théo Zimmermann, Yann Leray, Pierre Roux, Enrico Tassi, Pierre-Marie Pédrot, Gaëtan Gilbert

Notes

• [parsing] lets move forward and see how much breaks. PMP proposes help.

• Theorem :=. ok with #[sealed] attribute. := always means defined/transparent by default, as for Definition. So #[sealed] Theorem := foo for a Qed'ed theorem. Discussion drifts about Parameter/Axiom. Do not support #[defined] Theorem foo : t. ... Qed.

• printing of raw univs: agreed with ":"

• LLM experiments:

  • updatable evar-maps (Rocqola?)
  • removing bind scope to types
  • functionalization of environment passing (PR by Gaëtan 21160)
  • environment extension for caching (PMP)

  Let's gather them here: https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/LLM.20.2F.20Experiments/with/637240889