rocq 9.0+rc1 pulls in rocq-stdlib "dev" version

[RalfJung]

I am trying the RC for Rocq 9.0, and it turns out that opam install rocq.9.0+rc1 pulls in the dev version of rocq-stdlib. That's not what I expected, I don't want it to fetch the latest version from git (which has to be rebuilt after every opam update). I know I can work around this with pins, but then I will have to remember to update 2 pins (rocq and rocq-stdlib) every time I change the Rocq version, which is not great.

Expected behavior would be that it automatically installs version 9.0+rc1 of rocq-stdlib.

[erikmd]

I believe it's "expected", because if you don't say anything more to opam than "install rocq.9.0+rc1", given this kind of flexibility is allowed by rocq-prover.opam:

depends: [
…
  "rocq-core" {= version}
  "rocq-stdlib"
…
]

opam will just try to install if possible, the latest version of its dependencies. And "9.0+rc1" ≤ "dev" lexicographically.

To avoid this, I especially see one way:

Add another pinning beforehand,

opam pin add -n -y -k version rocq-stdlib 9.0+rc1

[RalfJung]

Yeah I understand why opam behaves that way, but IMO the dependencies should be set up differently to avoid this.

Having to pin rocq and rocq-stdlib separately all the time quickly gets old, and is also easy to get wrong.