Modern techniques for dependency resolution #890
Labels
Comments
|
Datapoints regarding distributing Z3: it is packaged in most distributions, it appears to be stable, without concerning dependencies, and runs on most architectures. Then a valid solution is impossible, the dependency solver in apt/aptitude can suggest multiple alternative solutions that break/ignore one or more constraint each, starting with the less "aggressive" first. Z3 might help doing the same easily. Also, https://ci.debian.net/doc/ runs automated tests against multiple solutions and across multiple packages to spot incorrect dependency constraints. Z3 could help doing local compilation tests against combinations of dependencies to spot similar issues. |
|
Current implementation of dependency resolution does not construct explicit dependency graph, and instead just loops Line 64 in 95e6870 Lines 84 to 86 in 95e6870 Maybe we could adopt an approach similar to https://hal.archives-ouvertes.fr/hal-00149566/document for mapping dependency requirements to something that is fed into Related links:
|
For good reasons: https://research.swtch.com/version-sat |
This is a classic, if you haven't already then check out the "Alternatives?" section. Some of the suggestions may sound familiar.
Specifying a concrete version in a Nimble file has always been a bad idea and largely discouraged. I think that once lock files are merged into Nimble that we should look into disallowing concrete versions in "requires" completely (without lock files this is the only way you can hope to get reproducible builds). Nim should also grow the ability to compile a package with a dependency on two different versions of the same package. I think I may have finally convinced Araq that this is necessary :) |
|
Approximate current stats for nimble package requirement specifications: |
|
I think it should be explicitly noted that while the addition of SAT solver might be considered debatable, the dependency resolution step of nimble should be refactored into explicit dependency graph construction with subsequent full download of packages to be installed. Current solution of resolving-packages-while-installing-packages-wile-resolving packages leads to overly verbose output where each dependency can be repeated, makes resolution dependent on order of Package can appear multiple times in the output if it is required by more than one package, but each additional encounter will have useless 'requirement already satisfied' message, cluttering output and making it much harder to determine what went wrong. It is possible to get all necessary dependency information by parsing version = pkgVersion # fae
# paravim
installExt = @[
"nim", "txt", "ttf", "glsl", "c", "h",
when defined(windows):
"dll"
elif defined(macosx):
"dylib"
elif defined(linux):
"so"
]
# metar
include metar/version
version = metarVersion
# plz
version = CompileDate.replace("-", ".")Are extremely rare, and for these cases fully downloading packages before resolving it is the only solution (as well as non-github hostings (account for 3% of all packages). |
|
Related nim forum discussion https://forum.nim-lang.org/t/7671 additional edit (not separate comment to avoid pings)
Encountered this absolute masterpiece of readable user output (only lines with Not to mention this |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Just a recap of a short discussion with @haxscramper and @FedericoCeratto on modern dependency resolution.
Nimble found a certain combination of dependencies impossible to resolve even though there is actually a solution.
Modern package managers that handles tens of thousands of packages and/or multiversioning are gradually delegating dependency resolution to SAT solvers as this is a problem that can be modelled as a Satisfiability problem.
Writeups:
TLDR;
If we provide Z3, for DrNim nimble can piggyback on it.
libsolvfrom the OpenSuse project which is very package management oriented: https://github.com/openSUSE/libsolvNote: I think there are other approaches possible from writing that ourselves or using alternative theories like Integer Linear Programming (ILP) but it's more pragmatic to reuse existing blocks that were optimized and stabilized over years of usage here and regarding ILP, I tried to wrap the one for LLVM (http://isl.gforge.inria.fr/) or write one myself (https://github.com/mratsim/hydra) but those are really complex.
The text was updated successfully, but these errors were encountered: