portable lock directories should pick the same version for cross-platform packages

[Alizter]

Currently portable lock directories cannot always pick, without further direction, the same package version across platforms.

This is because at the time of writing we are doing multiple separate solves. These will be merged into a single solve once #13645 is addressed.

As discussed in:

• Improve UX around portable lockdirs #11868

We should constrain the single solve so that packages that appear in multiple platforms share the same version.

@art-w has an idea on how to handle this in a single SAT problem.

Importantly we still want to allow some packages to only appear for a subset of platforms, however they should still share the same version. Take for example unix-only-package not being picked on Windows.

If users would like differing versions of the same package across multiple platforms, they are welcome to use a second (or more) lock file with the separate solution for the separate platforms.

We should also consider if we want to keep the version number in the directory structure of the lock directory. This might need some further discussion as I've heard from some users that they find it useful, but ultimately it is redundant information since the version can be found in the .pkg file. We should consider what git diff will observe.

[art-w]

With one SAT problem per platform, I don't know how to constrain the package versions to be the same across platforms (without a hack that would fail to find solutions in general, by enforcing specific package versions too early to be correct). But @Alizter has made progress on how to refactor the multiple SAT problems into a single SAT problem to solve all the platforms at once (but still solving for each platform independently, so the refactoring produces exactly the same solutions as before). In practice, this refactoring changes the SAT variables from representing <package_name> is <version> (for a single platform at a time) to on <platform>: <package_name> is <version> for each platform.

(so we might still get the undesirable solution with both on linux: lwt is 6.0 and on windows: lwt is 5.0 selected, but now these two boolean variables live in the same SAT universe so we'll be able to constrain them further to avoid this.)

Then, to ensure that different platforms pick exactly the same package version (and not different ones), we need to connect the platform-specific SAT variables together. For each package/version, we can introduce a new SAT variable called somewhere: <package_name> is <version> (with the standard constraint "at most one version is selected" if multiples are available, exaclty like the code already constrains on linux: lwt is <version> to pick exactly one version).

These new variables will serve to track the uniquely selected version of each package. If the variable somewhere: foo is 1.0 is true, then we'll know that at least one platform selected foo.1.0. We achieve this by adding new SAT constraints for each platforms, packages and versions:

(on <platform>: <pkg> is <version>) implies (somewhere: <pkg> is <version>)

For example: (on linux: lwt is 6.0) implies (somewhere: lwt is 6.0)
and (on windows: lwt is 5.0) implies (somewhere: lwt is 5.0).
So if linux picks lwt.6.0 and windows picks lwt.5.0, we get both (somewhere: lwt is 6.0) and (somewhere: lwt is 5.0), causing the SAT solver to realize that multiple lwt versions were picked, which is illegal (so backtracking follows, although in practice the SAT solver will do early deduction such that it'll not need to backtrack on such an obvious conflict).

(In pseudo-code, the sat solver handles constraints like x implies y as two deduction callbacks "if x becomes true, then deduce that y is true" and "if y becomes false, then deduce that x must be false". So I expect that the added implications will cut the search space significantly by tying together the per-platforms variables/constraints.)

Important: We do NOT want the reverse implication (somewhere: inotify is 2.0) implies (on windows: inotify is 2.0) as this would force windows to install the unavailable package inotify! With the right implication order however, we allow platforms to select a platform-specific package (in particular, both mac and linux may pick unix-only-pkg, as long as they agree on its version, while windows would be free to choose win-only-pkg)

Finally, when reading the solution produced by the solver, we don't have to change anything: we can ignore the somewhere: ... variables and keep on reading the more precise on <platform>: ... variables to know what is required by each platform. The "somewhere" variables are only an internal detail of the SAT representation to ensure version consistency across platforms.