Karl Palmskog (Sep 11 2021 at 23:01): Karl Palmskog (Sep 11 2021 at 23:01):After reading the preprint, I tried to convince the authors to qualify this negative assessment of the Coq opam archive, but to no avail (https://link.springer.com/article/10.1007/s10817-021-09604-0) [my emphasis]:
Coq has reached the usage size, where the central maintenance of libraries is no longer feasible. Instead, the Coq library has been factored into hundreds of repositories with a somewhat standardized build process. This allows distributed maintenance of the library. But it also means that not every repository always builds with the latest version of Coq. For example, when we ran our export in early 2019, only around 70 of around 250 repositories could be built, including the MathComp libraries (the situation has improved since then).
According to latest Coq opam bench, version 8.9.0 that they used for their export now has 450+ compatible "repositories" (they mean packages) as of September 2021.
What happened is that they performed the export just a few weeks after 8.9.0 was released, and did not consider any code in places such as Coq's CI. So Coq looks terrible in comparison to Isabelle and HOL Light.
Bas Spitters (Sep 12 2021 at 06:05):That's sloppy. They do say the situation has improved :grumpy:
Karl Palmskog (Sep 12 2021 at 08:03):well, the situation gets "bad" again at each release, and then "improves", it's just how Coq compatibility works, which I think anyone who now reads the paper will be misled about
Last updated: Dec 07 2023 at 18:01 UTC