Shards takes hours to resolve dependencies

[ysbaddaden]

Shards no longer crashes since #302 but now takes 77 minutes to resolve the following SPEC (copied from #282):

name: project
version: 1.1.1

dependencies:
  shainet:
    github: NeuraLegion/shainet
  myhtml:
    github: kostya/myhtml
  cadmium:
    github: watzon/cadmium
    branch: master
  fix:
    github: NeuraLegion/fix
  har:
    github: NeuraLegion/har
    branch: HEAD
  msgpack:
    github: benoist/msgpack-crystal
  kemal:
    github: kemalcr/kemal
    branch: HEAD
  kemal-basic-auth:
    github: kemalcr/kemal-basic-auth
  selenium:
    github: ysbaddaden/selenium-webdriver-crystal
    branch: HEAD
  stumpy_png:
    github: stumpycr/stumpy_png
    version: "~> 4.4.1"
  stumpy_utils:
    github: stumpycr/stumpy_utils

development_dependencies:
  ameba:
    github: veelenga/ameba
  mysql:
    github: crystal-lang/crystal-mysql

The SAT solver speed isn't a problem: it's fast enough and CaDiCaL for example, a state-of-the CDCL SAT solver doesn't magically solve the issue (shards still takes forever to resolve dependencies).

The problem is likely the high number of variables and clauses we pass to the solver. We can hardcode the "can install only one version at a time" constraint into the solver, to reduce the number of clauses to a very small number, but it still takes forever to resolve because we didn't reduce the number of variables.

Shards 0.9 already has optimizations in place to reduce the number of variables and clauses: it will only consider accessible dependencies and versions. The problem of the above SPEC is that there isn't any restriction so shards will reach and consider all dependencies and all their versions are accessible. This leads to 139 variables for the above SPEC and a thousand clauses, which leads to 77 minutes to resolve.

Note that adding a few version constraints like version: ~> x.y.0 to shainet, myhtml, ameba and mysql reduces those 77 minutes to 0.5 seconds. Yes, the performance improve is that dramatic.

[ysbaddaden]

The problem of the above SPEC is also that it has so few constraints, that almost every cases is possible, leading to too many possible solutions to choose from.

We can trick specialize the SAT solver by ordering variables (by dependency then by latest versions) allowing to skip entire variables and to find solutions quickly, but the dependency solver tries to exhaust the proposals to find the best outcome, the one closest to the ideal install (latest versions / as close as possible from the locked versions / no extraneous dependencies), which reduces this effort to ashes by trying every cases. Maybe it could return early when a best solution is found, possibly filtering extraneous dependencies by walking the dependency graph again?

In case of conflict it would still exhaust every possibility and fail, thought in case of conflicts there would probably be enough constraints that the number of variables is limited?

[ysbaddaden]

A trick could be to only consider the last few releases (or the locked version for conservative updates) for each shard without a version constraint or one that reaches too many versions.

Running the SAT solver should be fast because there are only a few variables and clauses. In case of failure, analyze the conflicts to add more versions and clauses, and try again. Possibly adding a --slow option to always select everything, along with a spinner to report that it's still running.

[straight-shoota]

Do you know how other dependency resolvers deal with this? This is unlikely a problem specific to shards. Or can dep mangeres with a centralized registry somehow circumvent this issue?

Anyway, the proposals to specialize the solver to descend from the latest version and/or limiting the amount of versions to the latest ones sounds reasonable. I'm not very familiar with shards' internals though, sorry.

[jackturnbull]

UX comment; is there any value (percieved or otherwise) in logging a warning with a possible solution when a certain number of variables & clauses are hit?

e.g. > The conflict resolver has detected a very large number of possibile depependency resolutions and as such may take a very long time to complete. One solution for this is to add a constraint (version: ~> x.y.0) to some of the dependencies in your shard.yaml to limit this number.

Wording just as an example.

[didactic-drunk]

How can I set maximum version in a published release? Releases use git tags which are immutable once published.

