Coq Call 2020 02 26

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

Topics

[note: order of discussion to be decided at the beginning of the call]

• Avoiding exceptions-as-control in the codebase? _exn prefix for functions that raise?

• copyright headers

• Refreshing contents of the few ML files mentioning credits https://github.com/coq/coq/pull/7198

• Garbage-collection of PRs?

• Plans for primitive projections? See for instance a basis for discussion here.

• CEP 42, and in particular the unsettled and debated question of the default transparency.

• CEP 41 status

• How to organize ourselves to clarify and communicate on our objectives (HH: 10 minutes to start a discussion to be continued offline)?

You are welcome to lead a discussion on:

• needs: discussion https://github.com/coq/coq/labels/needs%3A%20discussion

Notes

• copyright headers

  Agreement with removing the dates from each file

• Plans for primitive projections? See for instance a basis for discussion here.

  Discussion took a while:

  • convergence on removing the compatibility layer.
  • especially introducing a ProjRef in extended_glob_ref (outside the kernel)
  • Idea of syntax for projections: can we reuse foo.(bar x a) currently used for postfix applications.
  • Removing special support for compatibility constants.
  • Then the question of a similar treatment for positives.

  TODO: organize a specific call on the subject next week.

• CEP 42, and in particular the unsettled and debated question of the default transparency.

  Questions of transparency control for Theorem and Definition.

  Transparency controlled by attributes known at the start of a command. General agreement on the design. Problem of confusion with qed/defined/opaque/transparent. PMP mentions the third! dimension of private/public/sealed in modules.

• CEP 41 status

  Hugo has an initial implementation -> send link to Maxime

Postponed

• Avoiding exceptions-as-control in the codebase? _exn prefix for functions that raise?

• Garbage-collection of PRs?

• How to organize ourselves to clarify and communicate on our objectives (HH: 10 minutes to start a discussion to be continued offline)?

• Refreshing contents of the few ML files mentioning credits https://github.com/coq/coq/pull/7198