Version solving

Version solving consists in finding a set of packages and versions that satisfy all the constraints of a given project dependencies. In Rust, it is the package manager Cargo that takes the dependencies specified in the Cargo.toml file and deduces the complete list of exact versions of packages needed for your code to run. That includes direct dependencies but also indirect ones, which are dependencies of your dependencies. Packages and versions are not restricted to code libraries though. In fact they could refer to anything where "packages" act as a general name for things, and "versions" describe the evolution of those things. Such things could be office documents, laws, cooking recipes etc. Though if you version cooking recipes, well you are a very organized person.

Semantic versioning

The most common form of versioning scheme for dependencies is called semantic versioning. The base idea of semantic versioning is to provide versions as triplets of the form Major.Minor.Patch such as 2.4.1. The "semantic" term comes from the meaning of each part of the versioning system. Publishing a new patch version, for example from 2.4.1 to 2.4.2 means no interface has changed in the provided API of the library. That may be the case for documentation changes, or internal performance improvements for example. Increasing the minor number, for example from 2.4.1 to 2.5.0, means that things have been added to the API, but nothing was changed in the pre-existing API provided by the library. Finally, increasing the major number, such as from 2.4.1 to 3.0.0, means that some parts of the API have changed and thus may be incompatible with how we are currently using the previous version.

In Rust, packages are called crates and use semantic versioning. In fact, if you specify a dependency of the form package = "2.4.1", cargo will interpret that as the version constraint 2.4.1 <= v < 3.0.0 for that package. It does so based on the fact that any version in that range should not break our code according to the rules of semantic versioning. For more information on dependencies specifications in Cargo.toml you can read the Cargo reference book.

Side note on semantic versioning

Some people think that the granularity of semantic versioning is too broad in the case of major version changes. Instead, versions should never be breaking, but use new namespaces for things that change. It brings the same benefits in the large, that what choosing immutability as default brings in the small. For more information on this point of view, I highly recommend "Spec-ulation" by Rich Hickey, creator of the Clojure programming language.

Using the pubgrub crate

The PubGrub algorithm works for any package type implementing Clone + Eq + Hash + Debug + Display, and any version type implementing our Version trait, defined as follows.


#![allow(unused)]
fn main() {
pub trait Version: Clone + Ord + Debug + Display {
    fn lowest() -> Self;
    fn bump(&self) -> Self;
}
}

The lowest() trait method should return the lowest version existing, and bump(&self) should return the smallest version stricly higher than the current one.

For convenience, we already provide the SemanticVersion type, which implements Version for versions expressed as Major.Minor.Patch. We also provide the NumberVersion implementation of Version, which is basically just a newtype for non-negative integers, 0, 1, 2, etc.

Now that we know the Package and Version trait requirements, let's explain how to actually use pubgrub with a simple example.

Basic example with OfflineDependencyProvider

Let's imagine that we are building a user interface with a menu containing dropdowns with some icons, icons that we are also directly using in other parts of the interface. For this scenario our direct dependencies are menu and icons, but the complete set of dependencies looks like follows.

  • user_interface depends on menu and icons
  • menu depends on dropdown
  • dropdown depends on icons
  • icons has no dependency

We can model that scenario as follows.


#![allow(unused)]
fn main() {
use pubgrub::solver::{OfflineDependencyProvider, resolve};
use pubgrub::version::NumberVersion;
use pubgrub::range::Range;

// Initialize a dependency provider.
let mut dependency_provider = OfflineDependencyProvider::<&str, NumberVersion>::new();

// Add all known dependencies.
dependency_provider.add_dependencies(
    "user_interface", 1, vec![("menu", Range::any()), ("icons", Range::any())],
);
dependency_provider.add_dependencies("menu", 1, vec![("dropdown", Range::any())]);
dependency_provider.add_dependencies("dropdown", 1, vec![("icons", Range::any())]);
dependency_provider.add_dependencies("icons", 1, vec![]);

// Run the algorithm.
let solution = resolve(&dependency_provider, "user_interface", 1).unwrap();
}

As we can see in the previous code example, the key function of PubGrub version solver is resolve. It takes as arguments a dependency provider, as well as the package and version for which we want to solve dependencies, here package "user_interface" at version 1.

