Karl Palmskog (Oct 21 2021 at 13:14): Karl Palmskog (Oct 21 2021 at 13:14):I want to remind about the following quote from the paper on exporting proof assistant libraries that was recently retweeted by @coqlang (undeservedly so, IMO):
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 [packages] could be built, including the MathComp libraries (the situation has improved since then).
They did their export just after the release of 8.9.0, and it made us look terrible. 8.9.0 now has 400+ compatible packages.
As I describe here I tried to get the authors to include a hint about why they got so few packages.
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:25):Karl Palmskog said:
I want to remind about the following quote from the paper on exporting proof assistant libraries that was recently retweeted by
@coqlang(undeservedly so, IMO):
As the author of the retweet I agree with your evaluation of the paper, but I try to keep CoqLang neutral in the sense of not doing any reviews there :)
But you should answer to that tweet with your remark :D
Karl Palmskog (Oct 21 2021 at 13:30):can I send an angry handwritten letter to Irif that you scan and publish verbatim on @coqlang?
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:37):Karl Palmskog said:
can I send an angry handwritten letter to Irif that you scan and publish verbatim on
@coqlang?
Yes please! But as it is addressed to IRIF it needs a wax seal, _à la ancienne_
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:42):But going back to that tweet, indeed the retweet can be a good chance to actually point out the out of date information
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:42):I will personally retweet to that
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:42):so if you think that way, it is a good thing, as we can use twitter to just point out the paper is bogus
Karl Palmskog (Oct 21 2021 at 13:44):it's not a bogus paper overall, my view in a nutshell is that it gives a very misleading picture of Coq and its ecosystem
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:45):Here you go https://twitter.com/ejgallego/status/1451182716049768450
@Jose_A_Alonso @CoqLang It should be noted that the information on this paper regarding Coq's ecosystem libraries is _very_ outdated, thanks to a significant effort by many people, and in particular https://github.com/coq-community/ , the Coq package ecosystem is fully maintained and installable.
- Emilio Jesús GA (@ejgallego) Karl Palmskog (Oct 21 2021 at 13:45):OK, thanks.
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:45):Now that we are reviewing papers , my opinion is that it is bogus, but that's a different story :) This is why I refrain from judging contrituions from Coqlang, and instead try to share all equally
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:46):then people can comment and judge by themselves, we are talking about twitter after all XD
Karl Palmskog (Oct 21 2021 at 13:48):if one wants to do a heavyweight export of Coq code/terms to some intermediate format, I'm not sure how one can do it differently in principle. Of course, heavyweight exports are not very meaningful in the first place I think, and the tooling to work with the exported stuff seems inadequate. But hard to go from there to "bogus".
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:50):The approach has a few fatal flaws, including one of actually not working, but indeed we can discuss that paper in private if you are interested
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:51):I still think the work deserves some publicity tho,
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:51):these are not incompatible concepts for me
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:55):[disclaimer I was a reviewer for that paper]
Last updated: Apr 19 2024 at 02:02 UTC