Example:

• I'm the author of lib "foo".
• foo v0.1 depends on bar.
• bar releases v2.0 changing the API.
• foo v0.1 should be able to limit bar to version < 2.0.

How or where can I specify this? Should extra dependency file exist outside the shard?

I assume doing this would limit the number of dependencies.

[straight-shoota]

Releases use git tags which are immutable once published.

Tags can be overridden to point to a different commit. So for full stability, you need to reference a specific commit, not a hash. For obvious reasons, it's not recommended to change a tag after its release, but it's possible.

Limiting the maximum version is simply specifying a < version restriction:

# foo/shard.yml

dependencies:
  git: bar/bar
  version: "< 2.0"

Done.

[straight-shoota]

@jackturnbull Yeah, such a message might be useful as an interim remedy. But the goal regarding UX should be to require no extra effort to limit versions. Shards should be able to figure everything out in an efficient manner.

[didactic-drunk]

For obvious reasons, it's not recommended to change a tag after its release, but it's possible.

From git tag --help:

However, Git does not (and it should not) change tags behind users back.
So if somebody already got the old tag, doing a git pull on your tree
shouldn't just make them overwrite the old one.

Limiting the maximum version is simply specifying a < version restriction:

Does that work with a range?

>= 1.0.0 && <= 5.0.0

[straight-shoota]

Yes, git won't update a local tag if it's been moved on the remote. But at every fresh checkout the updated tag will be used. So moving tags causes a lot of trouble.

Ranges are currently not supported, see SPEC). But there is #261.

[didactic-drunk]

Then changing the tag isn't a solution to setting maximum version for a dependency after publishing unless shards does a fresh checkout. Does it?

Otherwise, how can I set maximum version in a library I already published but a dependency has released new incompatible versions?

[jhass]

Release a new hotfix version and take care initially to scope the dependency to the current major version. Ask the dependency to do another minor/hotfix release restoring compatibility if they are in violation of semver. Also lets stick on topic here.

[ysbaddaden]

Don't yank versions, specifying a few version: ~> x.y.0 or version >= x.y.z for some dependencies in an app's shard.yml will usually avoid the issue, or at least tame it down to something acceptable (seconds or minutes, not hours). If libraries also specify some version:, at least when a breaking change occurs and the library isn't compatible anymore with older versions, this will help (we can skip those older releases).

Yet, despite being a good practice, this is only a workaround. The SAT based solver in Shards doesn't scale, and it won't get any better the more dependencies you add, and even with the workaround you'll eventually hit the same wall.

Other package managers are behaving correctly with many dependencies and versions, so the problem can be solved. I guess. I lack the knowledge.

There isn't much papers and literature on the subject, which is weird because package version resolution is essential to software and operating systems. The best read, and possibly the only one on the subject is PubGrub for Dart's pub:

• https://medium.com/@nex3/pubgrub-2fb6470504f
• https://github.com/dart-lang/pub/blob/master/doc/solver.md

If you can find a good paper or book on the subject, please share.

[bcardiff]

I would like to see more conservative constraints in the community been used. That would definitely help. Yet I would also like that the language version to also be considered in those constraints. This is working great in elm to note if a package is ready for a new language version. That means to potentially force authors to publish a new version of the package upon a release of the language.

Regarding the resolver itself, I see a couple of alternatives to avoid mastering building a SAT solver.

1. Port molinillo that is used in bundler and has an ad-hoc algorithm.
2. Check if using z3 as in Section 22.3 Package manager and Z3 leads to better results
3. Check if minisat leads to better results

Using SMT/SAT solvers leads to having to inform the user about conflicts, which might be hard to extract. In SAT that means reading the unsat core and translating it to a human-friendly way.

Porting PubGrub can work also, but since I have been a bundler user I am more inclined to it.

I think that porting molinillo seems promising. What do others think?

[ysbaddaden]