The dependency provider must be an instance of a type implementing the DependencyProvider trait defined in this crate. That trait defines methods that the resolver can call when looking for packages and versions to try in the solver loop. For convenience and for testing purposes, we already provide an implementation of a dependency provider called OfflineDependencyProvider. As the names suggest, it doesn't do anything fancy and you have to pre-register all known dependencies with calls to add_dependencies(package, version, vec_of_dependencies) before being able to use it in the resolve function.

Dependencies are specified with a Range, ranges being versions constraints defining sets of versions. In most cases, you would use Range::between(v1, v2) which means any version higher or equal to v1 and strictly lower than v2. In the previous example, we just used Range::any() which basically means any version.

Writing your own dependency provider

The OfflineDependencyProvider is very useful for testing and playing with the API, but would not be usable in more complex settings like Cargo for example. In such cases, a dependency provider may need to retrieve package information from caches, from the disk or from network requests.

TODO: waiting on potential API changes for DependencyProvider.

Solution and error reporting

When everything goes well, the algorithm finds and returns a set of packages and versions satisfying all the constraints of direct and indirect dependencies. Sometimes however, there is no solution because dependencies are incompatible. In such cases, the algorithm returns a PubGrubError::NoSolution(derivation_tree) where the provided derivation tree is a custom binary tree containing the chain of reasons why there is no solution.

All the items in the tree are called incompatibilities and may be of two types, either "external" or "derived". Leaves of the tree are external incompatibilities, and nodes are derived. External incompatibilities express facts that are independent of the way this algorithm is implemented such as

  • dependencies: package "a" at version 1 depends on package "b" at version 4
  • missing dependencies: dependencies of package "a" are unknown
  • absence of version: there is no version of package "a" higher than version 5

In contrast, derived incompatibilities are obtained during the algorithm execution by deduction, such as if "a" depends on "b" and "b" depends on "c", then "a" depends on "c".

Processing a derivation tree in a custom way to generate a failure report that is human-friendly is not an easy task. For convenience, this crate provides a DefaultStringReporter able to convert a derivation tree into a human-friendly String explanation of the failure. You may use it as follows.


#![allow(unused)]
fn main() {
use pubgrub::solver::resolve;
use pubgrub::report::{DefaultStringReporter, Reporter};
use pubgrub::error::PubGrubError;

match resolve(&dependency_provider, root_package, root_version) {
    Ok(solution) => println!("{:?}", solution),
    Err(PubGrubError::NoSolution(mut derivation_tree)) => {
        derivation_tree.collapse_noversion();
        eprintln!("{}", DefaultStringReporter::report(&derivation_tree));
    }
    Err(err) => panic!("{:?}", err),
};
}

Notice that we also used collapse_noversion() above. This method simplifies the derivation tree to get rid of the NoVersion external incompatibilities in the derivation tree. So instead of seeing things like this in the report:

Because there is no version of foo in 1.0.1 <= v < 2.0.0
and foo 1.0.0 depends on bar 2.0.0 <= v < 3.0.0,
foo 1.0.0 <= v < 2.0.0 depends on bar 2.0.0 <= v < 3.0.0.

you may have directly:

foo 1.0.0 <= v < 2.0.0 depends on bar 2.0.0 <= v < 3.0.0.

Writing your own error reporting logic

The DerivationTree is a custom binary tree where leaves are external incompatibilities, defined as follows,


#![allow(unused)]
fn main() {
pub enum External<P: Package, V: Version> {
    NotRoot(P, V),
    NoVersion(P, Range<V>),
    UnavailableDependencies(P, Range<V>),
    FromDependencyOf(P, Range<V>, P, Range<V>),
}
}

and nodes are derived incompatibilities, defined as follows.


#![allow(unused)]
fn main() {
pub struct Derived<P: Package, V: Version> {
    pub terms: Map<P, Term<V>>,
    pub shared_id: Option<usize>,
    pub cause1: Box<DerivationTree<P, V>>,
    pub cause2: Box<DerivationTree<P, V>>,
}
}

