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?
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).
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...
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.)
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?
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).
How is that so dependant on the Coq version?
Because new releases of Coq mean that .v
files need to be adapted to non-backward compatible features.
So, the master
branch of Why3 can be compiled with Coq 8.15, but none of the actual releases.
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.
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.
But why3 would still support Coq, this thread is just about the Debian package...
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
this is unfortunate, but it seems very hard to coordinate release schedules and compatibility requirements just for this integration
@Karl Palmskog but AFAICT Ralf Treinen only maintains the Why3 _Debian_ packages, and everything else is a misunderstanding?
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.
@Guillaume Melquiond you indeed talked about Why3 itself, not the Debian package, but do you have some extra information?
my reading is that Ralf just views the Debian packaging problems as a symptom, and he plans to cut off the problematic limb completely
and he asks for feedback to "Debian OCaml Maintainers"?
Ralf is a prof in my lab, he is not related to (upstream) Why3 maintenance.
He is a Debian maintainer.
And he used to maintain the Coq package as well before @Julien Puydt came along.
so you're basically confirming he's just talking about Debian packages?
Yes
Thanks. Because Ralf's email was extremely ambiguous outside of its context.
IOW, Why3-Coq users would have to install Why3 otherwise — say via Coq Platform + opam install why3
.
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)
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).
well, "anybody can create a new pick", but only if a pick which satisfies all version requirements actually exists
I guess my main worry is about OCaml-level incompatibilities
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.
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.
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.
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...]
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.
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.
versioning the executables might be expensive but it could be worthwhile, since different Coq releases are not source compatible.
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]
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?
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.)
@Guillaume Melquiond “more awkward” compared to which alternative?
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.
but in that alternative, there is no why3 package at all, so why3 + coq users would need to install it from opam.
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.
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.
@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).
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.
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.
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.
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.
@Julien Puydt since I feel Zulip's better for chatting, let me reply to https://github.com/coq/coq/issues/15240#issuecomment-1072282186 here...
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?
I can imagine why that might happen, but I'd hope that simpler solutions exist.
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.
Coq on bytecode is only useful for debugging purposes
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.
Of course if the why3 maintainer also compiles it for mipsel...
I'd ask how SMTs do on that arch...
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.
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
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).
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: Dec 05 2023 at 06:01 UTC