Erik Martin-Dorel (Jul 15 2024 at 20:23): Erik Martin-Dorel (Jul 15 2024 at 20:23):Cc @Karl Palmskog @Pierre Roux I've just seen this:
https://github.com/coq-community/docker-coq-action/actions/runs/9942793660/job/27475427235
The following actions will be performed:
- recompile menhirSdk dev [upstream or system changes]
- recompile menhirLib dev [upstream or system changes]
- recompile menhir dev [upstream or system changes]
- recompile atd 2.15.0 [uses menhir]
- recompile atdts 2.15.0 [uses atd]
- recompile atdgen 2.15.0 [uses atd]
- recompile elpi 1.19.4 [uses menhir]
- recompile coq-elpi dev [uses elpi]
- recompile coq-hierarchy-builder dev [uses coq-elpi]
- recompile coq-mathcomp-ssreflect dev* [uses elpi]
- recompile coq-mathcomp-fingroup dev* [uses coq-mathcomp-ssreflect]
- recompile coq-mathcomp-algebra dev* [uses coq-mathcomp-fingroup]
- recompile coq-mathcomp-solvable dev* [uses coq-mathcomp-algebra]
- recompile coq-mathcomp-field dev* [uses coq-mathcomp-solvable]
- recompile coq-mathcomp-character dev* [uses coq-mathcomp-field]
But before triggering any rebuild, I'm puzzled to see that a released version of elpi pulls many dev dependencies
(this may be related to coqorg/coq:dev images which include extra-dev ?)
Also I don't know (yet) what is the exact behavior of opam w.r.t. dev packages with/without pinning:
is a mere push to the menhir git repository enough to raise an [upstream or system changes] ?
does this change if menhir if pinned to dev ? or pinned to a more precise version.
FTR, coq.dev pinning in coqorg/coq:dev is a "very precise" (git) pinning, thanks to this line:
https://github.com/coq-community/docker-coq/blob/379f1934489c087e9da6c7b7e740c5313d0aa8a4/coq/dev/Dockerfile#L24
@Karl Palmskog do you have some experience about this part of opam semantics ?
otherwise I'll do some experiments in the upcoming days to better figure out this
Karl Palmskog (Jul 15 2024 at 20:25):my very informal understanding of opam semantics is that only changes to package definitions will trigger the "upstream changes" issue
Karl Palmskog (Jul 15 2024 at 20:29):it looks like it could still be related to Menhir somehow, since Francois recently did a lot of changes to the repo and a release. However, the packages related to menhir in extra-dev did indeed not change for quite some time.
Erik Martin-Dorel (Jul 15 2024 at 20:29):Yes, I see no recent change in:
https://github.com/coq/opam/blob/master/extra-dev/packages/menhir/menhir.dev/opam
Karl Palmskog (Jul 15 2024 at 20:30):could it be some change in a dependency of menhirLib, menhirSdk or menhir maybe?
Erik Martin-Dorel (Jul 15 2024 at 20:30):so maybe a good "workaround" for the issue I mention (if my intuition is correct) would be to impose that
elpi 1.19.4 only use released versions of menhir, not menhir.dev
Karl Palmskog (Jul 15 2024 at 20:30):that could work, yes
Erik Martin-Dorel (Jul 15 2024 at 20:32):there are several ways to do this. Either I just pin a version of menhir in the Dockerfile.
Or we add upper bounds somewhere in the opam repositories
Erik Martin-Dorel (Jul 15 2024 at 20:33):In any case, too late to decide/implement this tonight :sweat_smile: but from now on, thanks for the quick feedback ! :+1:
Last updated: Oct 13 2024 at 01:02 UTC