Fix wrong conflict explanation messages that talk about formulas that do not appear in the requested packages

[kit-ty-kate]

Pushed to the edge by yet another wrong/bad explanation message on different forums (#5130 (comment)), i took a couple days off my weekend to try and see if i could recode the conflict explanation code. I'm still doing it but in the process i realized there seems to be a very easy fix for one of the most annoying and common wrong explanation message (see example in the link above)

$ cat opam
opam-version: "2.0"
name: "test"
depends: [
  "base" {= "0.16.2"}
]
$ opam-2.2.0-alpha3 install --dry-run .
[ERROR] Package conflict!
  * Missing dependency:
    - base < v0.9.0
    no matching version

No solution found, exiting
$ opam-this-branch install --dry-run .
[ERROR] Package conflict!
  * Missing dependency:
    - base = 0.16.2
    no matching version

No solution found, exiting

---

TODO:

• Add a test (Conflict messages #5130 (comment) and similar are a perfect showcase of the fix)

[kit-ty-kate]

This was the only use of that function. Do we want to also remove it from OpamFormula? Given this function obviously has a serious bug, should we also debug whether it comes from this one or OpamFormula.gen_formula as we might want to remove or fix this one too?

[kit-ty-kate]

I chose this route because trying to debug this code sounds like a time sink

[AltGr]

obviously has a serious bug

can you be more explicit ?

I believe the issue may come not from the function itself, but from the fact that it generates a formula that results in the same partition of the set of packages that it was supplied. And that already excludes unavailable packages, which is where the results may become misleading once put in the final message.
This is all IIRC 😬, it's been a while.

The fundamental issue, again IIRC, is that we are trying to extract the reasons from a graph of dependencies between individual package versions, at a point where the initial formulas have already been evaluated ; when walking the dependency chains we are performing set operations, etc. At this stage, recovering the initial formula is not really possible (and after set union, maybe not even desirable).

Of course here the focus case seems to be on singletons, where the results seem very dumb: we may want to special-case this case of figure — I believe the formula generation function would favor inequalities when only the upper or lower bound matches, we could prefer equalitites (both being correct mathematically, either being potentially wrong w.r.t. the original formula, which we can't retrieve at this point).

I thought this was no longer the case, but at some point, when encoding the Cudf constraint, we would transpose a never-matching constraint with < min-version for lack of a better thing. This transpiring into the user messages is pretty bad.

I chose this route because trying to debug this code sounds like a time sink

Yeah, I agree 😓

[AltGr]

Hm the original reason for this was to avoid extremely long enumerations of all the possible versions of a package. I am wondering why that doesn't seem to be the case here ?
IIRC that would happen in particular on versions of core, maybe ocaml as well. core in particular is bringing multiple layers of dependent packages with synchronised versions.

[AltGr]

obviously has a serious bug

can you be more explicit ?

I believe the issue may come not from the function itself, but from the fact that it generates a formula that results in the same partition of the set of packages that it was supplied. And that already excludes unavailable packages, which is where the results may become misleading once put in the final message.
This is all IIRC 😬, it's been a while.

The fundamental issue, again IIRC, is that we are trying to extract the reasons from a graph of dependencies between individual package versions, at a point where the initial formulas have already been evaluated ; when walking the dependency chains we are performing set operations, etc. At this stage, recovering the initial formula is not really possible (and after set union, maybe not even desirable).

Of course here the focus case seems to be on singletons, where the results seem very dumb: we may want to special-case this case of figure — I believe the formula generation function would favor inequalities when only the upper or lower bound matches, we could prefer equalitites (both being correct mathematically, either being potentially wrong w.r.t. the original formula, which we can't retrieve at this point).

I thought this was no longer the case, but at some point, when encoding the Cudf constraint, we would transpose a never-matching constraint with < min-version for lack of a better thing. This transpiring into the user messages is pretty bad.

I chose this route because trying to debug this code sounds like a time sink

Yeah, I agree 😓

[kit-ty-kate]

Superseded by #6106