Version SAT | Hacker News Reader

Version SAT

research.swtch.com

103 pointsjsnell19 comments

> Dart’s pub includes a simple backtracking solver that often takes a long time.

I'll note two things:

1. The backtracking solver isn't that simple. It's got a handful of pretty smart heuristics that we've added over time to help it get stuck.

2. It doesn't get stuck very often. It does happen. In particular, our ecosystem has one package that is very heavily depended on and also frequently ships breaking changes, which is always a recipe for version solver pain.

But pub works fine for probably >99% of invocations of it. Installing dependencies is a gating issue for getting any work done, so if pub was getting stuck often, users would be screaming at us.

Also, Natalie, the other half of the pub team, put together a comparable proof of version solving being equivalent to 3-SAT a year or two ago, but I can't seem to find it now.

Personally, I think the idea of treating breaking versions of packages as distinct and allowing them to co-exist is interesting but I worry about the usability impact of it. It will be very confusing for users if objects flow between those two packages and you get type errors like "Expected type Foo but got Foo." Good error messages can help a lot, though.

> It's got a handful of pretty smart heuristics that we've added over time to help it get stuck.

I assume you mean NOT get stuck? Or do you mean something else like settling on a solution?

Heh, oops, yes. Help it find a solution. :)

Leaving my mistake to bear my shame publicly.

Hi Bob, Agree about "simple" being a bad choice of name. What I meant is that it's not one of the crazy souped up SAT solving algorithms directly. I'll drop "simple".

FWIW we've seen those kinds of type errors in Go already with vendoring, which lets you have multiple copies of the same package. Good errors are essential (and we only get them half right).

Thanks.

Relevant: Russ Cox, the blog author is one of the core members of the Go team. Russ gave a great talk on challenges with code refactoring at GothamGo last month: - writeup https://talks.golang.org/2016/refactor.article - video https://www.youtube.com/watch?v=h6Cw9iCDVcU

A group of community members have been working on a proposal for a package manager for Go. Sam Boyer also wrote an article about their progress here: https://blog.gopheracademy.com/advent-2016/saga-go-dependenc...

Possibly related: http://wiki.apidesign.org/wiki/LibraryWithoutImplicitExportI.... This one seems to avoid the NP-completeness by giving up when it encounters a conflict between major versions of the same package. (instead of trying to figure out whether it could modify the solution to avoid the conflict by upgrading/downgrading some packages).

In the context of language package managers avoiding NP-completeness is interesting: if you have a global repository then you have to deal with conflicts in some way, however per-project repositories could try to get around limitation #4 (2 different versions of same package allowed to be installed). Whether it is desirable to do so is another matter though, you'd end up with various buggy versions of same package installed, never knowing whether you've fully upgraded to the fixed version...

Treating different major versions as different packages is interesting though, and happens to some extent in system packages already (e.g. both python2 and python3 can coexist)

> Treating different major versions as different packages

For emphasis, because I think that's what should ideally happen.

Wondering how Nix plays into this. I'm no expert on it, but IIUC it attacks point 4 of Russ' list: "Two different versions of a package cannot be installed simultaneously." Nix allows you to install multiple versions of a package, but I'm not sure how that affects its dependency resolution.

Nix allows two packages to exist simultaneously on the filesystem and can even put both in your $LANGPATH (i.e., PYTHONPATH, CLASSPATH, GOPATH, etc), but the linker/runtime will still only look at the first package to resolve correctly, ignoring the second. In other words, Nix just sets up your environment--the language tools still have the final say about how they resolve multiple dependencies within that environment.

I suppose one thing to keep in mind is the interface that the packaged software provides. If packages A and B provide standalone binaries /bin/A and /bin/B, and package C depends on both, then the dependencies of A and B are pretty much isolated: each can use their own versions of whatever they like, and C can invoke both binaries.*

On the other hand, if A and B provide (some sort of) libraries which C imports, then their dependencies may be exposed by appearing in the pool of libraries available to C. This is certainly the case for Haskell, where all of a library's dependencies accumulate in the ghc-pkg database and multiple versions of a library aren't allowed in the same program. As you say, such things are existing problems in external, language-specific tools, and aren't caused by Nix; although Nix may provide a useful abstraction to better manage such problems.

