Coq Call 2021 02 17

• February 17th, 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• vernacular commands on proof variables: use cases (MathComp developers)
  • canonical instances (not frequent, but blocking when it occurs). examples:
    • fieldext.irredp_FAdjoin (fieldExtType instance inside a proof and rmorphism instance as well https://github.com/math-comp/math-comp/blob/fb9fb240fe7f6a99035a4db23942cb774458d7a3/mathcomp/field/fieldext.v#L1510)
    • mathcomp/Abel is full of that (e.g. https://github.com/math-comp/Abel/blob/e6d97debf7ec1881500af59c880e48c9a75fc330/theories/xmathcomp/various.v#L878-L884 https://github.com/math-comp/Abel/blob/e6d97debf7ec1881500af59c880e48c9a75fc330/theories/abel.v#L795-L797 and even inside a subgoal https://github.com/math-comp/Abel/blob/e6d97debf7ec1881500af59c880e48c9a75fc330/theories/abel.v#L698-L706)
    • closed_field.countable_algebraic_closure (https://github.com/math-comp/math-comp/blob/fb9fb240fe7f6a99035a4db23942cb774458d7a3/mathcomp/field/closed_field.v#L853-L856)
  • managment of implicits in local definitions/abbrev/cuts (frequent, never blocking but painful)
    • we often need to pad local hypothesis with _ even when the first arguments are inferrable
    • we sometimes change the implicit status of global constants, but it should not survive the end of the proof.
• splitting CoqIDE
• Dune update:
  • "Switch to a Dune-based build system" https://github.com/coq/coq/pull/8729
  • "Enable Native Compilation" https://github.com/coq/coq/pull/12974
  • "Split stdlib" https://github.com/coq/coq/pull/12567
  • "Use Dune for OCaml" https://github.com/coq/coq/pull/13617
  • "Port the test suite to Dune" https://github.com/coq/coq/pull/13364

Notes

Enrico is taking them

• vernac on PV:

  • storing data in the evar map (inside evar_info) can cover CS + implicits. Glob_term does not carry implicits in type annotations.
  • a limited form of notation, eg. a new interpretation for an existing infix, then it may be feasible, but the general case seems a nightmare
  • W.G. in May to talk about details with PMP

• splitting CoqIDE:

  • pros:
    • simplify Coq repo (build)
    • decouple releases, issues
    • ease to contribute to CoqIDE (small source code)
  • cons:
    • to have a UI to play with Coq, one has to do make ci-coqide
    • harder to test your changes to Coq by running Coqide
  • PMP does not want coqidetop to go
  • Hugo finds it easier if it is inside
  • Guillaume and Enrico don't see the advantage
  • Theo: the maintainers have the last word, maybe the split can help the community (good experience with vscoq)

• Dune:

  • Next time