pin is being ignored; opam installs the wrong version of a package

[RalfJung]

I have told opam to pin coq to 8.19.dev. Nevertheless, it now installed version 8.18.dev of Coq.

I saw this happen on CI, in this job:

$ opam pin add -y -n -k version coq 8.19.dev
[...]
$ opam upgrade -y builddep/
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-iron-builddep.~dev] synchronised (no changes)
The following actions will be performed:
  - recompile coq                8.18.dev [upstream or system changes]
  - recompile coq-stdpp          dev*     [upstream or system changes]
  - recompile coq-iris           dev*     [upstream or system changes]
  - recompile coq-iris-heap-lang dev*     [upstream or system changes]
  - recompile coq-iron-builddep  ~dev*
===== 5 to recompile =====

This is pretty much the worst-case bug for using opam on CI: it silently installs the wrong thing, so even if the tests pass I can't be sure that they passed for the intended package versions. I have no idea how often this happens; usually I don't double check our CI logs. I just noticed this coincidentally while doing some mass-rebuild tests.

# opam config report
# opam-version         2.1.5 
# self-upgrade         no
# system               arch=x86_64 os=linux os-distribution=debian os-version=10
# solver               builtin-mccs+glpk
# install-criteria     -removed,-count[avoid-version,changed],-count[version-lag,request],-count[version-lag,changed],-count[missing-depexts,changed],-changed
# upgrade-criteria     -removed,-count[avoid-version,changed],-count[version-lag,solution],-count[missing-depexts,changed],-new
# jobs                 20
# repositories         4 (http), 1 (version-controlled) (default repo at 0286027b)
# pinned               6 (git), 1 (rsync), 2 (version)
# current-switch       default
# ocaml:native         true
# ocaml:native-tools   true
# ocaml:native-dynlink true
# ocaml:stubsdir       /builds/iris/iron/_opam/default/lib/ocaml/stublibs:/builds/iris/iron/_opam/default/lib/ocaml
# ocaml:preinstalled   false
# ocaml:compiler       4.14.0+options+flambda

[RalfJung]

Ah looks like in the next build step (opam upgrade -y) it then does properly take into account the pins, so it doesn't end up doing CI with the wrong version. Still strange that it would recompile coq but build a version that contradicts the pin.

[kit-ty-kate]

Let’s reopen this for now and figure out why it has this behaviour. I do agree that it sounds pretty buggy behaviour on first glance.

[RalfJung]

Rerunning the job after bumping the coq requirement of some dependencies, it now behaves as expected:

$ opam upgrade -y builddep/ dune coq
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-iron-builddep.~dev] synchronised (no changes)
[coq.8.19.dev] synchronised (git+https://github.com/coq/coq.git#v8.19)
The following actions will be performed:
  - upgrade   coq-core           8.18.dev to 8.19.dev  [required by coq]
  - upgrade   coqide-server      8.18.dev to 8.19.dev  [required by coq]
  - upgrade   coq-stdlib         8.18.dev to 8.19.dev  [required by coq]
  - upgrade   coq                8.18.dev to 8.19.dev*
  - recompile coq-stdpp          dev*                  [uses coq]
  - recompile coq-iris           dev*                  [uses coq]
  - recompile coq-iris-heap-lang dev*                  [uses coq-iris]
  - recompile coq-iron-builddep  ~dev*
===== 4 to recompile | 4 to upgrade =====

So it looks like the constraints of some of the packages (<8.19) are taking precedence over the pin, without a warning being printed.

[rjbou]

It seems to be fixed on 2.2.0~alpha, can you check ?

todo for opam devs: we need to add a test for this case.

[RalfJung]

That's great to hear!

This is on CI so I can't easily check this, and I'll not migrate our CI to an alpha version. Once a 2.2 stable release is out we can see how it fares on our CI.