Théo Zimmermann (Jun 27 2023 at 09:21): Théo Zimmermann (Jun 27 2023 at 09:21):Coq 8.17.1 has been released. Can we get opam packages and Docker-Coq update? cc @Karl Palmskog @Erik Martin-Dorel
Also cc @Michael Soegtrop FYI.
Théo Zimmermann (Jun 27 2023 at 09:27):When opam packages are out, we should update this: https://github.com/coq/www/blob/master/incl/macros.html
Karl Palmskog (Jun 27 2023 at 10:24):@Théo Zimmermann if I do the CoqIDE package (usually a terrible experience) can you do a Coq PR with the resulting CoqIDE opam file that has run their CI gauntlet?
Théo Zimmermann (Jun 27 2023 at 10:39):You mean, back to the Coq repository? Sure.
Karl Palmskog (Jun 27 2023 at 10:39):right, the idea is that we'd like opam-repository package definition to be in sync with Coq repository ones, as far as possible
Karl Palmskog (Jun 27 2023 at 10:40):for example, I noticed we had to add the following in the coq-core package:
conflicts: [
"coq" { < "8.17" }
"ocaml-option-bytecode-only"
]
The coq conflict is obvious, but I have no idea why bytecode only didn't work for 8.17.0.
Karl Palmskog (Jun 27 2023 at 10:55):also, shouldn't the coq.opam file in the repo have:
["dune" "subst"] {dev}
rather than
["dune" "subst"] {pinned}
@Théo Zimmermann would you like to work at some point on uploading 8.17.1 packages with dune-release?
Théo Zimmermann (Jun 27 2023 at 11:37):Karl Palmskog said:
for example, I noticed we had to add the following in the
coq-corepackage:conflicts: [ "coq" { < "8.17" } "ocaml-option-bytecode-only" ]The
coqconflict is obvious, but I have no idea why bytecode only didn't work for 8.17.0.
There was a fix for this in 8.17.1, so it is not relevant anymore: https://github.com/coq/coq/pull/17433
Karl Palmskog (Jun 27 2023 at 11:38):OK, I guess I will push the diff once the regular opam-repository CI run is finished
Théo Zimmermann (Jun 27 2023 at 11:38):Emilio Jesús Gallego Arias said:
Théo Zimmermann would you like to work at some point on uploading 8.17.1 packages with
dune-release?
I completely forgot about experimenting with dune-release when doing this release. But I think this is not really relevant anymore: dune-release is only useful if it takes care of the full process, including creating the GitHub release opam PR.
Emilio Jesús Gallego Arias (Jun 27 2023 at 11:54):Yes, the idea was to let dune-release create the opam packages, files, api doc, etc... open the PRs, upload the artifacts
Karl Palmskog (Jun 28 2023 at 21:17):all 8.17.1 packages (except coqide) are out on opam now
Karl Palmskog (Jun 29 2023 at 21:15):coqide.8.17.1 is out. Propagating the opam changes to coqide.opam in the Coq repo is a good idea.
Théo Zimmermann (Jun 30 2023 at 08:29):I have tried porting the changes to the Coq repo, but I have an issue that this file is supposed to be Dune-generated and I didn't find how to specify a build-only dependency in Dune (this is not documented).
Théo Zimmermann (Jun 30 2023 at 08:31):And even if I don't specify that a dependency is build-only, Dune still forces me to provide arguments (version bounds), when the opam file from the opam-repository doesn't have such bounds for all the dependencies.
Karl Palmskog (Jun 30 2023 at 08:32):in the case of OCamlfind, maybe making it a regular dep is the way to go, since it's a regular dep in coq-core.
Théo Zimmermann (Jun 30 2023 at 08:34):OK, and I will copy the minimum bound from coq-core.
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:42):Why did you add the build-only stuff folks?
@Théo Zimmermann it should be possible to specify the build-only stuff, let me have a look (and maybe open a bug?)
Karl Palmskog (Jun 30 2023 at 08:43):I didn't "add" anything, we just copy from previous opam packages.
Karl Palmskog (Jun 30 2023 at 08:44):the CoqIDE opam package in the Coq repo has been broken for maybe 2+ years (as defined by opam-repository CI)
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:44):@Théo Zimmermann this is the way:
(package
(name coq-lsp)
(depends
(coq :build)))
@Karl Palmskog we test the coqide opam package in our CI, so "it works for us"
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:45):open a bug if there is some problem
Karl Palmskog (Jun 30 2023 at 08:46):"it works for us" doesn't make them merge anything in the opam-repository.
Karl Palmskog (Jun 30 2023 at 08:47):since core has washed their hands of opam packaging [in opam-repository], how can it be a bug?
Théo Zimmermann (Jun 30 2023 at 08:48):Well, no need to open a bug since I said I would open a PR with these changes.
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:48):@Karl Palmskog I'm unable to understand what you mean. What does "core has washed their hands" ?
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:48):Where did you get this information from?
Karl Palmskog (Jun 30 2023 at 08:48):the RM doesn't do opam packages in opam-repository, this is done by volunteers
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:49):In fact see https://github.com/coq/coq/issues/17362 , the plan is to have this happen automatically
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:49):Lack of manpower != "washing hands"
Karl Palmskog (Jun 30 2023 at 08:49):it's inevitable that since opam-repository has different constraints, packages in repo will not work
Karl Palmskog (Jun 30 2023 at 08:49):either something is part of the RM (core) work or not.
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:50):You think is inevitable, but I have released over a hundreth releases of OCaml packages using the method we plan for Coq and it works pretty well.
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:51):I'm unsure what problem you are having with opam-repository, as last time you claimed that packages took like weeks to be merged, which is not the case, etc...
Karl Palmskog (Jun 30 2023 at 08:51):fine by me if core/RM starts to do package releases to opam-repository, but that's not how it works now
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:51):That's not how it works now because of lack of time, but you can see the open issues and roadmap
Karl Palmskog (Jun 30 2023 at 08:51):it has taken up to a week in some cases
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:51):I did propose to migrate 8.17.1 and 8.18 to dune-release, but indeed I can understand the RMs not having time
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:52):In my opinion your statements give a misleading information about what the team position in this issue is. Anyways let's go back on topic
Karl Palmskog (Jun 30 2023 at 08:52):I can add that submitting these packages is very thankless, since most people have the impression that this is core/RM work
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:52):Yes, I can understand very well how little appreciation work on tooling gets
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:53):At some points it has gotten me _extremely_ frustated
Karl Palmskog (Jun 30 2023 at 08:53):this is not even tooling
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:53):Not only it is often not appreciated, but often people push back against that with bogus reasons
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:53):however it is important not let frustation talk and lead to misleading statements
Emilio Jesús Gallego Arias (Jun 30 2023 at 08:54):Karl Palmskog said:
this is not even tooling
For me it is about tooling as I see little point on spending time in doing manual processes instead of trying to automate it
Karl Palmskog (Jun 30 2023 at 08:54):what is misleading? I stated that RM does not handle opam-repository packages, and it is not handled by core
Karl Palmskog (Jun 30 2023 at 08:57):if a package maintainer for an obscure Linux distro opened a bug about how his packaging process failed, is this considered a Coq bug? It might be, but probably not.
Théo Zimmermann (Jun 30 2023 at 09:05):Emilio Jesús Gallego Arias said:
That's not how it works now because of lack of time, but you can see the open issues and roadmap
This is not just a question of lack of time, but also lack of skills. Not all core devs are regular opam users (I am not).
Karl Palmskog (Jun 30 2023 at 09:06):I appreciate that core are careful with their time, and there is a plan to automate this eventually. But until this happens, these kinds of incongruences between packages living in different locations will happen
"Wash hands" was perhaps a too pointed way to say this
Karl Palmskog (Jun 30 2023 at 09:07):@Théo Zimmermann maybe we can add a small RM checklist point that, unless the next opam release is automated, they can upstream opam changes like you are doing now (given that they are properly pinged in opam-repository PRs)
Théo Zimmermann (Jun 30 2023 at 09:08):Sure: if you open a PR on dev/doc/release-process.md, I will merge it.
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:26):Indeed I think I got confused by what you meant by "wash hands", in Spanish we use this to mean "you don't care at all"
We do care about automating opam packaging, and indeed only since 8.17 it is possible as we got all the pieces in place.
I'd indeed recommend for people interesting in uploading opam packages to stop doing any manual work, and instead try dune-release.
Karl Palmskog (Jun 30 2023 at 09:27):I meant "wash hands" in English sense of: "don't want to have to do with"
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):That's a decision of each particular RM, not of core, but yes.
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):We need to solve https://github.com/coq/coq/issues/16071 first
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):But should be easy
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):Newer dune have actually improved support for this
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:30):Emilio Jesús Gallego Arias said:
That's a decision of each particular RM, not of core, but yes.
core has done quite a bit of work, including preparing the split opam setup, and fixing some files, adding CI for the opam packages (not as complete as the CI in opam-repos)
Karl Palmskog (Jun 30 2023 at 09:31):https://github.com/coq/coq/pull/17791
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:31):The workflow we should have is roughtly:
dune-project happen in master (and backported to the branch) Karl Palmskog (Jun 30 2023 at 09:32):I don't think you have convinced others in core that RCs are submitted to opam-repository (as opposed to the Coq core-dev)?
Karl Palmskog (Jun 30 2023 at 09:33):the problem I see with having RCs in opam-repository is that they then become legitimate Coq targets that must be tested by everyone for their projects, even long after the stable version are released
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:36):Karl Palmskog said:
I don't think you have convinced others in core that RCs are submitted to opam-repository (as opposed to the Coq
core-dev)?
The decision was taken to do so, and it has significant advantages over the current setup.
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:36):Karl Palmskog said:
the problem I see with having RCs in opam-repository is that they then become legitimate Coq targets that must be tested by everyone for their projects, even long after the stable version are released
How is that the case?
Karl Palmskog (Jun 30 2023 at 09:37):this is how we treat Coq releases on opam-repository currently
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:37):What does that mean?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:37):rcs are avoid-version, so unless you request them explicitly they won't show up for the users
Karl Palmskog (Jun 30 2023 at 09:40):for example, the opam Coq bench tests every version of Coq. I'm not convinced that this avoid-version will work in practice
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:43):What makes you not convinced?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:43):Anyways the decision was taken, if you want to reopen the discussion I'm happy to, but a good reason should be givne
Karl Palmskog (Jun 30 2023 at 09:43):what is the evidence that it works?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:44): Emilio Jesús Gallego Arias (Jun 30 2023 at 09:44):What is the evidence you have that it doesn't work?
Karl Palmskog (Jun 30 2023 at 09:45):from what I can see, OCaml betas still require a special repository activation: https://discuss.ocaml.org/t/ocaml-5-0-0-first-beta-release/10623
Why aren't they using this?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:46):They are using it.
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:48):You asked this several times, I'm unsure what problem we are having here:
$ opam show ocaml-base-compiler.5.0.0~rc1
flags compiler avoid-version
depends "ocaml" {= "5.0.0" & post}
"base-unix" {post}
"base-bigarray" {post}
"base-threads" {post}
"base-domains" {post}
"base-nnp" {post}
"ocaml-options-vanilla" {post}
"ocaml-option-bytecode-only" {arch != "arm64" & arch != "x86_64"}
"ocaml-beta" {opam-version < "2.1.0"}
here is from April, they also require special repo activation: https://discuss.ocaml.org/t/first-alpha-release-of-ocaml-5-1-0/11949
opam switch create 5.1.0~alpha1 --repositories=default,beta=git+https://github.com/ocaml/ocaml-beta-repository.git
I even requested the main opam-repos maintainer to come and confirm this is OK, so it is beyond my understanding what more do you need
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:49):@Karl Palmskog this is because the instructions are supposed to work also in opam 2.0.0 which doesn't support the avoid flag
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:49):so indeed Coq RC packages should do the same
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:49):or they could provide different instructions for opam 2.0 vs 2.1
Karl Palmskog (Jun 30 2023 at 09:50):so our RCs are not supposed to work on opam 2.0?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:50):They are supposed to work
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:50):We have had this discussion already 3 times, yet you still don't trust me or the opam-repos maintainer
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:52):I would appreciate if you could look at the opam 5.0.0-rc metadata before making such claims which are factually incorrect
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:53):I'd appreciate if you could answer my question tho, I will repeat it again:
"What evidence you have that it doesn't work?"
Karl Palmskog (Jun 30 2023 at 09:54):but you are saying yourself avoid-version is not working in opam 2.0?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):Indeed it doesn't work, how is that a problem?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):For opam 2.0 we use the old method of a repos
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):Can you answer my question now so we can continue the discussion?
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):Karl Palmskog said:
but you are saying yourself
avoid-versionis not working in opam 2.0?
The metadata I posted seems pretty clear to me, do you have any question about it? I'm happy to help.
Karl Palmskog (Jun 30 2023 at 09:57):so your position is: a technology for which no long list of flaws is immediately available must be accepted? If anything, I think we should recommend the repo activation approach for everyone
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:58):That is not my position.
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:58):I won't continue the discussion until you answer my question. I did answer yours, I think it is only fair I get a response
Karl Palmskog (Jun 30 2023 at 09:59):I'm not very familiar with the exact implementation of avoid-version, but the whole 2.0/2.1 difference seems like a serious flaw to me.
Emilio Jesús Gallego Arias (Jun 30 2023 at 09:59):My position is that opam and opam-repositoty have an official method to support rc version of software, which has significant advantages over the old "add a repos" solution. I do agree with opam upstream and I think this is the system Coq should use.
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:00):Karl Palmskog said:
I'm not very familiar with the exact implementation of
avoid-version, but the whole 2.0/2.1 difference seems like a serious flaw to me.
This doesn't answer my question. Or maybe the above implies that your answer is "I don't have any evidence that the official avoid-version setup is problematic"
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:00):I'm actually familiar with the problems avoid-version have by the way
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:01):Another question why is the 2.0 / 2.1 difference a flaw, and serious?
Karl Palmskog (Jun 30 2023 at 10:01):most users have no idea about what opam version they are using
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:01):That's why the instructions provided work for both versions
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:02):and the metadata works for both versions
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:04):I am sorry but I don't think the way things go here in terms of "providing evidence" is a healthy point of view. If you think a official solution that was long researched and decided by experts (avoid-version) and has been quite well tested (and problems found actually) is problematic, it is up to _you_ to provide evidence of the problem. The opam maintainers or myself have no obligation to produce evidence to counteract unfounded claims.
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:04):Not only unfounded but factually wrong.
Emilio Jesús Gallego Arias (Jun 30 2023 at 10:06):Moreover we have had this discussion more than twice already, including a call when the solution was decided.
Paolo Giarrusso (Jun 30 2023 at 10:37):to be clear, it seems OCaml RCs are disabled by default on all opam versions _and_ can be opted in for any opam >= 2.0 — this is just harder for opam 2.0? That does seem reasonable to me, in effect, but I can see why it raises questions
Paolo Giarrusso (Jun 30 2023 at 10:40):But I consider Karl an informed observer; if the discussion keeps coming up, maybe the answer isn't sufficiently documented? If it were, questions could be answered by a link.
Karl Palmskog (Jun 30 2023 at 10:42):my bottom line is that repo activation would be my preferred option for RCs in any opam version, and I have no idea how avoid-version will work out in practice
Paolo Giarrusso (Jun 30 2023 at 10:43):IIUC, that'd require more complex commands for opam >= 2.1, and the upside would be saving opam --version?
Paolo Giarrusso (Jun 30 2023 at 10:44):IIUC, opam switch create 5.1.0~alpha1 would fail-safe for opam 2.0. The only downside might be a bad error message?
Karl Palmskog (Jun 30 2023 at 10:46):yeah, I hope there will be some analysis of these commands in many opam versions before they [the instructions] go public
Erik Martin-Dorel (Jul 12 2023 at 12:17):Just FYI, cross-posting this comment of mine:
https://github.com/coq-community/docker-coq/issues/57#issuecomment-1632424323
Last updated: Dec 05 2023 at 11:01 UTC