Coq Call 2020 11 13

• November 13rd 2020, 3pm-4pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Discussing CEP "packaging coq-native" for upcoming 8.13 https://github.com/coq/ceps/pull/48
• Ordering of notations by precision seems to work well and I'd be tempted to make a step (#12986)
• Request for comments on #12685, which can also be seen as a case study about local incremental improvements vs headless duck development strategy vs Greek calends development strategy vs how to use our time and energy at best

Notes

• CEP for coq-native:

  • uniform config
  • allow to really use native-compute on devs with dependencies, which is a pain today.
  • After CEP discussion, we agree to go this way for 8.13, and might switch to split packages in the future (but requires some work on coq and the opam side). Just merging the configure PR should be needed on the Coq side + CI changes.

• Ordering of notations. Everyone seems to be favorable to the change, which can be reverted easily is needed, let's try in the beta.

• #12685: net improvement: using parenthesis around any term does not change parsing semantics (scopes are properly propagated). Indeed this again calls for a clear path out of the primitive projections/projection notation difficulty.