Coq Call 2020 06 24
- June 24th 2020, 4pm-5pm Paris Time
- The link to the visio room: https://rdv2.rendez-vous.renater.fr/coq-call
-
What is the plan for Ltac2 to become a drop in replacement of Ltac1 (for new projects)? (Théo)
See Jason's assessment at https://github.com/coq/coq/pull/12085#issuecomment-647771222 and Andrew's complaint about its documentation at https://github.com/coq/coq/issues/12549
-
Adding back fiat-crypto-legacy (Emilio) https://github.com/coq/coq/pull/12554
-
Upgrading Jenkins/coq-bench (the qualif server seems to be completely borked, see this issue I reported on Jenkins; if we can reset the installed version of Jenkins to the one on production, that'd be great, but the web interface doesn't seem to allow downgrading the qualif server) (Jason)
-
Integrating coq-bench with coqbot (https://github.com/coq/coq-bench/pull/85) (What's the blocker?) (Jason)
-
A few questions on problems with the current Hint implementation [Emilio]
-
The various kinds of syntax for global references and what to call them (https://github.com/coq/coq/pull/12568#issuecomment-648298048) (Jason)
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq 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.