CEP 3 - Using the Mamba solver in conda.

cep-3.md

@@ -0,0 +1,152 @@
+<table>
+<tr><td> Title </td><td> Using the Mamba solver in conda </td>
+<tr><td> Status </td><td> Draft </td></tr>
+<tr><td> Author(s) </td>
+    <td>
+        Jannis Leidel &lt;jleidel@anaconda.com&gt;,
+        Jaime Rodríguez-Guerra &lt;jrodriguez@quansight.com&gt;
+    </td>
+</tr>
+<tr><td> Created </td><td> Jul 20, 2021</td></tr>
+<tr><td> Updated </td><td> Jul 22, 2021</td></tr>
+<tr><td> Discussion </td><td> https://github.com/conda/ceps/pulls/2 </td></tr>
+<tr><td> Implementation </td><td> NA </td></tr>
+</table>
+
+## Abstract
+
+[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].
+
+## Motivation
+
+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.
+
+## Specification
+
+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.
+
+## Backwards Compatibility
+
+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.
+
+## Reference
+
+- [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
+
+
+[CEP 2]: https://github.com/conda/ceps/pull/1
+[libsolv]: https://github.com/openSUSE/libsolv
+[pycosat]: https://pypi.org/project/pycosat/
+[pycryptosat]: https://pypi.org/project/pycryptosat/
+[pysat]: https://github.com/pysathq/pysat
+[Mamba]: https://github.com/mamba-org/mamba
+[PicoSAT]: http://fmv.jku.at/picosat/
+[conda]: https://docs.conda.io/projects/conda/
+[conda-libmamba-solver]: https://github.com/conda-incubator/conda-libmamba-solver
+
+## Copyright
+
+All CEPs are explicitly [CC0 1.0 Universal](https://creativecommons.org/publicdomain/zero/1.0/).