opam updates a package, then forgets that it did so

[RalfJung]

I don't know how to reproduce this, but it's not the second time this has happened. Here are some excerpts from my terminal log:

$ make builddep clean # will invoke `opam install`
# Installing builddep packages.
[coq-gpfsl-builddep.dev] synchronised (no changes)
[coq-orc11-builddep.dev] synchronised (no changes)
The following actions will be performed:
  ↗ upgrade   coq-stdpp                  dev.2023-09-21.2.7f6df4fa to dev.2023-10-03.0.83c8fcbf [required by coq-orc11-builddep]
  ↗ upgrade   coq-iris                   dev.2023-09-26.0.32e79061 to dev.2023-10-03.0.70b30af7 [required by coq-gpfsl-builddep]
  ↻ recompile coq-orc11-builddep         dev*
  ↗ upgrade   coq-iris-heap-lang         dev.2023-09-26.0.32e79061 to dev.2023-10-03.0.70b30af7 [uses coq-iris]
  ↻ recompile coq-gpfsl-builddep         dev*
  ↻ recompile coq-iris-examples-builddep ~dev*                                                  [uses coq-iris-heap-lang]
===== ↻ 3   ↗ 3 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-iris-examples-builddep.~dev  (no changes)
⬇ retrieved coq-stdpp.dev.2023-10-03.0.83c8fcbf  (git+https://gitlab.mpi-sws.org/iris/stdpp.git#83c8fcbf63dc432aa464bc26a88a2ad883f15292)
⬇ retrieved coq-iris.dev.2023-10-03.0.70b30af7  (git+https://gitlab.mpi-sws.org/iris/iris.git#70b30af7df05921be85e84a32c02694b5503e1ef)
⬇ retrieved coq-iris-heap-lang.dev.2023-10-03.0.70b30af7  (git+https://gitlab.mpi-sws.org/iris/iris.git#70b30af7df05921be85e84a32c02694b5503e1ef)
⊘ removed   coq-gpfsl-builddep.dev
⊘ removed   coq-iris-examples-builddep.~dev
⊘ removed   coq-iris-heap-lang.dev.2023-09-26.0.32e79061
⊘ removed   coq-iris.dev.2023-09-26.0.32e79061
⊘ removed   coq-orc11-builddep.dev
⊘ removed   coq-stdpp.dev.2023-09-21.2.7f6df4fa
∗ installed coq-stdpp.dev.2023-10-03.0.83c8fcbf
∗ installed coq-orc11-builddep.dev
∗ installed coq-iris.dev.2023-10-03.0.70b30af7
∗ installed coq-gpfsl-builddep.dev
∗ installed coq-iris-heap-lang.dev.2023-10-03.0.70b30af7
∗ installed coq-iris-examples-builddep.~dev
Done.
[...]
$ opam list
# Packages matching: installed
# Name                     # Installed               # Synopsis
base-bigarray              base
base-threads               base
base-unix                  base
cairo2                     0.6.4                     Binding to Cairo, a 2D Vector Graphics Library
camlp-streams              5.0.1                     The Stream and Genlex libraries for use with Camlp4 and Camlp5
conf-adwaita-icon-theme    2                         Virtual package relying on adwaita-icon-theme
conf-cairo                 1                         Virtual package relying on a Cairo system installation
conf-findutils             1                         Virtual package relying on findutils
conf-gmp                   4                         Virtual package relying on a GMP lib system installation
conf-gtk3                  18                        Virtual package relying on GTK+ 3
conf-gtksourceview3        0+2                       Virtual package relying on a GtkSourceView-3 system installation
conf-pkg-config            3                         Check if pkg-config is installed and create an opam switch local pkgconfig folder
coq                        8.17.1                    The Coq Proof Assistant
coq-autosubst              dev                       Coq library for parallel de Bruijn substitutions
coq-core                   8.17.1                    The Coq Proof Assistant -- Core Binaries and Tools
coq-equations              1.3+8.17                  A function definition package for Coq
coq-ext-lib                0.11.8                    A library of Coq definitions, theorems, and tactics
coq-gpfsl-builddep         dev                       pinned to version dev at file:///home/r/Dokumente/Unisachen/iris/coq-users/gpfsl/builddep
coq-iris                   dev.2023-09-26.0.32e79061 A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-iris-examples-builddep ~dev                      pinned to version ~dev at file:///home/r/Dokumente/Unisachen/iris/coq-users/examples/builddep
coq-iris-heap-lang         dev.2023-09-26.0.32e79061 The canonical example language for Iris
coq-itree                  5.1.1                     Library for representing recursive and impure programs with equational reasoning
coq-orc11-builddep         dev                       pinned to version dev at file:///home/r/Dokumente/Unisachen/iris/coq-users/gpfsl/builddep
coq-paco                   4.2.0                     Coq library implementing parameterized coinduction
coq-record-update          0.3.0                     Generic support for updating record fields in Coq
coq-stdlib                 8.17.1                    The Coq Proof Assistant -- Standard Library
coq-stdpp                  dev.2023-09-21.2.7f6df4fa An extended "Standard Library" for Coq
coqide                     8.17.1                    The Coq Proof Assistant --- GTK3 IDE
coqide-server              8.17.1                    The Coq Proof Assistant, XML protocol server
csexp                      1.5.1                     Parsing and printing of S-expressions in Canonical form
dune                       3.3.1                     pinned to version 3.3.1
dune-configurator          3.5.0                     Helper library for gathering system configuration
lablgtk3                   3.1.3                     OCaml interface to GTK+3
lablgtk3-sourceview3       3.1.3                     OCaml interface to GTK+ gtksourceview library
ocaml                      4.14.0                    The OCaml compiler (virtual package)
ocaml-config               2                         OCaml Switch Configuration
ocaml-option-flambda       1                         Set OCaml to be compiled with flambda activated
ocaml-variants             4.14.0+options            Official release of OCaml 4.14.0
ocamlfind                  1.9.5                     A library manager for OCaml
zarith                     1.12                      Implements arithmetic and logical operations over arbitrary-precision integers

As you can see, the installation of coq-stdpp version dev.2023-10-03.0.83c8fcbf completed successfully, but afterwards opam list still shows the old version number (and same for the other packages that got updated). The actually installed version is indeed dev.2023-10-03.0.83c8fcbf (I can tell by importing the files), so somehow opam installed the new version and then neglected to properly register that in its database.

# opam config report
# opam-version         2.1.4 
# self-upgrade         no
# system               arch=x86_64 os=linux os-distribution=debian os-version=n/a
# 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                 8
# repositories         4 (http), 1 (local), 1 (version-controlled) (default repo at d45d933f)
# pinned               13 (rsync), 1 (version)
# current-switch       /home/r/Dokumente/Unisachen/iris/coq-users/examples
# ocaml:native         true
# ocaml:native-tools   true
# ocaml:native-dynlink true
# ocaml:stubsdir       /home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/ocaml/stublibs:/home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/ocaml
# ocaml:preinstalled   false
# ocaml:compiler       4.14.0+options+flambda

[rjbou]

Does you script have some switch manipulation ? Does it use the current switch ?

[RalfJung]

It's just a single opam install, no switch manipulation.

[kit-ty-kate]

can you list the opam repository that you used here to get coq-stdpp.dev.2023-10-03.0.83c8fcbf ?

[RalfJung]

Here's opam repo list:

 1 iris-dev     git+https://gitlab.mpi-sws.org/FP/opam-dev.git
 2 coq-released https://coq.inria.fr/opam/released
 3 default      https://opam.ocaml.org/

coq-stdpp.dev.2023-10-03.0.83c8fcbf comes from iris-dev.

[kit-ty-kate]

I tried building https://gitlab.mpi-sws.org/iris/gpfsl manually with the same steps you have in CI and I can’t reproduce the issue. Do you have the link to the CI buildlog? I couldn’t find it.

The only weird thing we can see right now, that could be related is that seemingly all of the opam files in https://gitlab.mpi-sws.org/iris/opam have their version field set to dev. When inside a repository where the directory name gives the version already they should be ignored, but maybe there is a bug somewhere that makes them resurface randomely.

Could you try removing the version: "dev" lines from all the opam file in this repository and see if that helps?
Even though I would still not understand how that happens randomely (i tried to have a small reproduction case with just this, to no avail), that would help give some direction to debug the problem further.

[RalfJung]

Thanks for investigating!

Yeah I don't think I can reproduce the issue. It just happened that one time, and I think it happened before, a few months ago. Most of the time make builddep works just fine, but sometimes opam gets really confused.

Could you try removing the version: "dev" lines from all the opam file in this repository and see if that helps?

That repo is auto-generated so this is not really easily possible. Also the issue isn't reproducible and it occurs only rarely so I wouldn't even know if it helps...

I guess we could try to adjust the auto-publisher to remove the version field from new versions that we add. But I'm quite happy that so far we can just copy the opam file (appending the URL info at the end) and I'm not looking forward to mucking about with grep/sed patching the opam file...