Skip to content

Conversation

hannesm
Copy link
Member

@hannesm hannesm commented Jun 2, 2025

This is the proposal from the run started late May.

@hannesm hannesm force-pushed the maintenance-intent branch from 6456010 to 4789b68 Compare June 6, 2025 09:49
@mseri
Copy link
Member

mseri commented Jun 12, 2025

This is ready to merge once the new opam is released (right?)

@hannesm
Copy link
Member Author

hannesm commented Jun 12, 2025

This is ready to merge once the new opam is released (right?)

yes. I'm fine to take care of it.

@hannesm hannesm force-pushed the maintenance-intent branch from 4789b68 to f506a4b Compare June 19, 2025 20:16
@hannesm
Copy link
Member Author

hannesm commented Jun 19, 2025

ok, opam 2.4 beta1 is out - I'll merge that now.

@hannesm hannesm merged commit 2c7fa9d into ocaml:master Jun 19, 2025
3 checks passed
@hannesm hannesm deleted the maintenance-intent branch June 19, 2025 20:35
@Blaisorblade
Copy link
Contributor

I'm debugging some CI regression, and it seems due to this MR — I guess I just need to add https://github.com/ocaml/opam-repository-archive to undo its effects, and read https://discuss.ocaml.org/t/proposed-package-archiving-policy-for-the-opam-repository/15713 for more info?

Including such context would speed up debugging. I genuinely don't know if you should have.

Should somebody else run into similar problems, the error I got was simply that some package was no longer available:

$ opam install local-package-foo

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><>  🐫
[local-package-foo.dev] synchronised (no changes)

[ERROR] Package conflict!
  * Missing dependency:
    - local-package-foo → local-package-bar → dune = 3.17.2 → dune.3.17.2: no longer available

No solution found, exiting

@hannesm
Copy link
Member Author

hannesm commented Jun 20, 2025

Dear @Blaisorblade, thanks for your comment. Sorry for the inconvenience.

I don't quite understand what you mean with "Including such context would speed up debugging. I genuinely don't know if you should have." -- Where should "such context" be included? In this issue, in the discuss post, ...?

@liyishuai
Copy link
Contributor

Is there a version of Dune that never gets pruned from this repository?

If not, then I might need to explicitly maintain some "Dune LTS" repo.

@mseri
Copy link
Member

mseri commented Jun 23, 2025

That's a very good point. We should have a better strategy for some critical packages like dune. In the meantime there are three fast workarounds:

  1. add opam-repository-archive as additional opam repository until you decide to update your dune version
  2. re-instate the necessary archived packages here (we can always do it when it is important for some workflows). We just need to remove it from opam-repository-archive and add it back here with x-maintained: true (until you don't need it any longer)
  3. move to more recent dune (but I know that this is not always doable and that sometimes one wants something more stable)

Ping @shonfeder and @raphael-proust (can you also pin somebody from dune to discuss this?)

@mseri
Copy link
Member

mseri commented Jun 23, 2025

See also #28065 (thanks for opening the issue)

@hannesm
Copy link
Member Author

hannesm commented Jun 23, 2025

That's a very good point. We should have a better strategy for some critical packages like dune. In the meantime there are three fast workarounds:

1. add `opam-repository-archive` as additional opam repository until you decide to update your dune version

2. re-instate the necessary archived packages here (we can always do it when it is important for some workflows). We just need to remove it from `opam-repository-archive` and add it back here with `x-maintained: true` (until you don't need it any longer)

3. move to more recent dune (but I know that this is not always doable and that sometimes one wants something more stable)

Ping @shonfeder and @raphael-proust (can you also pin somebody from dune to discuss this?)

I'd be in favour of option 2. We can add a comment where this version is used/pinned.

@raphael-proust
Copy link
Contributor

Maybe long term we need to allow x-maintained: "LTS 12m" and then the archiver resolves this to true if the date it is run at is within 12months of the date the package was introduced.

In the meantime, we can re-instate yes.

@hannesm
Copy link
Member Author

hannesm commented Jun 23, 2025

@raphael-proust that's an interesting path to take. I can see that there may be similar failures if users don't update the versions at the right time.

So, I'm more interested how can we get the users to report which packages they rely on, and I asked this in #28065.

@pi8027
Copy link
Contributor

pi8027 commented Jun 23, 2025

Dear @hannesm, do you mind unarchiving elpi (at least 1.16.10, 1.17.4, and 1.19.6)? Elpi is a part of the recent Docker MathComp images (2.x.x-...), and we are heavily depending on them in CI.

@hannesm
Copy link
Member Author

hannesm commented Jun 23, 2025

Dear @pi8027, thanks for your comment. Would you mind to point to the source where these elpi versions are referenced, so we can keep that as a reference?

@pi8027
Copy link
Contributor

pi8027 commented Jun 23, 2025

@hannesm I found these version numbers in the output of CI, but 1.19.6 should be the latest version of Elpi compatible with Coq 8.19. The constraints can be found in the opam file for the coq-elpi package: https://github.com/rocq-prover/opam/blob/master/released/packages/coq-elpi/coq-elpi.2.2.3/opam

If I'm not mistaken, 1.16.10 and 1.17.4 should be the same thing for Coq 8.17 and 8.18. Let me check.

@hannesm
Copy link
Member Author

hannesm commented Jun 23, 2025

Thanks, to me it looks like elpi 1.16.10 (for coq-elpi 1.18.0 for coq 8.17), and elpi 1.18.1 (for coq-elpi 2.0.0.1 for coq 8.18). but you likely know your CI better :)

@pi8027
Copy link
Contributor

pi8027 commented Jun 23, 2025

You are right.

  • elpi.1.16.10 and coq-elpi.1.16.0 are the latest releases compatible with Coq 8.16.
  • The mathcomp/mathcomp:2.0.0-coq-8.17 and mathcomp/mathcomp:2.0.0-coq-8.18 image uses slightly older versions of Elpi and Coq-Elpi than the ones you pointed out, seemingly because of the dependency path coq-mathcomp-ssreflect.2.0.0 -> coq-hierarchy-builder -> coq-elpi and the constraints involved.

I'm unsure if I can provide a complete list of the versions of Elpi potentially used in CI. I probably need to check all the Docker images... (Unfortunately, I don't have time to do so right now.)

@pi8027
Copy link
Contributor

pi8027 commented Jun 23, 2025

Let me try to summon @erikmd, who maintains the Docker Coq/MathComp images.

@pi8027
Copy link
Contributor

pi8027 commented Jun 23, 2025

Or we can dry-run opam install for all the possible combinations of the versions of coq-mathcomp-ssreflect.2.x and Coq/Rocq to see which version of Elpi it wants to install.

@shonfeder
Copy link
Member

Ping

Since the dune maintenance intent is set by dune devs, maybe an issue on the dune repo is on order?

HadrienRenaud added a commit to HadrienRenaud/herdtools7 that referenced this pull request Jun 24, 2025
@mseri
Copy link
Member

mseri commented Jun 24, 2025

Good idea, @shonfeder can you do that, linking the issue?

HadrienRenaud added a commit to HadrienRenaud/herdtools7 that referenced this pull request Sep 8, 2025
HadrienRenaud added a commit to HadrienRenaud/herdtools7 that referenced this pull request Sep 8, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

8 participants