Coq Call 2020 11 04

• November 04th 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Test relevance before structural equality https://github.com/coq/coq/pull/12205
• Lifting the restrictions on algebraic universes (Matthieu, 15min max)
• Which build system for 8.13? Only one answer allowed.
• Last things to do for the 8.12.1 release
• Performing native compilation a posteriori from compiled vo files https://github.com/coq/coq/pull/13287

Notes

• 8.13 with dune only ? PR incoming: https://github.com/coq/coq/pull/13193 native compute incoming.

  Some worries with being on the bleeding edge and issues with the cache. Emilio explained that some more changes are needed in Coq to support the cache correctly and other features. Dune 3 will provide in the future a way to modify the build rules from inside Coq Théo mentions a good objective would be to remove the Makefiles for ML code after the 8.13 freeze, until then, it's good to keep the two build systems for now (thinking about packagers in particular).

• The team asks for a more lenient/flexible view on PRs that perform refactorings. They are work in progress but still an improvement and should be treated as such, not asking for the "perfect" solution. Authors should on the other hand strive to separate refactorings from issues/bug fixing.

• 8.12.1 status

  • Dune PR to be merged
  • Issue with template https://github.com/coq/coq/issues/13300 but has a workaround