-
Notifications
You must be signed in to change notification settings - Fork 636
Coq Call 2020 11 04
- November 04th 2020, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- 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
-
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).
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.