Attending: Yves Bertot, Alessandro Bruni, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Théo Stotskopf, Enrico Tassi, Quentin Vermande

• quick announce: nasty filename (absence of) conflict now fixed in master: https://github.com/rocq-prover/rocq/pull/20601 Nix and OPAM should now behave the same in case of duplicated file

• Large scale documentation of mathcomp: phase 1 request for annotations

  • three projects: "translate" proof scripts from Lean to Rocq able to translate some proof terms (success rate currently around 30%)

  • Crrrocq: interaction between LLM and proof assistants

  • LM4Docq: generate documentation using LLMs

    • add docstrings to all element sof the mathcomp library
    • exploit them in natural language queries
    • need some work to audit the currently generated docstrings https://github.com/LLM4Rocq/LLM4Docq
    • where are the docstrings stored: currently in a separate database, ultimately we want them in the file
    • Théo probably attending Rocq'n'share
    • need to schedule something together: Rocq'n'share, sharing days? announce it on mathcomp dev zulip channel

• Clarify the authorship of multinomials (before September if possible) https://github.com/math-comp/multinomials/issues/59

  Discuss it with Pierre-Yves

• https://github.com/math-comp/math-comp/wiki still reads "Next Sharing day: 2025-05-28" did we decide something?

  Let's go for July 9th. Kazuhiko or Quentin will announce it.

• Export all_boot in all_order,... ? (c.f. https://rocq-prover.zulipchat.com/#narrow/channel/237664-math-comp-users/topic/Error.20with.20syntax.20levels.20all_fingroup.20vs.20all_algebra/with/523275229 )

  Needs more discussion, for instance at Rocq'n'share

• chair for next meeting (July 9th): Pierre

• PR triage

  • https://github.com/math-comp/math-comp/pull/1438
    • new heuristic for pattern selection skipping implicit arguments
    • sometime breaks with phantom, workaround with multiple implicits
    • selecting wrong instance can be very bad performancewise (not a new problem but needs to be careful)
    • discuss design in Paris (end of June)
    • complete overlays during next sharing days (July 9th)