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