The terms hashmap contains the terms of the derived incompatibility. The rule is that terms of an incompatibility are terms that cannot be all true at the same time. So a dependency can for example be expressed with an incompatibility containing a positive term, and a negative term. For example, "root" at version 1 depends on "a" at version 4, can be expressed by the incompatibility {root: 1, a: not 4}. A missing version can be expressed by an incompatibility with a single term. So for example, if version 4 of package "a" is missing, it can be expressed with the incompatibility {a: 4} which forbids that version. If you want to write your own reporting logic, I'd highly suggest a good understanding of incompatibilities by reading first the section of this book on internals of the PubGrub algorithm.

The root of the derivation tree is usually a derived incompatibility containing a single term such as { "root": 1 } if we were trying to solve dependencies for package "root" at version 1. Imagine we had one simple dependency on "a" at version 4, but somehow that version does not exist. Then version solving would fail and return a derivation tree looking like follows.

Derived { root: 1 }
	├─ External dependency { root: 1, a: not 4 }
	└─ External no version { a: 4 }

The goal of error reporting is to transform that tree into a friendly human-readable output. It could be something like:

This project depends on version 4 of package a which does not exist
so version solving failed.

One of the subtleties of error reporting is that the binary derivation tree is actually a DAG (directed acyclic graph). Occasionally, an incompatibility may cause multiple derived incompatibilities in the same derivation tree such as below, where the incompatibility 2 is used to derive both incompatibilities 4 and 5.

                          +----------+        +----------+
                 +------->|incompat 4|------->|incompat 1|
                 |        +----------+        +----------+
                 |                |
          +----------+            |           +----------+
  (root)  |incompat 6|            +---------->|incompat 2|  (shared)
          +----------+            |           +----------+
                 |                |
                 |        +----------+        +----------+
                 +------->|incompat 5|------->|incompat 3|
                          +----------+        +----------+

For ease of processing, the DerivationTree duplicates such nodes in the tree, but their shared_id attribute will hold a Some(id) variant. In error reporting, you may want to check if you already gave an explanation for a shared derived incompatibility, and in such cases maybe use line references instead of re-explaning the same thing.

Internals of the PubGrub algorithm

For an alternative / complementary explanation of the PubGrub algorithm, you can read the detailed description of the solver provided by the original PubGrub author in the GitHub repository of the dart package manager pub.

PubGrub is an algorithm inspired by conflict-driven nogood learning (CDNL-ASP), an approach presented by Gabser, Kaufmann and Schaub in 2012. The approach consists in iteratively taking decisions (here picking a package and version) until reaching a conflict. At that point it records a nogood (an "incompatibility" in PubGrub terminology) describing the root cause of the conflict and backtracks to a state previous to the decision leading to that conflict. CDNL has many similarities with CDCL (conflict-driven clause learning) with the difference that nogoods are conjunctions while clauses are disjunctions of literals. More documentation of their approach is available on their website.

At any moment, the PubGrub algorithm holds a state composed of two things, (1) a partial solution and (2) a set of incompatibilities. The partial solution (1) is a chronological list of "assignments", which are either decisions taken or version constraints for packages where no decision was made yet. The set of incompatibilities (2) is an ever-growing collection of incompatibilities. We will describe them in more details later but simply put, an incompatibility describes packages that are dependent or incompatible, that is packages that must be present at the same time or that cannot be present at the same time in the solution.

Incompatibilities express facts, and as such are always valid. Therefore, the set of incompatibilities is never backtracked, only growing and recording new knowledge along the way. In contrast, the partial solution contains decisions and deductions (called "derivations" in PubGrub terminology), that are dependent on every decision made. Therefore, PubGrub needs to be able to backtrack the partial solution to an older state when there is a conflict.

Overview of the algorithm

Solver main loop

The solver runs in a loop with the following steps:

  1. Perform unit propagation on the currently selected package.
  2. Make a decision: pick a new package and version compatible with the current state of the partial solution.
  3. Retrieve dependencies for the newly selected package and transform those into incompatibilities.

At any point within the loop, the algorithm may fail due to an impossibility to solve a conflict or an error occuring while trying to retrieve dependencies. When there is no more decision to be made, the algorithm returns the decisions from the partial solution.

Unit propagation overview

