Stream: Coq devs & plugin devs

Topic: Coq 8.17.1


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jun 27 2023 at 10:39):

You mean, back to the Coq repository? Sure.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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}

view this post on Zulip Emilio Jesús Gallego Arias (Jun 27 2023 at 11:16):

@Théo Zimmermann would you like to work at some point on uploading 8.17.1 packages with dune-release?

view this post on Zulip 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-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.

There was a fix for this in 8.17.1, so it is not relevant anymore: https://github.com/coq/coq/pull/17433

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jun 28 2023 at 21:17):

all 8.17.1 packages (except coqide) are out on opam now

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 30 2023 at 08:34):

OK, and I will copy the minimum bound from coq-core.

view this post on Zulip 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?)

view this post on Zulip Karl Palmskog (Jun 30 2023 at 08:43):

I didn't "add" anything, we just copy from previous opam packages.

view this post on Zulip 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)

view this post on Zulip 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)))

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 08:45):

@Karl Palmskog we test the coqide opam package in our CI, so "it works for us"

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 08:45):

open a bug if there is some problem

view this post on Zulip Karl Palmskog (Jun 30 2023 at 08:46):

"it works for us" doesn't make them merge anything in the opam-repository.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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" ?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 08:48):

Where did you get this information from?

view this post on Zulip Karl Palmskog (Jun 30 2023 at 08:48):

the RM doesn't do opam packages in opam-repository, this is done by volunteers

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 08:49):

Lack of manpower != "washing hands"

view this post on Zulip Karl Palmskog (Jun 30 2023 at 08:49):

it's inevitable that since opam-repository has different constraints, packages in repo will not work

view this post on Zulip Karl Palmskog (Jun 30 2023 at 08:49):

either something is part of the RM (core) work or not.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jun 30 2023 at 08:51):

it has taken up to a week in some cases

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 08:52):

Yes, I can understand very well how little appreciation work on tooling gets

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 08:53):

At some points it has gotten me _extremely_ frustated

view this post on Zulip Karl Palmskog (Jun 30 2023 at 08:53):

this is not even tooling

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 08:53):

however it is important not let frustation talk and lead to misleading statements

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 30 2023 at 09:27):

I meant "wash hands" in English sense of: "don't want to have to do with"

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):

That's a decision of each particular RM, not of core, but yes.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):

We need to solve https://github.com/coq/coq/issues/16071 first

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):

But should be easy

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:28):

Newer dune have actually improved support for this

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Jun 30 2023 at 09:31):

https://github.com/coq/coq/pull/17791

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:31):

The workflow we should have is roughtly:

view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jun 30 2023 at 09:37):

this is how we treat Coq releases on opam-repository currently

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:37):

What does that mean?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:43):

What makes you not convinced?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jun 30 2023 at 09:43):

what is the evidence that it works?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:44):

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:44):

What is the evidence you have that it doesn't work?

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:46):

They are using it.

view this post on Zulip 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"}

view this post on Zulip Karl Palmskog (Jun 30 2023 at 09:48):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:49):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:49):

so indeed Coq RC packages should do the same

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:49):

or they could provide different instructions for opam 2.0 vs 2.1

view this post on Zulip Karl Palmskog (Jun 30 2023 at 09:50):

so our RCs are not supposed to work on opam 2.0?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:50):

They are supposed to work

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?"

view this post on Zulip Karl Palmskog (Jun 30 2023 at 09:54):

but you are saying yourself avoid-version is not working in opam 2.0?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):

Indeed it doesn't work, how is that a problem?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):

For opam 2.0 we use the old method of a repos

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):

Can you answer my question now so we can continue the discussion?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:55):

Karl Palmskog said:

but you are saying yourself avoid-version is 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 09:58):

That is not my position.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 10:00):

I'm actually familiar with the problems avoid-version have by the way

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jun 30 2023 at 10:01):

most users have no idea about what opam version they are using

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 10:01):

That's why the instructions provided work for both versions

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 10:02):

and the metadata works for both versions

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2023 at 10:04):

Not only unfounded but factually wrong.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Jun 13 2024 at 06:01 UTC