Dependency Solvers à la Carte

Package managers, such as NPM, are critical components of modern software development, allowing programmers to access large ecosystems full of useful packages. Given only a few lines of configuration, a package manager automates the downloading and installation of perhaps hundreds of (transitive) dependencies. To achieve this, package managers perform dependency solving to choose which concrete versions of dependencies to install. However, different solvers select dependency versions in very different ways, which affects correctness, code size, and other factors of the final bundled software in ways that are opaque and confusing to programmers. Moreover, the exact behaviors of dependency solvers are defined by their implementations, rather than by specifications, which inhibits systematic comparisons of dependency solvers, whether looking at formal properties or empirical evaluations. We present PacSolve, a unifying formal semantics of dependency solving. PacSolve is parameterized along several key axes, allowing it to compactly represent the key features and differences between NPM, PIP and Cargo, and to express a wide variety of alternative semantics for dependency solving. We then build an executable implementation of PacSolve using Rosette, and use it to implement a drop-in replacement for NPM called MinNPM. MinNPM allows the user to customize both the consistency criteria and optimization objectives. We show empirically that MinNPM shrinks the footprint of 21% of the top 1,000 most downloaded NPM packages with at least one dependency, and that it produces a newer set of dependencies for 14%. We also use MinNPM to answer key empirical questions about dependency solver design. Notably, we show that NPM's tree-solving semantics is only necessary for 1.9% of its packages, and that MinNPM gives higher quality solutions while taking only 2.6 seconds longer than NPM on average.