Minutes June 16 2020 - math-comp/math-comp GitHub Wiki

  • About the issues in order https://coq.zulipchat.com/#narrow/stream/237665-math-comp-devs/topic/hierarchy.2Eml

    • PY had problems extending order's hierarchy, KS tool has some issues and a workaround

      • you can run it without compiling all.v but you have to manually Import (transitively)
      • you can at least use the all_something to "factor" some imports

    • CC wonders if we could use Export in some .v files to transitively close automatically (if you Import A that Exports B, then you Import B automagically)

    • the Exports modules are always Exported at the end of the files

    • AM there was a bug w.r.t. Export and coercions (exporting twice the same module with a coercion was failing)

    • conclusion: we should try this

    • PY: order is very complex, hard to do by hand, let's hope Hierarchy Builder comes soon

    • PY: CS indexed on the type, not the order relation, but you have many (on the same type) and today you have to alias the type.

      • CC: we should have both. Roadmap:
        1. HB only indexes on types for now
        2. Next morphisms (index on functions)
        3. Next mixins on different indexes.
      • ET: we should organize a meeting where we try to port order to HB

  • About OPAM naming policy

    • we could not find a rule for cutting it
    • maybe should be in sync with the GH organization

  • About packaging

    • google points to Guillaume Claret blog which is outdated
    • no single source of info/scripts
    • ET: I would recommend coq-community
      • but does not support choosing a prefix other than coq- for the name of the package
    • CC: improve nix template for coq-community, the "packager" tool should be used/advertised there
    • The work should go into coq-community, not MC specific