Minutes October 7 2020 - math-comp/math-comp GitHub Wiki

Participants: Christian, Maxime, Kazuhiko, Enrico, Reynald, Cyril.

• Ok to remove https://github.com/math-comp/math-comp/wiki/Publications from the wiki? Contents supereded by https://math-comp.github.io/papers.html which is the only page that points to it afaik.

  • Cyril already emptied the wiki page from its contents and kept only the link to the website.
  • Reynald will remove the link back to the wiki.

• This PR redefines the class_of records as primitive records except for morphisms and finGroupType, and also removes the xclass idiom by following #462 (comment) by @ggonthier.

  • Summary of the problem (unconvertible coercion paths).
  • is there an attribute, rather than Set Primitive Records and Unset Primitive Records?
    • we have to check from which version of Coq this exists, the answer is no: we have to stay with Set, Unset. Opened an issue on Coq/issues.
  • another point was the efficiency, how is it?
    • It's supposed to subsume the xclass idiom.
    • Not completely obvious.
    • Kazuhiko's experiment shows a 6% improvement (but the bench was run on a laptop).
  • It would be nice to have a benchmark infrastructure.
  • let's merge, after annotating the test with a comment explaining which tests used to work, and which test work thanks to the PR.
  • We will be dropping support for 8.7 and 8.8. The INSTALL.md is mentioning 8.8.0 we should update or abstract (x.y.z)