Minutes October 5 2022 - math-comp/math-comp GitHub Wiki

  • Licencing issue (cf zulip). In order to get on gitlab CI free plan we need an OSI-approved and GPL-compatible license which is not the case of CeCILL-B. We should change licence or forget about free plans, but a nontrivial decision is required.

    • we are considering moving MathComp to an MIT license and will contact Inria services to that aim

  • Enrico: demonstration about automatically generated documentation for the HB port of MathComp

    • example: generation of the ssralg.v documentation using HB.about
      1. annotation written at the right within the header
      2. #[format="coqdoc"] HB.doc command after the header
      3. header fixed with automatically generated information
    • what to put in the header?
    • the part about definitions and notations should stay hand-written
    • caution: automatically generated documentation is likely to contain duplicates if not careful
    • generate graphical information for inheritance relation? how?
    • we still plan to go through coqdoc afterwards
    • the current solution should be integrated in the CI