| Title | Using the Mamba solver in conda |
| Status | Accepted |
| Author(s) | Jannis Leidel <[email protected]>, Jaime Rodríguez-Guerra <[email protected]> |
| Created | Jul 20, 2021 |
| Updated | Jul 22, 2021 |
| Discussion | https://github.com/conda/ceps/pulls/2 |
| Implementation | NA |
Conda's current default dependency solver based on pycosat has a number of downsides that led to community efforts writing a faster and more modern solver based on libsolv. The result was the basis for the alternative conda implementation called Mamba.
The intention of this CEP is to propose an experimental feature for conda to add support for the solver used in Mamba, eventually based on the plugin architecture proposed in CEP 2.
Conda's functionality and usability is predicated on the runtime characteristics of its low-level dependency resolver since it's a major part of its architecture -- next to the code infrastructure for the command line interface, the environment management and the handling of repo and channel data.
Speed, accuracy, debuggability and other impacts on the user
experience are heavily reliant on the underlying functionality of the
solver and conda's ability to interpret and communicate it to the user.
For example long running calls of the conda install command to resolve
complex environments and dependency trees directly impacts users'
real world experience of the package manager.
In addition, there is a wide-ranging proliferation of community efforts to improve the usability issues with conda outside the regular conda code project which makes it harder to retain a consistent technical and community roadmap. As such the experimental integration of the Mamba solver is to be considered but the first step to affect lasting change in the conda community and recognize the innovative solutions that have been worked on by community members.
Conda contains a solver registry in the conda.resolve module, currently
(4.10.x) listing three solvers:
- pycosat (default), a wrapper around the PicoSAT solver
- pycryptosat, a wrapper around the CryptoMiniSat solver
- pysat, a generic wrapper for a number of SAT solvers, Glucose4 is used
These solvers expose a pure SAT interface: they are conda-agnostic and
only understand SAT clauses, generated by the Clauses classes.
libsolv and mamba do not expose a pure SAT interface, so adding
support for this solver requires modifications higher in the abstraction
tree.
conda.core.solve sits high up in the conda logic, right below the
command-line interface for the install, update, remove and
create commands. There, a class named Solver is in charge of
collecting the index metadata, prefix state and other variables before
sending the list of required MatchSpec objects to the underlying
conda.resolve.Resolve instance.
The Resolve class is too tied to the Clauses class, and some of its
abstractions do not hold true for libsolv. As a result, we need to
operate at the Solver level. We have to subclass Solver and replace its
Solver.solve_final_state() method, which only requires us to return an
iterable of PackageRecord objects that is then diffed with the initial
environment state and turned into a transaction by the other methods in
the base class.
The resulting subclass would live in a separate project
conda-libmamba-solver and only depends on libmambapy (Mamba's
Python wrapper) and conda itself. To enable the experimental solver,
we add a new key to the Context class (experimental_solver) and a
command-line flag (--experimental-solver), which can take any of the
values added to a new Enum in conda.base.constants
(ExperimentalSolverChoice). The adequate solver class would be
returned by a helper function added to conda.core.solve
(_get_solver_class()) once the context has been initialized.
In a way, this means that the new solver class is pre-registered as a plugin, but must be installed separately. In the future, when the plugin system described in CEP 2 is fully implemented, this manual integration could be replaced by the necessary plugin hooks.
The default choice for the solver class must stay the same as long as the Mamba solver plugin is marked as experimental. Only after considerable functional and integration testing to verify the performance and solving improvements, it could be considered as a default candidate -- and only in a new major version of conda.
The metrics that define the success of this experiment are to be determined as part of the work on this CEP in coordination with the work on a separate CEP for the minimum viable solving behavior and the related test suite.
Given the differences in implementations and algorithms between the already supported solvers, it's to be expected that Mamba's solver will also produce slightly different solutions, depending to the requested set of dependencies.
To guarantee an acceptable degree of backwards compatibility with
conda's behavior, we need to make the experimental solver
comply with the existing conda integration test suite.
Any potential backward incompatibilities discovered as part of this work require formal documentation to be shared with the conda users and also inform the decision making around the status as an experimental solver.
In the future, the authors would like to see if it would be possible to compile an essential technical specification and prose documentation of the minimum viable solver logic, possibly accompanied by an automatic test suite of expected outcomes. Given the intricate nuances and implicit behavior of the existing logic, this task is deferred to a new CEP, yet to be drafted.
- conda: the conda package manager
- CEP 2: Add plugin architecture to conda
- Libsolv: the SAT solver that Mamba uses behind the scenes
- PicoSAT: the SAT solver wrapped by pycosat
- Mamba: the conda community reimplementation
- conda-libmamba-solver: The experimental libmamba solver integrations, packaged separately
All CEPs are explicitly CC0 1.0 Universal.