Julien Puydt (Mar 15 2022 at 07:38): Julien Puydt (Mar 15 2022 at 07:38):Hi, I'm the main packager for coq in Debian, so I'm a bit annoyed by this proposition: the why3 main packager wants to drop support for coq...
Any advice?
Théo Zimmermann (Mar 15 2022 at 07:43):I must say that his arguments make sense to me, the fact that Debian can only package one version of Coq and that the latest version of Why3 is always lagging behind in terms of Coq support makes the situation difficult. If it helps, I assume that we could consider adding Why3 to Coq's CI so that compatibility fixes arrive earlier. But it would still require Why3 to make more frequent releases after a Coq release, and this is something that only Why3 maintainers can decide to commit to (or not).
Karl Palmskog (Mar 15 2022 at 08:01):didn't the more high-level tools using Why3 like wp drop Coq support as well? Release timing compatibility seems a really high bar for having an integration, though...
Guillaume Melquiond (Mar 15 2022 at 08:12):Karl Palmskog said:
didn't the more high-level tools using Why3 like wp drop Coq support as well?
Frama-C developers did indeed drop support for Coq a few months ago. (But this is no way related to Why3's own support for Coq, as far as I know.)
Enrico Tassi (Mar 15 2022 at 17:01):what does it mean to drop support for coq exactly? there used to be a coq tactic, and that clealy depends on the Coq internals. But wasn't why generating text (coq text)? Is that dropped too?
Guillaume Melquiond (Mar 15 2022 at 17:13):The Coq tactic was removed several years ago. What is at stake here is the Coq realization of the Why3 standard library, so pure .v files. They are not strictly necessary, but it basically means that users will no longer use Coq to discharge Why3 proof obligations. They will have to resort to other provers (i.e., for interactive provers, Isabelle/HOL).
Enrico Tassi (Mar 15 2022 at 17:22):How is that so dependant on the Coq version?
Guillaume Melquiond (Mar 15 2022 at 17:25):Because new releases of Coq mean that .v files need to be adapted to non-backward compatible features.
Guillaume Melquiond (Mar 15 2022 at 17:26):So, the master branch of Why3 can be compiled with Coq 8.15, but none of the actual releases.
Ali Caglayan (Mar 15 2022 at 17:27):I don't get why debian can't supply multiple versions of coq? How do they package python for example? That is quite version incompatible sometimes.
Guillaume Melquiond (Mar 15 2022 at 17:32):A few packages are deemed worth the effort of maintaining several versions (e.g., Python 2 versus Python 3). I doubt Coq falls into that category.
Paolo Giarrusso (Mar 15 2022 at 18:45):But why3 would still support Coq, this thread is just about the Debian package...
Karl Palmskog (Mar 15 2022 at 18:50):Paolo Giarrusso said:
But why3 would still support Coq, this thread is just about the Debian package...
Based on what Guillaume and Ralf Treinen are saying, my interpretation is that the Why3 repo will drop all Coq support, probably forever. This means that there is no way to maintain applications like this anymore, where a WhyML program's correctness depends on a Coq theorem: https://github.com/coq-community/bertrand/blob/master/why/Knuth.mlw
Karl Palmskog (Mar 15 2022 at 18:52):this is unfortunate, but it seems very hard to coordinate release schedules and compatibility requirements just for this integration
Paolo Giarrusso (Mar 15 2022 at 18:52):@Karl Palmskog but AFAICT Ralf Treinen only maintains the Why3 _Debian_ packages, and everything else is a misunderstanding?
Paolo Giarrusso (Mar 15 2022 at 18:53):At least AFAICT:
http://why3.lri.fr/
Why3 is developed in the team-project Toccata (formerly ProVal) at Inria Saclay-Île-de-France / LRI Univ Paris-Saclay / CNRS.
and https://toccata.gitlabpages.inria.fr/toccata/members.en.html does not list Treinen anywhere.
Paolo Giarrusso (Mar 15 2022 at 18:53):@Guillaume Melquiond you indeed talked about Why3 itself, not the Debian package, but do you have some extra information?
Karl Palmskog (Mar 15 2022 at 18:54):my reading is that Ralf just views the Debian packaging problems as a symptom, and he plans to cut off the problematic limb completely
Paolo Giarrusso (Mar 15 2022 at 18:55):and he asks for feedback to "Debian OCaml Maintainers"?
Théo Zimmermann (Mar 15 2022 at 18:55):Ralf is a prof in my lab, he is not related to (upstream) Why3 maintenance.
Théo Zimmermann (Mar 15 2022 at 18:55):He is a Debian maintainer.
Théo Zimmermann (Mar 15 2022 at 18:55):And he used to maintain the Coq package as well before @Julien Puydt came along.
Paolo Giarrusso (Mar 15 2022 at 18:55):so you're basically confirming he's just talking about Debian packages?
Théo Zimmermann (Mar 15 2022 at 18:56):Yes
Paolo Giarrusso (Mar 15 2022 at 18:57):Thanks. Because Ralf's email was extremely ambiguous outside of its context.
Paolo Giarrusso (Mar 15 2022 at 18:58):IOW, Why3-Coq users would have to install Why3 otherwise — say via Coq Platform + opam install why3.
Karl Palmskog (Mar 15 2022 at 18:59):hmm, do we even know this is possible generally? From what I remember, why3 has a lot of dependencies that may conflict with the Platform's (i.e., different mandated versions)
Paolo Giarrusso (Mar 15 2022 at 19:14):Yes, "say" was doing lots of work; but IIUC the platform scripts are customizable enough that anybody can create a new pick (and yes, you'll have to build from source, or use Nix instead).
Karl Palmskog (Mar 15 2022 at 19:16):well, "anybody can create a new pick", but only if a pick which satisfies all version requirements actually exists
Karl Palmskog (Mar 15 2022 at 19:17):I guess my main worry is about OCaml-level incompatibilities
Guillaume Melquiond (Mar 15 2022 at 19:46):Karl Palmskog said:
Based on what Guillaume and Ralf Treinen are saying, my interpretation is that the Why3 repo will drop all Coq support, probably forever.
No. I was only talking about the Debian packaging of Why3 (and about Frama-C). As for Why3 itself, I have no intention of dropping Coq support. All the releases of Why3 up to now have supported the latest release of Coq at that time, and I intend to keep it that way for the foreseeable future.
Enrico Tassi (Mar 15 2022 at 20:51):Wouldn't it make sense to have these .v files be part of Coq's CI? Not really to help you port them, but to see these breakages. I did not think we were doing so many these days.
Julien Puydt (Mar 16 2022 at 08:01):Ok, things went a bit south this night, so let me get a few things straight.
The title of the thread is quite explicit on the scope: it's about why3's Debian package, not about why3 upstream.
Since both coq and why3 in Debian are managed within the "Debian Ocaml Maintainers" team, the Debian Developer behind the why3 packaging (Ralf Treinen) wrote to that team to explain issues he had with why3's Debian package, present his plans to get around them and get feedback from the team. And since I'm a member of that team and nowadays the Debian Developer behind the coq packaging, I'm now asking for feedback here, as the issues raised are definitely upstream-level.
If I followed well the complaints are:
coq-on-Debian's lack of support for some architectures -- that's my doing, but I reported it as an issue so that part is already a work-in-progress hopefully ;
coq-upstream moves too fast with respect to why3-upstream -- that's only a problem if newer coq releases break things, so perhaps there are ways to make sure that doesn't happen too often. I don't think it's been precisely reported, but I get the impression that it's related to the recent discussions about coqide, vscoq & the rest : after all it's some sort of user interface on top of coq...
There are several ways forward, in fact:
I think 1. is lazy and bad, 2. unrealistic and 3. looks like a better one.
Julien Puydt (Mar 16 2022 at 08:07):About packaging several coq versions: yes, that could be done. But not without coq upstream making it easier. For example, coq libs should get installed and easily found in versioned paths -- I fought long and hard to get things working in the Debian package for just a single version, and it's definitely not just me! The executables should be versioned too, ie /usr/bin/coq8.15 and /usr/bin/coq8.16 (and then the Debian packages would use tricks to provide /usr/bin/coq as a symlink to the latest).
For Python, upstream had Python 2 and Python 3 and worked hard to make things co-installable without toe-stomping. And even then, that was quite a pain. [I'm a member of the Debian Python team too...]
Paolo Giarrusso (Mar 16 2022 at 08:08):re the breakage, I think you misunderstand: this is not a user interface problem. Why3 includes some actual Coq source code, and different Coq versions are not 100% source compatible.
Guillaume Melquiond (Mar 16 2022 at 08:08):Julien Puydt said:
I don't think it's been precisely reported, but I get the impression that it's related to the recent discussions about coqide, vscoq & the rest : after all it's some sort of user interface on top of coq...
No. This is unrelated to the user interface. Why3 does not care about such things. It just runs coqtop over a .v file and hopes for the best. (It could also be coqc, but Why3 does not care about .vo files, so coqtop it is.) This .v possibly depends on a bunch of precompiled .vo files (https://gitlab.inria.fr/why3/why3/-/tree/master/lib/coq), so the question is whether they do or do not compile with a given version of Coq.
Paolo Giarrusso (Mar 16 2022 at 08:12):versioning the executables might be expensive but it could be worthwhile, since different Coq releases are not source compatible.
Julien Puydt (Mar 16 2022 at 08:19):You mean they use actual coq source files, coming from coq itself, giving them access to internal representations of data hence highly volatile, not just coq source file like mathcomp? That's where I'm not sure I get things right. Notice that in that case, it's still a matter of coq providing a clean interface so why3 uses that and doesn't need to access the internals.
What makes why3 needs different from those coqide and vscoq? [Notice: I don't know much about why3 yet]
Guillaume Melquiond (Mar 16 2022 at 08:19):Paolo Giarrusso said:
versioning the executables might be expensive but it could be worthwhile, since different Coq releases are not source compatible.
But versioning the executables also makes things more awkward. Let us consider the example of Why3 again. Should the Debian package for Why3 then depend on a very specific version of Coq (possibly different from some other package containing Coq libraries, even if there would be a common release of Coq compatible with both packages)? Or should there be as many versions of Why3's Coq libraries as there are Coq executables?
Guillaume Melquiond (Mar 16 2022 at 08:22):Julien Puydt said:
You mean they use actual coq source files, coming from coq itself, giving them access to internal representations of data hence highly volatile, not just coq source file like mathcomp? That's where I'm not sure I get things right. Notice that in that case, it's still a matter of coq providing a clean interface so why3 uses that and doesn't need to access the internals.
From a packaging perspective, Why3 is no different from MathComp. It is just a bunch of Coq vernacular files that need to be compiled. (Let us ignore the Why3 tool itself, which is completely oblivious to Coq.)
Paolo Giarrusso (Mar 16 2022 at 08:23):@Guillaume Melquiond “more awkward” compared to which alternative?
Guillaume Melquiond (Mar 16 2022 at 08:25):Compared to having a single Coq executable. If you have only one executable, you only have one user-contrib directory to fill. If there are many, so are there contribution directories.
Paolo Giarrusso (Mar 16 2022 at 08:25):but in that alternative, there is no why3 package at all, so why3 + coq users would need to install it from opam.
Michael Soegtrop (Mar 16 2022 at 08:26):I think at some point in time it might make sense to test certain packages not in Coq Platform, say one a week, in Coq Platform CI to see if they are compatible with Coq Platform - just to publish this any maybe to inform the package maintainers.
Paolo Giarrusso (Mar 16 2022 at 08:26):to be clear: outside of Why3, supporting multiple Coq versions would make distribution packages more useful, tho I don’t know how many users would care.
Enrico Tassi (Mar 16 2022 at 09:04):@Guillaume Melquiond how are these files entangled to why3? I mean, would just taking the lib/coq/ directory from master work with an older version of why3? If the entanglement is light, then this is the simplest solution (the Debian package couples a released why3 with a cherry pick of the coq stuff).
Enrico Tassi (Mar 16 2022 at 09:05):Then R.Trainer may not like this and opt out, his time after all... but I would not do anything on the Coq side if that was the case.
Guillaume Melquiond (Mar 16 2022 at 09:34):They are very tightly entangled. (In fact, they are rewritten on the fly by Why3. As such, one of the CI jobs checks that this is the identity for the precompiled files, so that precompiling them still makes sense.) That said, we are careful with compatibility. Thus, one could presumably take the .v files from the master branch and dump them into an older release of Why3 and it would work out of the box.
Julien Puydt (Mar 17 2022 at 10:10):Well, a Debian package can come with patches to upstream -- they're supposed to be as simple as possible so we don't fork.
So if a new coq comes out and it's trivial/easy to patch why3, a new patched Debian why3 package can be published with an updated patch.
Say, if why3 upstream is 1.4.0, then the Debian packages will be 1.4.0-n with n starting at 1, and each increment in the Debian part of the versioning can mean updated patches, and change the coq version they depend on.
That would be a working solution.
Julien Puydt (Mar 18 2022 at 09:58):Oh, there's also the problem of coq having dropped support for some of the main architectures of Debian. I think I'll tell RT to proceed, then get back for a renewed support when that issue will be gone.
Paolo Giarrusso (Mar 18 2022 at 10:36):@Julien Puydt since I feel Zulip's better for chatting, let me reply to https://github.com/coq/coq/issues/15240#issuecomment-1072282186 here...
Paolo Giarrusso (Mar 18 2022 at 10:39):There's clearly something I'm missing, because it _seems_ you're not saying Coq has users on bytecode architectures, just that Coq should support them... so that users on other ones could get Coq and Why3 packaged together? Do I misunderstand something?
Paolo Giarrusso (Mar 18 2022 at 10:41):I can imagine why that might happen, but I'd hope that simpler solutions exist.
Julien Puydt (Mar 18 2022 at 10:44):I don't know if there are users on said architectures -- at least nobody complained about my change to the coq packaging, but there was no official Debian stable release since then.
Enrico Tassi (Mar 18 2022 at 10:44):Coq on bytecode is only useful for debugging purposes
Enrico Tassi (Mar 18 2022 at 10:46):What I mean is that no real user would be happy on a mipsel router. It would run, sure, but just to prove a point, no to do actual work.
Enrico Tassi (Mar 18 2022 at 10:48):Of course if the why3 maintainer also compiles it for mipsel...
Enrico Tassi (Mar 18 2022 at 10:48):I'd ask how SMTs do on that arch...
Julien Puydt (Mar 18 2022 at 10:49):Coq support in why3:
Those are the main reasons why the person managing the package in Debian wants to drop it, if I understood his mail.
And that means no coq support in why3 in any architecture, even the ones where coq works and has users.
Enrico Tassi (Mar 18 2022 at 10:51):I'd say: ask Ralf to put a line "install why3 (and coq) via opam if you need the coq backend" in the README.Debian
Enrico Tassi (Mar 18 2022 at 10:52):There is a reason if other package managers do exist. I did package many Lua stuff for debian, but also luarocks (the pkg manager of lua) and encouraged people to use it when the things they wanted could not be reasonably packaged in Debian (for both quality or policy).
Enrico Tassi (Mar 18 2022 at 10:56):IMO, it is not the end of the world if the why3 that comes as a deb does not support coq out of the box, as long as it tells users what do if they need the coq backend.
Last updated: May 31 2023 at 16:01 UTC