Coq Call 2020 02 12

• February 12th 2020, 4pm-5pm Paris Time
• How to join the call
• Add your topics below

Topics

[note: the order of the list doesn't imply order of discussion]

• date for CUDW 2020 ?
• https://github.com/coq/coq/pull/11380 (Deprecate aliases for exception re-raising)
• https://github.com/coq/coq/pull/10951 (where to place the tactics lib)
• OCaml warning 40 https://github.com/coq/coq/pull/11485
• stdlib2 plans/status
• fine-grained Import/Export
• replacing explicitations by a label system
• what to do with UIP PR?
• copyright headers

Notes

// @prefix coq call 12-02-2020 // @description

[note: the order of the list doesn't imply order of discussion]

• date for CUDW 2020

  22 to 26 June 2020.

• what to do with UIP PR?

  => make it available with a flag and warn users about loss of termination for now.

• https://github.com/coq/coq/pull/11380 (Deprecate aliases for exception re-raising)

  Merged

• https://github.com/coq/coq/pull/10951 (where to place the tactics lib)

  => rather move tactics to a library after vernac (moving schemes). We should also move back tactics that are in plugins/ltac back to this library.

• OCaml warning 40 https://github.com/coq/coq/pull/11485

  => deficiency of OCaml. Tooling could help locally by having your own compilation mode with e.g. warning 40 deactivated.

• stdlib2 plans/status

  • sources: taking as basis of
    • mathcomp
    • coqstdpp
    • stdlib1

  Maxime mentions that we cannot satisfy all users at once (contradicting requirements). It is good to know the users requirements but better start opening up discussion from a starting proposal.

  We need more work on basic feature (e.g. primitive projections) taking GlobRef vs applicable glob ref.

  • TODO gather a group to talk on primitive projections and stdlib 2 in more details.

• fine-grained Import/Export

• Vincent is a priori not working on it now
• Short-term plans:
  • A prelude for stdlib2 so that stdlib1 can be rebased on it.
  • Different organisation in stdlib2 requires fine-grained export/import lists. 2 problems:
    • Definitions imported/exported with associated metadata (scopes, arguments)
    • How to implement it with the current libobject: let each object get a request for import depending on what was asked to be imported? Seems doable according to Maxime.

• replacing explicitations by a label system

  Is it realistic? This might break alpha-equivalence in the kernel. PMP points to deficiencies in the label system of OCaml we should not bring. mangle names reveals issues with explicitation.

  The main idea is to preserve what Arguments declaration imposes to make naming more stable. Seems to be shared by Hugo and Maxime, working on the subject currently.

• copyright headers: postponed