opam confuses "A depends on B" with "B depends on A"

[Blaisorblade]

An example where opam's actually proposing the wrong choice:

$ opam remove coq-dot-iris
The following actions will be performed:
  ⊘ remove    coq-dot-iris  ~dev*
  ↻ recompile coq-autosubst 1.7*  [uses coq-dot-iris]
$ opam info coq-autosubst --field depends
"coq" {(>= "8.10" & < "8.16~") | (= "dev")}
$ opam info coq-dot-iris --field depends
"coq" {(>= "8.13.0" & < "8.15~")}
"coq-iris" {= "3.6.0"}
"coq-autosubst" {= "1.7"}

Where coq-dot-iris is a locally installed copy of https://github.com/Blaisorblade/dot-iris/blob/master/coq-dot-iris.opam — I swear that's not meant to be a Bobby tables, and even passes opam lint. (I see the name is mistaken, and I'm testing if that makes a difference).

The above was maybe cheating a bit, as I had removed the default repo from the switch (to avoid updating ocaml yet). But if I put if back, I see that all dependencies of coq-dot-iris are inverted, claiming that coq, coq-iris and coq-autosubst depend on coq-dot-iris.

$ opam remove coq-dot-iris
The following actions will be performed:
  ↻ recompile ocaml-variants      4.10.2+flambda         [upstream or system changes]
  ⊘ remove    coq-dot-iris        ~dev*
  ↻ recompile ocaml-config        1                      [uses ocaml-variants]
  ↻ recompile ocaml               4.10.2                 [uses ocaml-variants]
  ↻ recompile seq                 base                   [uses ocaml]
  ↻ recompile ocamlfind           1.9.1                  [uses ocaml]
  ↻ recompile dune                2.9.1                  [uses ocaml]
  ↻ recompile camlp5              7.14                   [uses ocaml]
  ↻ recompile zarith              1.12                   [uses ocaml]
  ↻ recompile num                 1.4                    [uses ocaml]
  ↻ recompile base-bytes          base                   [uses ocaml]
  ↻ recompile stdlib-shims        0.3.0                  [uses ocaml]
  ↻ recompile sexplib0            v0.14.0                [uses ocaml]
  ↻ recompile result              1.5                    [uses ocaml]
  ↻ recompile re                  1.10.3                 [uses ocaml]
  ↻ recompile ppx_derivers        1.2.1                  [uses ocaml]
  ↻ recompile ocaml-compiler-libs v0.12.4                [uses ocaml]
  ↻ recompile mmap                1.1.0                  [uses ocaml]
  ↻ recompile csexp               1.5.1                  [uses ocaml]
  ↻ recompile cppo                1.6.8                  [uses ocaml]
  ↻ recompile coq                 8.13.2+flambda+bedrock [uses coq-dot-iris]
  ↻ recompile ppxlib              0.24.0                 [uses ocaml]
  ↻ recompile dune-configurator   2.9.1                  [uses ocaml]
  ↻ recompile ocplib-endian       1.2                    [uses ocaml]
  ↻ recompile coq-stdpp           1.7.0                  [uses coq]
  ↻ recompile coq-autosubst       1.7*                   [uses coq-dot-iris]
  ↻ recompile ppx_deriving        5.2.1                  [uses ocaml]
  ↻ recompile lwt                 5.4.2                  [uses ocaml]
  ↻ recompile coq-iris            3.6.0*                 [uses coq-dot-iris]
  ↻ recompile elpi                1.13.8                 [uses ocaml]
===== ↻ 29   ⊘ 1 =====
Do you want to continue? [Y/n] n

$ opam config report
# opam config report
# opam-version         2.1.2
# self-upgrade         no
# system               arch=arm64 os=macos os-distribution=homebrew os-version=12.1
# 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                 11
# repositories         4 (http), 7 (local), 4 (version-controlled) (default repo at bb9ffa66)
# pinned               1 (git), 4 (version)
# current-switch       4.10.2+flambda
# ocaml:native         true
# ocaml:native-tools   true
# ocaml:native-dynlink true
# ocaml:stubsdir       /Users/pgiarrusso1/.opam/4.10.2+flambda/lib/ocaml/stublibs:/Users/pgiarrusso1/.opam/4.10.2+flambda/lib/ocaml
# ocaml:preinstalled   false
# ocaml:compiler       4.10.2+flambda

