Minutes May 05 2021 - math-comp/math-comp GitHub Wiki

Cyril, Enrico, Quentin, Kazuhiko, Christian, Pierre, Enzo, Pierre-Yves, Laurent, Assia, Reynald

About the TODOs from the last meeting

  • document the MathComp practice (github workflow + API doc)
    • not to go in CONTRIBUTING.md
    • how to document the way MathComp is documented
      • in particular, difference between the API to be exposed to users and internal contents which ideally should be hidden
      • documentation about how to read the headers
        • document on the wiki?
        • make a short intro at the beginning of each header
    • videos planned to explain a recommended github workflow (based on nix but going beyond)
  • coqdoc features to be discussed today in the Coq call
    • Enrico to discuss about
      • how to attach meta-data in general
      • attach some form of documentation as the one we get from coqdoc
      • goal: generate some part of the header using commands written by us
        • inspired from the HB documentation for factories
    • Emilio also on a similar topic
  • list of meta-data we want from coqdev:
    • docstring to a general text
    • bib entry
    • alternative/literature names
    • alternative statement for Search (for example, for associative)
      • either based on unfold or manual statement
    • keywords
    • what is public? what is private?
    • module/file-level docstrings
  • concerns that too many attributes would clutter the source files
  • answer to concerns, e.g., on bigop: good practice to put doc in the header, not in the docstrings
  • remark: only the main theorems would have a long documentation
  • reminder: lemmas were not documented so far because too long and too fragile
  • Enrico: I think that for bigop we need text search. I mean I want to "exchange sum and prod", or "pull an item out of bigcup".

About triaging PRs

  • Triaging of PR to be done a need-to basis unless we have time

About ring tactics

  • Recorded demo of Kazuhiko Sakaguchi's ring tactic for MathComp