Coq Call 2021 04 07 - coq/coq GitHub Wiki

• April 7th 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• 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