MInutes August 10 2022 - math-comp/math-comp GitHub Wiki

Participants: Cyril, Pierre, Reynald

• port to HB (#733, port of Analysis is in progress, last big thing seems to be the doc)
  • https://github.com/math-comp/math-comp/blob/hierarchy-builder/mathcomp/algebra/ssralg.v
    • faire apparaitre les structures (e.g., ringType)
    • [ringType of R for S] : HB cannot generate these notations but they are essentially made up with XYZ.clone
    • we need to document these notations
    • List of factories (including mixins)
      • would be better to delegate this to HB.howto and HB.about
      • just list the factories with a few comments but the list of parameters should be obtained using HB.about
    • remove constructors that start with a cap (e.g., UnitRingType, ComUnitRingMixin, FieldMixin)
  • shouldn't the doc be automatically generated?
  • TODO: make a tutorial about using HB.about and HB.howto
    • TODO: review the HB.howto PR
  • TODO: work on a template to have a good idea of what we want to generate
    • one file, say ssralg.v
  • TODO: HB_doc to generate coqdoc from HB.howto
    • as a shell script that modifies .v files?
• port the hierarchy of monoids in bigop.v as well as additive, multiplicative
  • additive, multiplicative will be useful for mathcomp-analysis