Unit propagation is the core mechanism of the algorithm. For the currently selected package, unit propagation aims at deriving new constraints (called "terms" in PubGrub and "literals" in CDNL terminology), from all incompatibilities referring to that package. For example, if an incompatibility specifies that packages a and b are incompatible, and if we just made a decision for package a, then we can derive a term specifying that package b should not appear in the solution.

While browsing incompatibilities, we may stumble upon one that is already "satisfied" by the current state of the partial solution. In our previous example, that would be the case if we had previously already made a decision for package b (in practice that exact situation could not happen but let's leave that subtlety for later). If an incompatibility is satisfied, we call that a conflict and must perform conflict resolution, and backtrack the partial solution to a state previous to the root cause of the conflict.

Conflict resolution overview

Conflict resolution aims at finding the root cause of a conflict, recording it in an incompatibility, and backtracking the partial solution to a state previous to the decision at the root of the conflict. This is performed by a loop composed of two steps:

  1. Find the earliest assignment in the partial solution such that the conflictual incompatibility is satisfied by the partial solution until there. That assignment is called the "satisfier".
  2. If the satisfier is the root cause of the conflict, end the loop and backtrack the partial solution. Otherwise, compute the "prior cause" of the satisfier, which is a new incompatibility and continue the loop with that one as the conflictual incompatibility.

Terms

Definition

A term is an atomic variable, called "literal" in mathematical logic, that is evaluated either true or false depending on the evaluation context. In PubGrub, a term is either a positive or a negative range of versions defined as follows.


#![allow(unused)]
fn main() {
pub enum Term<V> {
    Positive(Range<V>),
    Negative(Range<V>),
}
}

A positive term is evaluated true if and only if a version contained in its range was selected. A negative term is evaluated true if and only if a version not contained in its range was selected, or no version was selected. The negate() method transforms a positive term into a negative one and vice versa. In this guide, for any given range \(r\), we will note \([r]\) its associated positive term, and \(\neg [r]\) its associated negative term. And for any term \(T\), we will note \(\overline{T}\) the negation of that term. Therefore we have the following rules,

\[\begin{eqnarray} \overline{[r]} &=& \neg [r], \nonumber \\ \overline{\neg [r]} &=& [r]. \nonumber \\ \end{eqnarray}\]

Special terms

Provided that we have defined an empty range of versions \(\varnothing\), there are two terms with special behavior which are \([\varnothing]\) and \(\neg [\varnothing]\). By definition, \([\varnothing]\) is evaluated true if and only if a version contained in the empty range is selected. This is impossible and as such the term \([\varnothing]\) is always evaluated false. And by negation, the term \(\neg [\varnothing]\) is always evaluated true.

Intersection of terms

We define the "intersection" of two terms as the conjunction of those two terms (a logical AND). Therefore, if any of the terms is positive, the intersection also is a positive term. Given any two ranges of versions \(r_1\) and \(r_2\), the intersection of terms based on those ranges is defined as follows,

\[\begin{eqnarray} [r_1] \land [r_2] &=& [r_1 \cap r_2], \nonumber \\ [r_1] \land \neg [r_2] &=& [r_1 \cap \overline{r_2}], \nonumber \\ \neg [r_1] \land \neg [r_2] &=& \neg [r_1 \cup r_2]. \nonumber \\ \end{eqnarray}\]

And for any two terms \(T_1\) and \(T_2\), their union and intersection are related by

\[ \overline{T_1 \lor T_2} = \overline{T_1} \land \overline{T_1}. \]

Relation between terms

We say that a term \(T_1\) is satisfied by another term \(T_2\) if \(T_2\) implies \(T_1\), i.e. when \(T_2\) is evaluated true then \(T_1\) must also be true. This is equivalent to saying that \(T_2\) is a subset of \(T_1\), which is verified if \( T_2 \land T_1 = T_2 \).

Note on comparability of terms:

Checking if a term is satisfied by another term is accomplished in the code by verifying if the intersection of the two terms equals the second term. It is thus very important that terms have unique representations, and by consequence also that ranges have a unique representation.

In the provided Range type, ranges are implemented as an ordered vec of non-intersecting semi-open intervals. It is thus important that they are always reduced to their canonical form. For example, the range 2 <= v < 2 is actually empty and thus should not be represented by vec![(2, Some(2))] but by the empty vec![]. This requires special care when implementing range intersection.

Incompatibilities

Definition

Incompatibilities are called "nogoods" in CDNL-ASP terminology. An incompatibility is a conjunction of package terms that must be evaluated false, meaning at least one package term must be evaluated false. Otherwise we say that the incompatibility has been "satisfied". Satisfied incompatibilities represent conflicts and thus the goal of the PubGrub algorithm is to build a solution such that none of the produced incompatibilities are ever satisfied. If one incompatibility becomes satisfied at some point, the algorithm finds the root cause of it and backtracks the partial solution before the decision at the origin of that root cause.

Remark: incompatibilities (nogoods) are the opposite of clauses in traditional conflict-driven clause learning (CDCL) which are disjunctions of literals that must be evaluated true, so have at least one literal evaluated true.

The gist of CDCL is that it builds a solution to satisfy a conjunctive normal form (conjunction of clauses) while CDNL builds a solution to unsatisfy a disjunctive normal form (disjunction of nogoods).

In addition, PubGrub is a lazy CDNL algorithm since the disjunction of nogoods (incompatibilities) is built on the fly with the solution.

In this guide, we will note incompatibilities with curly braces. An incompatibility containing one term \(T_a\) for package \(a\) and one term \(T_b\) for package \(b\) will be noted

\[ \{ a: T_a, b: T_b \}. \]

Remark: in a more "mathematical" setting, we would probably have noted \( T_a \land T_b \), but the chosen notation maps well with the representation of incompatibilities as hash maps.

Properties

Packages only appear once in an incompatibility. Since an incompatibility is a conjunction, multiple terms for the same package are merged with the intersection of those terms.

Terms that are always satisfied can be removed from an incompatibility. We previously explained that the term \( \neg [\varnothing] \) is always evaluated true. As a consequence, it can safely be removed from the conjunction of terms that is the incompatibility.

\[ \{ a: T_a, b: T_b, c: \neg [\varnothing] \} = \{ a: T_a, b: T_b \} \]

Dependencies can be expressed as incompatibilities. Saying that versions in range \( r_a \) of package \( a \) depend on versions in range \( r_b \) of package \( b \) can be expressed by the incompatibility

\[ \{ a: [r_a], b: \neg [r_b] \}. \]

Unit propagation

If all terms but one of an incompatibility are satisfied by a partial solution, we can deduce that the remaining unsatisfied term must be evaluated false. We can thus derive a new unit term for the partial solution which is the negation of the remaining unsatisfied term of the incompatibility. For example, if we have the incompatibility \( \{ a: T_a, b: T_b, c: T_c \} \) and if \( T_a \) and \( T_b \) are satisfied by terms in the partial solution then we can derive that the term \( \overline{T_c} \) can be added for package \( c \) in the partial solution.

Rule of resolution

Intuitively, we are able to deduce things such as if package \( a \) depends and package \( b \) which depends on package \( c \), then \( a \) depends on \( c \). With incompatibilities, we would note

\[ \{ a: T_a, b: \overline{T_b} \}, \quad \{ b: T_b, c: \overline{T_c} \} \quad \Rightarrow \quad \{ a: T_a, c: \overline{T_c} \}. \]

This is the simplified version of the rule of resolution. For the generalization, let's reuse the "more mathematical" notation of conjunctions for incompatibilities \( T_a \land T_b \) and the above rule would be

\[ T_a \land \overline{T_b}, \quad T_b \land \overline{T_c} \quad \Rightarrow \quad T_a \land \overline{T_c}. \]

In fact, the above rule can also be expressed as follows

\[ T_a \land \overline{T_b}, \quad T_b \land \overline{T_c} \quad \Rightarrow \quad T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c} \]

