6 ms·
I think calling it a SAT solver is appropriate here. A lot of package managers were "organically grown" i.e. they were created in response to a problem that aro
by sansnomme 7y ago
I think calling it a SAT solver is appropriate here. A lot of package managers were "organically grown" i.e. they were created in response to a problem that arose. Not much thought was given to the underlying problem and in the long term users suffer with e.g. dependencies taking forever to install and strange deadlocks. Recognizing it as a SAT problem from the start means we can easily throw Z3 or similar at it instead of manually adding heuristics everytime a user files a GitHub issue. (See Bundler and other pre-2018/2017 package management tools for example) Also, it's not always a SAT problem. For npm, Java Classloaders it's just tree traversal because conflicting sub dependencies of a dependency can co-exist.
That said, the Go's team (and to a lesser extent Python's too) dropped the ball here. None of the challenges of dependency management was unknown or unsolved. Anyone who has used e.g. Maven should be more than familiar. (A 11 section blog post is indeed nice though, good for onboarding new programmers I suppose) If developer experience was considered a first class priority, this could have been solved from day 0.
(My personal favorite is NPM since conflicting dependencies can co-exist at the expense of greater disk usage, but memory is cheap these days. No one with an electron app on their desktop has any right to complain about the memory usage of plain text source code.)
- mfer 7y ago> A lot of package managers were "organically grown" Many of the package managers we have now are thought out. Some replaced existing ones while others were crafted by people who had worked on dependency management in the past. Cargo and Composer are two examples of this.
- pcwalton 7y agoSee, that's the reason why calling it a SAT solver makes the problem sound scarier than it is. Using Z3--or even MiniSAT--is massive overkill. The naive exponential algorithm is fine, and it leads to more maintainable and understandable code. Rust's build performance has nothing to do with dependency solving. I've never heard of a package manager in which core dependency solving was a speed problem; dep was slow because of I/O, not SAT solving.
- Groxx 7y agoI/O + the absurd lengths you need to go to to (mostly) safely use Git as an external binary + no package repository to globally cache things like package names and versions. yea. "SAT solving" was an incredibly tiny amount of the runtime, like you'd expect for a CPU-bound algorithm. It's a straw man that keeps getting dragged out, but anyone who has used and understood this kind of dependency manager knows it's meaningless. You can definitely argue about its impact on community behavior, but it functions just fine, handles a ton of real-world issues reasonably, and it's nowhere near slow enough to care about.
- sansnomme 7y agoAsk the Python pipenv people. Take a look at their GitHub issues. https://github.com/pypa/pipenv/issues https://github.com/pypa/pipenv/issues Perhaps they need to "rewrite it in Rust" /s Their competitor's isn't much better either when it comes to dependency resolution related bugs. https://github.com/sdispater/poetry/issues https://github.com/sdispater/poetry/issues
- steveklabnik 7y agohttps://poetry.eustace.io/docs/faq/#why-is-the-dependency-resolution-process-slow https://poetry.eustace.io/docs/faq/#why-is-the-dependency-re... This is due to the fact that not all libraries on PyPI have properly declared their metadata and, as such, they are not available via the PyPI JSON API. At this point, Poetry has no choice but downloading the packages and inspect them to get the necessary information. This is an expensive operation, both in bandwidth and time, which is why it seems this is a long process. https://github.com/pypa/pipenv/issues/2284#issuecomment-395294319 https://github.com/pypa/pipenv/issues/2284#issuecomment-3952... (from 2018, may be outdated) we compute a resolution graph that attempts to satisfy all of the dependencies you specify, before we build your environment. That means we have to start downloading, comparing, and often times even building packages to determine what your environment should ultimately look like, all before we've even begun the actual process of installing it (there are a lot of blog posts on why this is the case in python so I won't go into it more here). ------------------ As I stated in another comment on this thread, Cargo has to do none of this. This stuff is the source of things being slow, not the actual "Okay I have all the versions and constraints, what's the answer" bit.
- mntmoss 7y agoI think the appropriate way to view this is not just as that this domain needs "SAT" (which enforces standardized algorithms as "the solution") so much as it describes an urgent need to popularize the concept of constraint satisfaction and optimization problems as a domain of coding that programmers actually deal with regularly and informally. Being able to sort, search and rank is the first step to having a backtracking solver, a technique that is very powerful and generalizable(albeit slow). But how many CS programs teach you to write solvers? Our education methods could do a lot more to draw this technique into its applications. For example, in game programming, satisfaction tends to come up rather abruptly when talking about physics solvers; not because it's only needed then, but because the jargon was appropriated from academic simulation papers, and it comes as part of a sudden bomb of math concepts, making it look more intimidating than it is. Non-realistic physics are just called "collision code", handwaved away and not given a great deal of formal attention, even though they are performing the work of solvers too, just usually with a mix of linear programming and local search. As such, a lot of new game programmers get stuck on collision problems and concurrency bugs that result from poorly constrained solutions, because they don't have the conceptual tools surfaced to reason about it with confidence. Likewise there are plenty of CRUD-style apps where a solver is a helpful building block for creating views and filters, but it's not approached as one, so you just get a buggy feature.