Minutes April 05 2023 - math-comp/math-comp GitHub Wiki

Participants: Julien, Pierre, Reynald, Thomas, Yves

conclude about https://github.com/math-comp/math-comp/pull/934 (renaming long suffixes)

  • the i in ltriX2l means "interior"
  • the e in ltreXn2l means "exterior"
  • TODO: put underscores in front of i and e
  • rule: don't put _ when the suffix starts with a cap
  • the documentation mentions sp/sn but they are not used that much (exception: ltr_spaddl, etc.)
    • TODO: update the documentation?
  • TODO: modify the contributing guidelines
  • maxrnMr -> maxr_nMr
  • what about div -> MV?
    • makes for difficult to read names (MVlM)
    • search for M would also display MV
      • just add - "V" to the search
    • by the way, we have B instead of ND because of nat
    • let us keep div
  • ler_pdivl_mulr -> ler_pdivl_Mr or ler_pdivlMr?
    • the 2nd _ would mean "equal"
    • however, we do not want to change ler_subl_addl -> lerBlDl
    • rule: put _ in front of small prefixes but not suffixes

merge https://github.com/math-comp/math-comp/pull/790 ?

  • NB: name -> binder
  • TODO(rei): merge

drop support for 8.13 and 8.14? (c.f. https://github.com/math-comp/math-comp/pull/980 )

  • notation that does not work with 8.13 et 8.14
  • drop to support 0%O and 1%O (even though they are temporary)
  • we can drop because we sill support three versions
  • where is the statement that we support three versions?
    • no need to be clear about that

reminder about the poll for the doc spring sprint:

https://evento.renater.fr/survey/mathcomp-2-documentation-sprint-ck97yi5r

  • TODO: advertise again the sprint
  • we took a quick look at the tentative doc for eqtype:
  • question: how to document notations such as [eqType of _]?
    • because they are going to look alike across many files and there may be many of them in ssralg and order
  • we may need to add the topic of documenting HB to the program of the sprint
    • [the A of B] is to recover an instance
      • Remark(enrico): may become less and less used, since Coq 8.16 if you write nat where an eqType is expected, the elaborator will generate nat_eqType for you, no need to wrap nat into [the eqType of ...]
      • (the elaborator uses the solution to the unification problem triggered by the fancy notation with Phantom arguments, in some sense it triggers the same unification). These are the "reverse coercions" thing.
    • clone reconstructs a canonical instance using a constructor e.g. Equality.clone nat is Equality.Pack nat nat_eqClass, Equality.clone T will eta-expand and hence clone should be used with caution.
    • [eqType of _] are string notations for clone (historically it was not always eta-expanding, bug only in some very specific cases)
    • copy copies the class but might change the key, e.g. Equality.copy T nat is an Equality class on T which is definitely equal to that of nat.
    • S.on T is an abbreviation of S.copy T T, i.e. it tries to infer a class instance of S on T (either because it already exists on T or because it can be obtained by unfolding) a typical usecase is for aliases. Example, if I create an alias nat' := nat and want to copy everything up to Choice I can do HB.instance Definition _ := Choice.on nat' and then I can create diverging instances from nat.
    • NB: don't document if it is not supposed to last (e.g., .on)
  • TODO: pierre and reynald to meet next week to make progress