This paper throws some shade at coq-opam-archive:
[W]hen 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).
I wonder if any packages in
extra-dev were tried?
some demands on devs and users from the paper (my emphasis):
Firstly, Coq must process its proofs in away that allows recovering mid-level proof terms— terms that includes [sic] more information than the users [sic] tactic script (e.g., all intermediate proof states and tactic invocations) but less than the low-level λ-terms. Secondly, proofs that are the result of search and other computations must be refactored to ensure they are not massively larger than necessary.
not to say this can't be construed as constructive criticism, but have they [Kolhase and Rabe] opened any issues or posted to Coq-club or similar with this feedback?
Kolhase and Rabe are pretty optimistic on Coq tooling here though (emphasis mine):
A major Coq-specific logistical challenge is given by the distributed library. While necessary due to the size of the user community, it brings a host of new maintenance problems such as different libraries depending on different versions of Coq. It is likely that this problem will not go away as new versions of Coq will be released faster than all existing content will be adapted. Therefore, new tools will be needed to manage the symptoms. However, this is a general issue facing the Coq community, and we expect good package and build managers to emerge in the near future, which can then be integrated with exports.
I don't think they asked for feedback. Try reaching out to them!
Did they use opam to build the packages or did they randomly tried make like that machine learning paper or do they mean that most packages are not compatible with the latest version of Coq? When looking at https://coq-bench.github.io/clean/Linux-x86_64-4.05.0-2.0.6/released/, one doesn't get the impression that there are a lot of packages that don't build...
Empirical science with no reproducible data... hard to refute ;-)
About opening issues, it is very "uncommon" thing according to my experience. It is damn obvious thing to do if you are used to open source, but I've seen so many talks of people consider tool X (Coq included) a black box the could not patch in any way. It is true that many, even academic, tools are like that. It just a bit sad that the one you work on is open but they don't know :-/
It is true that many, even academic, tools are like that
Right but this is definitely something that should change. Open science bordel!
Someone should contact them. They are generally reasonable and cooperative people.
OK, let me give some additional background. The work on Coq exporting was done with Claudio Sacerdoti Coen, so they are implicitly referring to his repository: https://gl.mathhub.info/Coqxml -- there one can see exactly what packages were used (for Coq 8.9)
Claudio did indeed open an issue in opam-coq-archive as part of his exporting work, to point out some missing dependencies: https://github.com/coq/opam-coq-archive/issues/593 -- I think these are all fixed now.
nevertheless, I think Kolhase and Rabe could have worded the negatives about Coq differently in this "export overview" paper, especially since the only interaction w.r.t. the export work with the Coq community/devs was (seemingly) Claudio's issue. And that some software "must" do something is overly strong in this context (IMO).
looked into Claudio's paper a bit more. My understanding is that Claudio finished the plugin and did the export for Coq 8.9 very shortly after 8.9.0 was released:
At the time of writing of this paper, there are only 49 opam packages that compile with the recently released version 8.9.0 of Coq.
Even going forward, I think we can never ensure package compatibility for a majority of packages in less than a few weeks after a major version release.
@Karl Palmskog My point was simple, if one finds a bug in a paper, it's considered good form to contact the authors so they can fix the bug.
I sent a complaint by email to the authors, I guess we'll see what happens. Bas, I put you in bcc so you can see how it turned out.
if they respond constructively, I'll follow up with them about the Coq dev feedback, otherwise it all goes to
had a pretty constructive discussion with Florian Rabe via email. The conclusion is along the lines of: (1) if they re-do the Coq export via OPAM, they will coordinate with us to get maximum number of Coq projects, and (2) it may be possible to integrate optional OMDoc export into Coq's CI, which is probably the ideal, but this will require developer commitment/time (e.g., Dedukti/MKM funding)
As I hoped a constructive outcome!
Last updated: Dec 01 2023 at 06:01 UTC