Open mratsim opened 3 years ago
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 https://github.com/nim-lang/nimble/blob/95e6870f60655e81ff488779c7f589fe649061ec/src/nimble.nim#L64 though requirements, almost immediately installing them https://github.com/nim-lang/nimble/blob/95e6870f60655e81ff488779c7f589fe649061ec/src/nimble.nim#L84-L86 which I believe to be the source of such bugs as https://github.com/nim-lang/nimble/issues/505 and https://github.com/nim-lang/nimble/issues/887 (could be prevented with explicit dependency graph construction).
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 z3
Related links:
requires
Both are looking into SAT solver
For good reasons: https://research.swtch.com/version-sat
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:
total package count: 1565
processing ok: 1382
not using github: 51
http error when getting: 87
configuration parse fail: 19
verLater ( > V ): 28
verEarlier ( < V ): 4
verEqLater ( >= V ): 1759
verEqEarlier ( <= V ): 2
verIntersect (> V & < V ): 37
verEq ( V ): 24
verAny ( * ): 319
verSpecial ( #head ): 34
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 requires
statements, and makes it hardly possible to do things like nimble build
and nimble test
without installing anything.
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 .nimble
file, but without evaluating it, and while this might seem like an overly fragile approach it worked successfully for approximately 96% of the [processed] packages. It is not possible to account for all possible ways of writing package specification of course, but things like
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)
Current solution of resolving-packages-while-installing-packages-wile-resolving packages leads to overly verbose output
Encountered this absolute masterpiece of readable user output (only lines with Dependency
are show, sorted to illustrate the point. Actual output is x2 longer due to Verifying dependencies for hmisc@0.11.5
)
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on benchy@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on cligen@any version already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on compiler@>= 1.4.0 already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on fusion@any version already satisfied
Info: Dependency on hcparse@any version already satisfied
Info: Dependency on hdrawing@>= 0.1.3 already satisfied
Info: Dependency on hdrawing@>= 0.1.3 already satisfied
Info: Dependency on hdrawing@>= 0.1.3 already satisfied
Info: Dependency on hdrawing@>= 0.1.3 already satisfied
Info: Dependency on hdrawing@>= 0.1.3 already satisfied
Info: Dependency on hdrawing@>= 0.1.3 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.1 already satisfied
Info: Dependency on hmisc@>= 0.10.4 already satisfied
Info: Dependency on hmisc@>= 0.10.7 already satisfied
Info: Dependency on hmisc@>= 0.11.3 already satisfied
Info: Dependency on hmisc@>= 0.11.3 already satisfied
Info: Dependency on hmisc@>= 0.4.0 already satisfied
Info: Dependency on hmisc@>= 0.9.15 already satisfied
Info: Dependency on hmisc@>= 0.9.15 already satisfied
Info: Dependency on hmisc@>= 0.9.15 already satisfied
Info: Dependency on hmisc@>= 0.9.15 already satisfied
Info: Dependency on hmisc@>= 0.9.15 already satisfied
Info: Dependency on hmisc@>= 0.9.15 already satisfied
Info: Dependency on hmisc@>= 0.9.15 already satisfied
Info: Dependency on hmisc@>= 0.9.16 already satisfied
Info: Dependency on hmisc@>= 0.9.1 already satisfied
Info: Dependency on hmisc@>= 0.9.1 already satisfied
Info: Dependency on hnimast@>= 0.3.18 already satisfied
Info: Dependency on hnimast@>= 0.3.18 already satisfied
Info: Dependency on hnimast@>= 0.3.18 already satisfied
Info: Dependency on hnimast@>= 0.3.18 already satisfied
Info: Dependency on hnimast@>= 0.3.18 already satisfied
Info: Dependency on hnimast@>= 0.3.18 already satisfied
Info: Dependency on hnimast@>= 0.3.19 already satisfied
Info: Dependency on hnimast@>= 0.3.20 already satisfied
Info: Dependency on hnimast@any version already satisfied
Info: Dependency on hnimast@#head already satisfied
Info: Dependency on hpprint@>= 0.2.11 already satisfied
Info: Dependency on hpprint@>= 0.2.11 already satisfied
Info: Dependency on hpprint@>= 0.2.12 already satisfied
Info: Dependency on hpprint@any version already satisfied
Info: Dependency on hpprint@any version already satisfied
Info: Dependency on hpprint@any version already satisfied
Info: Dependency on https://github.com/disruptek/balls@>= 2.0.0 & < 3.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/balls@>= 2.0.0 & < 3.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/criterion@< 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/criterion@< 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/gram@>= 0.3.2 already satisfied
Info: Dependency on https://github.com/disruptek/grok@>= 0.5.0 & < 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/grok@>= 0.5.0 & < 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/grok@< 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/grok@< 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/skiplists@>= 0.5.1 & < 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/ups@< 1.0.0 already satisfied
Info: Dependency on https://github.com/disruptek/ups@< 1.0.0 already satisfied
Info: Dependency on https://github.com/haxscramper/cxxstd.git@any version already satisfied
Info: Dependency on https://github.com/haxscramper/cxxstd.git@any version already satisfied
Info: Dependency on https://github.com/haxscramper/fusion.git@#matching-fixup already satisfied
Info: Dependency on https://github.com/haxscramper/fusion.git@#matching-fixup already satisfied
Info: Dependency on https://github.com/haxscramper/hasts@< 1.0.0 already satisfied
Info: Dependency on https://github.com/haxscramper/nimtrail.git@>= 0.1.1 already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on macroutils@any version already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimble@<= 0.13.0 already satisfied
Info: Dependency on nimspell@any version already satisfied
Info: Dependency on nimspell@any version already satisfied
Info: Dependency on nimtraits@any version already satisfied
Info: Dependency on npeg@>= 0.23.2 & < 1.0.0 already satisfied
Info: Dependency on npeg@>= 0.23.2 & < 1.0.0 already satisfied
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;
libsolv
from 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.