Open RalfJung opened 2 years ago
I was able to reproduce with the following dockerfile:
FROM ocaml/opam
RUN sudo apt install -yy libgmp-dev
RUN sudo ln -f /usr/bin/opam-2.0 /usr/bin/opam
RUN opam repo add coq-released https://coq.inria.fr/opam/core-dev
RUN opam pin -k version coq 8.16.dev
RUN opam update --development
RUN opam pin remove -y -n coq
RUN opam pin add -y -n -k version coq 8.16.dev
RUN opam upgrade -y --show coq
I am pretty sure this used to work in the past, some time during the opam 2.0 cycle.
The above dockerfile is using opam 2.0.10. I also tested it using opam 2.0.0, opam 2.1.3 and opam master (https://github.com/ocaml/opam/commit/7c51e210400874e2fd2040892133c1a326475af5) and it all produced the same result. So I'm wondering if you instead did something different in the past. As far as i can see, it always worked like this and is not a regression.
Now, even if the steps are unlikely to be done by non-automated users (unpin and then re-pin on the same git remote), it can be something to be fixed.
Hm, it is true that we didn't always have the pin remove
step (we added it when we had trouble due to unexpected pins persisting via the cache), but I thought I had checked that caching still works after adding pin remove
.
Caching definitely still works for non-git versions, e.g. pinning to coq 8.15.2
.
Indeed not removing the Coq pin helps, thanks! I can work around the problem by exempting coq
from our 'unpin everything' logic (which is okay since we always pin Coq). It will probably still unnecessarily rebuild some other packages, but those are much quicker to build than Coq.
Interestingly, the other packages are not being rebuilt. They are slightly different pins, so this might be reproduced as follows:
RUN opam repo add coq-released https://coq.inria.fr/opam/core-dev
RUN opam pin -k version coq 8.16.dev
RUN opam pin add -y git+https://gitlab.mpi-sws.org/iris/stdpp
# now comes the re-run part
RUN opam init --no-setup --disable-sandboxing --reinit -y
RUN opam update --development
RUN opam pin remove -y -n coq-stdpp
RUN opam pin add -y git+https://gitlab.mpi-sws.org/iris/stdpp
RUN opam upgrade -y coq
RUN opam upgrade -y
Also coq-stdpp is not explicitly listed in the opam upgrade
, maybe that is the key difference? I recall having to explicitly add coq
there to ensure that if the git branch the package points to changes, then opam reinstalls the package as needed. But https://github.com/ocaml/opam/issues/3727 has been marked as fixed so maybe that is not needed any more. It's hard to test though since it needs the git repo to be pushed to.
I'm guessing that the bug comes from the fact that this is a git repository pointed by a regular package and we're doing opam pin -k version
on the package whereas stdpp is using opam pin -k git
directly.
The first case is fairly rare so I'm guessing that's why the bug hasn't popped-up before.
It still has something to do with the opam upgrade
arguments though; the following does not rebuild:
FROM ocaml/opam
RUN sudo apt install -yy libgmp-dev
RUN sudo ln -f /usr/bin/opam-2.0 /usr/bin/opam
RUN opam repo add coq-released https://coq.inria.fr/opam/core-dev
RUN opam pin -k version coq 8.16.dev
RUN opam pin add -y git+https://gitlab.mpi-sws.org/iris/stdpp
# now comes the re-run part
RUN opam init --no-setup --disable-sandboxing --reinit -y
RUN opam update --development
RUN opam pin remove -y -n coq
RUN opam pin -y -n -k version coq 8.16.dev
RUN opam upgrade -y
The following also does not rebuild though:
FROM ocaml/opam
RUN sudo apt install -yy libgmp-dev
RUN sudo ln -f /usr/bin/opam-2.0 /usr/bin/opam
RUN opam repo add coq-released https://coq.inria.fr/opam/core-dev
RUN opam pin -k version coq 8.16.dev
RUN opam pin add -y git+https://gitlab.mpi-sws.org/iris/stdpp
# now comes the re-run part
RUN opam init --no-setup --disable-sandboxing --reinit -y
RUN opam update --development
RUN opam pin remove -y -n coq
RUN opam pin remove -y -n coq-stdpp
RUN opam pin -y -n -k version coq 8.16.dev
RUN opam pin -y -n git+https://gitlab.mpi-sws.org/iris/stdpp
RUN opam upgrade -y --show coq-stdpp
so this only happens when it's both a regular package with a git URL (rather than a direct git pin), and the package name is listed after opam upgrade -y
.
Consider the following two CI builds using opam:
The opam root is preserved via the CI cache, and the git branch that
coq.8.16.dev
points at did not change between these two runs. And yet the second run rebuilds Coq. It doesn't even say why, it just saysWhat CI does at the start of the 2nd run is roughly
opam update --development
opam pin remove -y -n coq
opam pin add -y -n -k "version" "coq" "8.16.dev"
opam upgrade -y coq
opam upgrade -y
(There are more packages involved, but they are all further down the dependency tree, i.e. they depend on Coq, so they should not affect whether Coq gets rebuilt.)
This bug means that our CI rebuilds Coq all the time, and a huge amount of CI time is wasted doing that. (Even more so since for some projects we use flambda to make Coq faster, but that makes building Coq a lot slower -- which I thought would be fine because we have caching, but looks like somehow caching is broken.)
I am pretty sure this used to work in the past, some time during the opam 2.0 cycle.