Karl Palmskog (Jun 13 2020 at 10:55): Karl Palmskog (Jun 13 2020 at 10:55):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 inextra-dev were tried?
Karl Palmskog (Jun 13 2020 at 11:01):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.
Karl Palmskog (Jun 13 2020 at 11:05):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?
Karl Palmskog (Jun 13 2020 at 12:16):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.
Bas Spitters (Jun 13 2020 at 13:02):I don't think they asked for feedback. Try reaching out to them!
Théo Zimmermann (Jun 13 2020 at 13:44):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...
Enrico Tassi (Jun 13 2020 at 13:48):Empirical science with no reproducible data... hard to refute ;-)
Enrico Tassi (Jun 13 2020 at 13:54):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 :-/
Théo Zimmermann (Jun 13 2020 at 13:56):It is true that many, even academic, tools are like that
Right but this is definitely something that should change. Open science bordel!
Bas Spitters (Jun 13 2020 at 15:01):Someone should contact them. They are generally reasonable and cooperative people.
Karl Palmskog (Jun 13 2020 at 15:03):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)
Karl Palmskog (Jun 13 2020 at 15:05):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.
Karl Palmskog (Jun 13 2020 at 15:10):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).
Karl Palmskog (Jun 13 2020 at 15:20):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.
Bas Spitters (Jun 13 2020 at 19:16):@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.
Karl Palmskog (Jun 14 2020 at 18:40):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.
Karl Palmskog (Jun 14 2020 at 19:04):if they respond constructively, I'll follow up with them about the Coq dev feedback, otherwise it all goes to /dev/null
Karl Palmskog (Jun 16 2020 at 11:00):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)
Bas Spitters (Jun 16 2020 at 11:15):As I hoped a constructive outcome!
Last updated: Sep 15 2024 at 13:02 UTC