Minutes October 10 18 - math-comp/math-comp GitHub Wiki

Participants: Cyril, Kazuhiko, Quentin, Reynald

observation:

there are several "mathcomp complements" files and directories in the mathcomp hierarchy, e.g.:

• Coq-Combi: https://github.com/math-comp/Coq-Combi/tree/master/theories/SSRcomplements
• cad: https://github.com/math-comp/cad/blob/master/extra_ssr.v
• newtonsums: https://github.com/math-comp/newtonsums/blob/master/auxresults.v
• multinomials: https://github.com/math-comp/multinomials/blob/master/src/ssrcomplements.v
• CoqEAL: https://github.com/coq-community/coqeal/blob/master/theory/ssrcomplements.v

it would be nice to collect useful things from them but how to do that efficiently?

• calls for contributions to particular files?
  • e.g., "please send your PR contributions to xyz.v"
• we could do it ourselves but this is not reasonable
  • NB: some of us have right access to every repo in the mathcomp organization
• this is a job for an AI?
  • how to find name? https://github.com/EngineeringSoftware/roosterize !
  • in which file where to put the lemmas?
  • NB: not to find proofs
  • NB: GPT4 seems very good at producing Coq statements
• we should apply for resource at Inria
  • TODO: Cyril to write the application but needs help to review it
• should we make this a regular topic of this meeting?
  • yes

chat about documentation:

• we should insert a coqdoc topic in the roadmap https://github.com/coq/ceps
• alectryon is used to write tutorials (e.g., for coq-elpi: https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_HOAS.html)
• mv files from https://github.com/ejgallego/coq-lsp
• we should have docstrings in Coq to attach doc to global identifiers
  • there is a poll about docstrings https://framadate.org/kjVAVOxyCVDCDYxb
• https://github.com/ejgallego/udoc
• https://github.com/coq-community/proviola

PR triaging in preparation for releases.

• https://github.com/math-comp/math-comp/pull/1094 good to go
• https://github.com/math-comp/math-comp/pull/1062 merged
• https://github.com/math-comp/math-comp/pull/986 needs to be rebased
• https://github.com/math-comp/math-comp/pull/931 Cyril to ping the authors