CaDiCaL didn't improve anything. Minisat probably won't too. I believe the problem isn't the SAT solver itself but the dependency solver logic on top that uses it.

Thanks for the links!

[didactic-drunk]

Also lets stick on topic here.

One workaround is reducing the graph size. I'm attempting to do so for older published releases.

Release a new hotfix version and take care initially to scope the dependency to the current major version. Ask the dependency to do another minor/hotfix release restoring compatibility if they are in violation of semver.

Another release is one more entry in the graph that's considered valid compounding the problems in this issue.

It may not be a semver violation. Foo v1 could work with Bar v1-4 and break later when Bar v5 is released.

[straight-shoota]

@didactic-drunk Please don't worry about purposely keeping the number of versions low. That's not going to work anyway when individual shards grow longer and longer histories. Currently, most shards have maybe a few releases max. Image the sizes after a few more years of development.

The thing is shards should just work, no matter the amount of releases your share uses and no matter if there are small versions restrictions. That seems feasible, but needs some (a lot?) more work to figure it out. If this would not be possible, shards would simply be unusable and we should move to a different, working dependency manager.

[rdp]

maybe rubygems has an example?

[RX14]

If this is not production ready, it should be reverted, or the release revoked. Arch linux naturally has updated to the latest release, 0.9.0. Having two conflicting ideas of "latest release" does not sound like a happy situation.

[ysbaddaden]

Lets stay focus on the bug.

[RX14]

Then where should this be discussed? Because it's a problem.

[waj]

During the last few days I've been playing around the idea of porting Molinillo to Crystal. The port was quite easy and the integration with Shards was a breeze (thanks @ysbaddaden for the well organized and clean code!). This is still very preliminar but this very same spec is resolved in less than two seconds and it looks really promising.

Due to my mathematical background I love the idea of solving the dependencies with a SAT solver. But the solver alone seems to be unfeasible for real world as the dependency problem is demonstrated to be NP hard. We need heuristics to reduce the search space and don't aim for optimal solution in the general case. I couldn't find any other project with a similar goal already solved so even I feel we could eventually get there, it's hard to estimate the complexity of this task.

With Crystal 1.0 coming closer and closer, it's really important to have a stable and reliable dependency manager. So, unless someone has a really good argument, I'll focus the next few days or weeks to complete the port of Molinillo, integrate with Shards and release a new version.

We could still keep the SAT solver around in case we eventually find a solution and demonstrate is more reasonable, powerful, elegant or convenient than using the Molinillo algorithm.

[ysbaddaden]

@waj That's great! Feel free to open any PR you want :)

[ysbaddaden]

Note: a SAT solver is nice, but it will need specializations to behave correctly, or a correct extraneous approach to build many SAT, instead of a single big one, because there are just too many variables & clauses. The one in 4a5cc30 is behaving nicely, and its only bug is including extraneous dependencies (it probably misses a few clauses). Thought the actual bug is trying to exhaust all possible solutions in Shards::Solver in search of the perfect one.

Basically, Molinillo seems to do just that: consider a subset of whatever is reachable in the graph, skipping entire sub-graphs, to quickly reach a solution. A SAT solver can't beat that level of specialization.

[RX14]

@waj I'm interested why you chose Molinillo vs pubgrub which was mentioned before, since the latter has had more mathematical analysis. Or did you not see the discussion on that earlier?

[waj]

@RX14 I did see the discussion and Pubgrub looks wonderful. It's really well documented although I didn't get through all of it. Molinillo was just more convenient because it's written in Ruby, it was really easy to port and it maches almost perfectly with the requirements in Shards. I'm very close to have it working with all the tests passing already.

So, with a relatively small effort I have something that it's working. That means if we want to replace it in the future with something else we would not regret having spent this time.

[waj]

Yesterday I pushed https://github.com/crystal-lang/crystal-molinillo and a molinillo branch with all the tests passing already. I didn't sent the PR yet because I'm working on the error reporting but it's already usable in case anyone want to start testing 🙂