since for any term \( T \), the disjunction \( T \lor \overline{T} \) is always true. In general, for any two incompatibilities \( T_a^1 \land T_b^1 \land \cdots \land T_z^1 \) and \( T_a^2 \land T_b^2 \land \cdots \land T_z^2 \) we can deduce a third, called the resolvent whose expression is

\[ (T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2). \]

In that expression, only one pair of package terms is regrouped as a union (a disjunction), the others are all intersected (conjunction). If a term for a package does not exist in one incompatibility, it can safely be replaced by the term \( \neg [\varnothing] \) in the expression above as we have already explained before.

Partial solution

The partial solution is the part of PubGrub state holding all the decisions taken and the derivations computed from unit propagation on almost satisfied incompatibilities. We regroup decisions and derivations under the term "assignment".

The partial solution must be backtrackable when conflicts are detected. For this reason all assignments are recorded with their associated decision level. The decision level of an assignment is a counter for the number of decisions that have already been taken (including that one if it is a decision). If we represent all assignments as a chronological vec, they would look like follows:

[ (0, root_derivation),
  (1, root_decision),
  (1, derivation_1a),
  (1, derivation_1b),
  ...,
  (2, decision_2),
  (2, derivation_2a),
  ...,
]

The partial solution must also enable efficient evaluation of incompatibilities in the unit propagation loop. For this, we need to have efficient access to all assignments referring to the packages present in an incompatibility.