* There may be application-specific problems at runtime, e.g. if A and B try to de/serialise each other's data, but I'd count that as a bug: if A and B are meant to be standalone then they're buggy, as their I/O formats should be more robust; on the other hand, if A and B are meant to be used together then the packaging is buggy: A and B should expose their shared dependency as a parameter, and C should pass in the same version to both.

Nix has no dependency resolution: all dependencies are specified exactly for every package.

The reason this is tractable is that Nix packages are written in an expressive language. Most package definitions are actually functions, which accept their dependencies as arguments. Such functions provide flexibility, making it easy to switch out dependencies or perform other changes, and are often passed around using higher-order functions. The closest thing to dependency resolution is to take the fixed-point of a function, which is used to populate each package's dependency arguments using the other packages (which we're also populating the arguments of; this relies on Nix being lazy!).

For example, the `cabal2nix` tool can read a Haskell '.cabal' file and create a Nix function, which accepts dependencies and returns a package. We can turn this into a concrete package by specifying a version of Haskell to use (e.g. `haskell.ghc7103` for GHC 7.10.3, `haskell.ghc801` for GHC 8.0.1, `haskell.ghcjs` for GHCJS, etc.); each contains a higher-order function `callPackage`, which we pass our generated function to, along with any non-default overrides.

For example, we can run the command:

    nix-shell -p "(haskell.ghc7103.callPackage ($(cabal2nix /path/to/project.cabal)) { some-dep = my-version-of-some-dep; })"

This will drop us into a bash shell where the Haskell project at /path/to/project.cabal has been built using GHC 7.10.3, with default versions of all dependencies except for "some-dep" which we override to be some other package. If, for example, our Haskell package defines a bunch of executables, they'll be available in this shell's $PATH.

There are also higher-order functions like `ghcWithPackages` for defining Haskell environments with pre-populated package databases, `override` which takes the fixed-point of a set of packages (so overriding "foo" ensures that all packages depending on "foo" get our version, transitively), etc.

Red Hat's DNF package manager (which does not stand for "disjunctive normal form") and SUSE's Zypper package manager both use minisat for dependency resolution for RPMs.

https://lwn.net/Articles/503581/

https://en.opensuse.org/openSUSE:Libzypp_satsolver

I believe the conda package manager also has a SAT solver [1]

[1] https://www.continuum.io/blog/developer/new-advances-conda-0

one more, FreeBSD's pkg uses picosat - https://github.com/freebsd/pkg/tree/master/external/picosat

It would be really awesome if the SAT Competitions required open source licenses instead of academically-restricted licenses. It would be amazing if we could use {Lin,Plin,Treen}geling solvers or the like for open source software like this.

I think you'd find you wouldn't have any serious entries in the competitions any more.

Several of those entrants have open source licenses.

The Solaris package manager (aka "pkg(5)") also uses a SAT solver for dependency resolution (minisat):

https://blogs.oracle.com/barts/entry/satisfaction https://docs.oracle.com/cd/E36784_01/html/E36856/glulp.html

However, a large drawback to SAT solutions is friendly messaging when no solution is found; just as hard as doing the initial dependency analaysis if not more difficult.

There are also interesting corner cases such as "metapackages" (in Debian terms) and alternatives, etc.

https://docs.oracle.com/cd/E53394_01/html/E54820/dependtypes...

For pkg(5), almost all of the magic is here:

https://java.net/projects/ips/sources/pkg-gate/content/src/m...

Gosh I wish someone would solve this problem in the Java ecosystem. I work at a BigCo and the developer years that are lost each year to old fashioned JAR hell is astonishing, and it's only getting worse as runtime environments grow in complexity, we run in increasingly managed contexts which violate core assumptions of build systems, code dependencies are getting more complex, some people don't model package dependencies correctly, etc. Please, someone solve this and convince everyone to use it!

Reply on news.ycombinator.com