Minutes March 09 2022 - math-comp/math-comp GitHub Wiki

  • Participants: Reynald, Assia, Christian, Cyril, Kazuhiko, Yves, Laurent, Pierre

  • discussion about migration to coq-community (cont'd)

    • discussion on four-colour move:
      • Yves must file an issue to coq-community
      • Cyril provided this link
      • Yves does not have rights, but will warn an owner of the math-comp organization so that the transfer is initiated from the math-comp side git repository.
    • What's next?
      • make a list of the next project to transfer?
      • let's wait for four-colour
    • how to search for mathcomp project in coq-community?
      • use tags in "Most used topics" on the github site
      • see the list of projects on http://coq-community.org
      • is a mathcomp tag the right tag?
        • we maybe do not want to use coq-community to improve visibility of MathComp
        • the mathcomp tag is for things that depend on MathComp
        • we maybe want to have a curator for the list of MathComp projects
    • Is the final step to make the mathcomp organization disappear?
      • original goals:
        1. use the support for coq-community (this is clear)
        2. improve the visibility (this is less clear)
      • every Coq code should eventually move to coq-community?
      • there should be a way to indicate that a package in coq-community requires special care when it depends on MathComp
        • simply put this information in the readme?
        • have the MathComp icon on the coq-community website to identify MathComp project?

  • discussion about reverse coercions (cont'd)

    • the goal is to get rid of phantoms so that we do not have to write [the ringType of ...]
    • feature request by Arthur and Cyril
    • going backward in a coercion is like creating an instance using canonical structures
    • there do not seem to be any complexity issue, as reverse coercions do the same things as phantom types
    • demo with poly.v
      • removing the phantom type of poly_of
      • discussing the use of a notation to recover printing
      • some people would like coercions to be not necessarily implicit, right now it is not possible to de/activate selectively coercions
      • similarly, it is not obvious how to name notations to display/hide them selectively