Coq Call 2021 04 07
- April 7th 2021, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
-
Renaming Coq, again. (...) happy!
-
Arthur: would like to plan discussion on hint databases, either today, or next call, or as private discussion, see the summary of my proposal at the end of https://github.com/coq/coq/issues/10559 .
- More work needed to determine which union operation we want to implement. TODO: gather with Pierre-Marie and Matthieu to refine this.
-
Arthur: would like to know if we're converging towards a final decision on support for "true" absolute paths for
Require. (See PR #12108, and PR #13992, and my suggestion a parameter to coqdep to specify desired behavior on missing files.) There has been a lengthy, fruitful discussion, maybe it is time to conclude on it.- preliminary proposals look fine, we need to be sure the implementation is "stable" with regards to FS contents
- main problem is duplication of code handling location of libs
- this is trying to be solved by PR https://github.com/coq/coq/pull/14059 cleans up and refactors loadpath/require handling. Once it's done we should be able to improve more easily (and economically)
coqdep - we can further coordinate on zulip
- upcoming CEP about deeper changes / improvements for the library model
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.