[Blaisorblade]

swear that's not meant to be a Bobby tables, and even passes opam lint. (I see the name is mistaken, and I'm testing if that makes a difference).

FWIW, it seems to make a difference. I fixed the package (Blaisorblade/dot-iris@89c3c2b), reinstalled it (and recompiled coq-autosubst with it, see below), then everything became normal again...

$ opam repo remove default
$ opam install .
$ opam repo remove default
Repositories removed from the selections of switch 4.10.2+flambda. Use '--all' to forget about them altogether.
(0 : 00:46:51) pgiarrusso1@KillBill(arm64):~/git/gDOT/dot-iris$ opam install .
[NOTE] Ignoring uncommitted changes in /Users/pgiarrusso1/git/gDOT/dot-iris (`--working-dir' not active).
[coq-dot-iris.~dev] synchronised (no changes)
The following actions will be performed:
  ↻ recompile coq-autosubst 1.7*  [upstream or system changes]
  ↻ recompile coq-dot-iris  ~dev*
===== ↻ 2 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
⬇ retrieved coq-autosubst.1.7  (cached)
⬇ retrieved coq-dot-iris.~dev  (no changes)
⊘ removed   coq-dot-iris.~dev
⊘ removed   coq-autosubst.1.7
∗ installed coq-autosubst.1.7
∗ installed coq-dot-iris.~dev
Done.

[AltGr]

I don't know if you can still reproduce, but the output of --cudf outfile would be useful (it includes the actual graph of actions in outfile-*.dot)

Worth noting is that there are 2 different things at play here:

• the actions themselves: these should be guaranteed correct unless there is a critical bug. They are derived mechanically from the package relationships and the result of the solver.
• the displayed "reasons" for the actions (in [square brackets]): these are generated after-the-fact through heuristics, based on the actions and their relationships. They are much more likely to be off, but that wouldn't affect the soundness of the switch.

The reason for the 2nd point is that the solvers we use (SMT, in general) are black boxes that don't justify their choices.If you use unconventional solver criteria like maximising downgrades, the reasons are unlikely to make sense.

[Blaisorblade]

• the actions themselves: these should be guaranteed correct unless there is a critical bug. They are derived mechanically from the package relationships and the result of the solver.

That would imply there's a critical bug? Because #5035 (comment) recompiles coq-autosubst for no valid reason — so maybe the data gets corrupted before being fed into the solver.

[Blaisorblade]

• the displayed "reasons" for the actions (in [square brackets]): these are generated after-the-fact through heuristics, based on the actions and their relationships. They are much more likely to be off, but that wouldn't affect the soundness of the switch.

Even taking that into account, the heuristics should not invent dependency edges that are outright absurd: coq does not depend on coq-dot-iris.

[AltGr]

Because #5035 (comment) recompiles coq-autosubst for no valid reason — so maybe the data gets corrupted before being fed into the solver.

The line ↻ recompile coq-autosubst 1.7* [upstream or system changes] hints that the package is pinned and opam detected changes that warrant recompilation. It doesn't have to be linked to your current command (opam install .), although if there is absolutely no relationship between the two opam may be able to skip this recompilation (we have improvements on that for the next release).

You can check those "pending recompilations" with opam reinstall --list-pending

As for the original confusing [uses coq-dot-iris], it's difficult to analyse without knowing your package graph: it's spurious in the sense that your further tests show that this recompilation needs to be done anyway. The heuristics inferred it from the fact that, in the graph of actions to be processed, the removal was to be done before the reinstallation. There have already been some tuning to this code since last release so it may be more precise now...

I had removed the default repo from the switch (to avoid updating ocaml yet)

Pro tip: you can use opam repo set-url default git+https://github.com/ocaml/opam-repository#HASH to fix the commit-HASH of the default repo you want to use. Or use opam switch set-invariant to lock the ocaml version you want.

[Blaisorblade]

Thanks for the tips. I tried to reproduce this, got more confusing outputs, but failed to identify any sensible patterns (or to capture cudf files for the strange results). I don't think I have tweaked my solver criteria:

# Solver: builtin-mccs+glpk
# Criteria: -removed,-count[avoid-version,changed],-count[version-lag,solution],-count[missing-depexts,changed],-new

[Blaisorblade]

Self-closing as unactionable.