Agenda of the May 22nd 2019 documentation meeting 9h30 to 12h30 - math-comp/math-comp GitHub Wiki

Participants: Georges, Reynald, Marie, Assia, Enrico, Cyril.

Installation troubleshooting

Troubleshooting opam

  • Tracking updates of opam: explain how to update and upgrade
  • Recall what problem opam solves: find the right versions of ocaml and coq.
  • Having modular OPAM instructions with pointers to previous OPAM instructions.

Alternative nix

  • more stable and flexible.
  • Cyril will use Assia as a Guinea Pig

Coq package management

  • raise the issue at the User and Developper Coq meeting

Visibility on Internet

Browsing the web

  • "Mathematical Componenets" : site mcb -> put the link to lib earlier in the page
  • "Ssreflect" :
    • stackover
    • ssreflect coq doc -> put a reference to mathcomp early

Documenting the library

Typical questions (by Assia)

  • What exists? E.g. elementary number theory (scattered over ssrnat, div, prime). How to find which files are relevant?
  • Notations? Part of the information is in the headers, but this may not be enough
  • How do I make some types of proof steps? e.g. natural recursion, case analysis, ...
  • where to find examples of use? (by Marie)
  • Enrico: search "number theory site:math-comp.github.io" or "trichotomy site:math-comp.github.io".
  • Assia: for trichotomy no pointer from the code to the documentation on how to use it.
  • Marie: How to use the hierarchy of morphisms and sub-structures? (Examples)

Maxime was afraid of dis-synchronization between this and the code, who and how to maintain.

Suggestions

  • Marie:
    • have examples of basic theorems in using each libraries
    • two levels:
      • instruction by instructions first
      • combining to go faster
    • explain in a few sentences which mathematical/CS intuitions do not apply to mathcomp
    • have a link to the winter schools. (e.g. "here is what you can do with matrices")
  • Assia: have a showcase.
  • Cyril: put keywords in comments of lemma, to help search engines and to point to appropriate documentation.
  • Reynald:
    • reference to papers using theorems
    • Gather winter school scripts in a repo and put them in the CI

Actions

TBD on July 1st, 2019