To enable both efficient backtracking and efficient access to specific package assignments, the current implementation holds a dual representation of the the partial solution. One is called history and keeps dated (with decision levels) assignments in an ordered growing vec. The other is called memory and organizes assignments in a hashmap where they are regrouped by packages which are the hashmap keys. It would be interresting to see how the partial solution is stored in other implementations of PubGrub such as the one in dart pub.

Conflict resolution

As stated before, a conflict is a satisfied incompatibility. We may detect such conflict while generating new derivations in the unit propagation loop. Given a satisfied incompatibility, conflict resolution aims at finding the root cause of the conflict and backtracking the partial solution just before the decision at its origin.

TODO: explain how finding the earliest satisfier fits into this.

TODO: explain that prior cause is just the previously explained rule of resolution on two incompatibilities, the current one, and the one being the cause of the earliest satisfier.

Building a report tree

Terminal incompatibility

Whenever we build an incompatibility that will always be satisfied, version solving has failed. The empty incompatibility, for example is an incompatibility for which terms of all packages are \( \neg [\varnothing] \) and thus all terms are satisfied. Another terminal incompatibility is an incompatibility containing a single package term, satisfied by picking the package and version at the root of the solution, the one for which we want to resolve dependencies.

Derivation tree to report tree

Incompatibilities are either external or derived. External incompatibilities are the one expressing facts independent of the solver deductions capabilities, such as dependencies, unavailable dependencies, missing versions etc. In contrast, derived incompatibilities are the one obtained through the rule of resolution when computing prior causes. Every derived incompatibility keeps a reference to the two incompatibilities that were used to derive it. As a consequence, a chain of derived incompatibilities defines a binary tree, that we call the derivation tree.

When version solving failed, it is thus possible to take the derivation tree of the terminal incompatibility to build a complete explanation of why it failed. That derivation tree however is using incompatibilities whose shape are dependent on internal implementation details. The purpose of the report tree is then to transform the derivation tree into a data structure easily usable for reporting.

Report tree type

In order to provide information in the most detailed way, the report tree uses enum types that try to be as self-explanatory as possible. I'm not sure the current design, based on a recursive (boxed) enum is the best one but it has the advantage of presenting the binary report tree in a very straightforward manner, easy to process.

Duplicate nodes

Though it has the shape of a binary tree, and can be represented as a binary tree, the derivation tree is actually a derivation graph. Indeed, even if every derived incompatibility was built from two others, some incompatibilities may have been used to derive multiple new incompatibilities.

TODO: ascii representations similar to the ones in the error reporting section of pub solver.md.

There is still much API exploration work to be done on error reporting.

Testing and benchmarking

How can I contribute? Here are some ideas

  • Use it! Indeed there is quite some work left for custom dependency providers. So just using the crate, building you own dependency provider for your favorite programming language and letting us know how it turned out would be amazing feedback already!

  • Non failing extension for multiple versions. Currently, the solver works by allowing only one version per package. In some contexts however, we may want to not fail if multiple versions are required, and return instead multiple versions per package. Such situations may be for example allowing multiple major versions of the same crate. But it could be more general than that exact scenario.