Add support for a CDCL-type SAT solver using the Resolvo crate #1179
Conversation
|
Something of a PSA for anyone trying this code out, we've discovered that #1130 introduced a bug that makes the original solver not respect host options. We're working on a fix. |
|
An update on the topic we discussed in the weekly meeting about getting different results from the solver between different runs. I realized that what is happening is currently builds of a version are not being sorted and so the build the solver will pick is subject to one or more per-process random seeds. If I ask for python and it depends on gcc, it will first try to use the highest version of python available, but it might by chance pick a build of python that depends specifically on gcc/6. This is all due to how the candidates of python are ordered. I will revisit the sort logic to make it behave more like the original solver. This should make the solve result deterministic between runs if the repo contents are the same. |
jrray
force-pushed
the
resolvo
branch
2 times, most recently
from
03ee415 to
daa4be4
Compare
jrray
force-pushed
the
resolvo
branch
3 times, most recently
from
9a3c596 to
c8a558a
Compare
There was a problem hiding this comment.
Pull Request Overview
This PR adds support for a CDCL‐type SAT solver via integration of the Resolvo crate. Key changes include replacing direct repository usage with a solver interface across several CLI commands, updating Cargo.toml to include the new spk‑solve workspace, and modifying the BinaryPackageBuilder API to accept a solver instance while removing legacy formatter resolver functions.
Reviewed Changes
Copilot reviewed 60 out of 60 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
| crates/spk-cli/cmd-make-binary/src/cmd_make_binary.rs | Replaced the old repositories field with a new solver field and updated decision formatter usages. |
| crates/spk-cli/cmd-install/src/cmd_install.rs, crates/spk-cli/cmd-explain/src/cmd_explain.rs, crates/spk-cli/cmd-env/src/cmd_env.rs | Updated to utilize the new solver.decision_formatter_settings instead of the removed formatter_settings. |
| crates/spk-build/src/build/binary.rs | Modified BinaryPackageBuilder to be generic over a solver, replacing old resolver callbacks with calls to run_and_print_resolve, and updating related type constraints. |
| Various test and macro files | Updated invocations to use from_recipe_with_solver and added a new macro parameter for specifying the solver to use. |
| Cargo.toml files | Added the spk-solve workspace dependency and updated version numbers for rstest and tokio. |
Comments suppressed due to low confidence (2)
crates/spk-cli/cmd-make-binary/src/cmd_make_binary.rs:29
- The field 'solver' replaces the old 'repos' field; please ensure that all references and functionality formerly provided by 'repos' (including repository management) are now fully supported by the new solver configuration.
pub solver: flags::Solver,
crates/spk-build/src/build/binary.rs:450
- [nitpick] Consider removing commented-out legacy resolver code to improve clarity and maintain maintainability now that the new run_and_print_resolve approach is being used.
//let (solution, graph) = self.source_resolver.solve(&self.solver).await?;
| @@ -232,6 +235,9 @@ pub struct Solver { | |||
| #[clap(flatten)] | |||
| pub repos: Repositories, | |||
|
|
|||
| #[clap(flatten)] | |||
| pub decision_formatter_settings: DecisionFormatterSettings, | |||
There was a problem hiding this comment.
This change makes it more difficult to create a solver programmaitically when using spk as a library in another tool. The problem is DecisionFormatterSettings has some fields that are not public (my fault, I didn't make those ones public and I don't think there was a reason) and this prevents a program making this object direclty. You have to make a list of string for the correct arguments and feed them through a clap parser to be able to get get_solver() to get a properly configured solver. That's fine for spk command line commands, but it is a bit clunky from a program that already has all the values not as strings.
An example is a tool we have that used to run spk bake... command and process the output. We changed it to use spk as a library and constuct a configured solver to run a solve and get data from calls without all the parsing (of input and output). But now it can't construct Solver clap objects directly and it has to create and parse fake command line arg strings to get a configured solver.
I think moving the DecisionFormatterSettings inside the Solver struct is fine. But it would be nice to either:
- Be able to construct the clap objects directly (by having all their fields public, or having them support
default(), or having some contructors for them), or - Have a way of constructing a solver, using the same logic that's in
get_solver(), without needing the clap objects (that probably means another layer of builder objects or similar structs to use as parameters to some create a solver function, thatget_solver()would also call).
| AllImpossibleChecks, | ||
| // This isn't a solver on its own. It indicates: the run all the | ||
| // solvers in parallel but show the output from the unchanged one. | ||
| // This runs all the solvers implemented in the original solver. At least | ||
| // for now, it is not possible to run both the original solver and the | ||
| // new solver in parallel. |
There was a problem hiding this comment.
Is this because of its current relative slowness, having to read all the specs in? Or is it something else, and what is that something else? Is it likely to change in future? I could see a situation where running them all in parallel for confirmation testing, or a part of a transition to just using the new solver, would be good. I guess making the 'because ...' part of the comment would help our future selves.
There was a problem hiding this comment.
This is documenting the state of the code but I didn't intend to imply it is impossible to implement.
|
From the meeting today:
|
I opted to work on this in a separate PR: #1217 |
Resolvo is a CDCL sat solver for package managers and will hopefully prove to be much better at solving quickly than our mostly brute-force approach. Making a checkpoint here after achieving a simple "solve" to get a feel for how spk type map onto Resolvo's concepts. Although currently the smallest unit the solver works with is a package, and that likely needs to change to a component. Signed-off-by: J Robert Ray <jrray@jrray.org>
By using an enum here, the global var handling can use its own enum variant instead of the flawed string prefix approach. Now it is simply not possible for a package name to be confused for a global var. Signed-off-by: J Robert Ray <jrray@jrray.org>
Messed up the logic when checking :all cases. Add test for this case. Signed-off-by: J Robert Ray <jrray@jrray.org>
These are effectively turned into more requests. Now the host options are being looked at. Signed-off-by: J Robert Ray <jrray@imageworks.com>
It is safe to update the known values without restarting the solve here, since these functions are only called before starting the solve. But that's not enforced by the code in any way at the moment. Signed-off-by: J Robert Ray <jrray@imageworks.com>
The requested by column is not populated. Signed-off-by: J Robert Ray <jrray@imageworks.com>
At SPI the newest python version available on centos is an embedded package, but it is undesirable for `spk env python` to choose an embedded python package. It also follows that it would have preferred to build from source a newer version of a package instead of use an existing build of an older version. Signed-off-by: J Robert Ray <jrray@imageworks.com>
Improve performance by not reading builds for packages that are for versions that are not applicable to the root requests. Signed-off-by: J Robert Ray <jrray@imageworks.com>
Log an info message for now, in order to gauge how many retries are happening in practice. Signed-off-by: J Robert Ray <jrray@imageworks.com> Signed-off-by: J Robert Ray <jrray@jrray.org>
The abstract solver now has a `run_and_print_resolve` that takes a formatter, which makes it possible to run either the old or new solver in a consistent way. The original `run_and_print_resolve` function has become `pub(crate)` to catch all the places that needed to be modified to use the new function. Signed-off-by: J Robert Ray <jrray@imageworks.com> Signed-off-by: J Robert Ray <jrray@jrray.org>
Making the original function `pub(crate)` to force code to change to use the trait instead. Remove the unused `run_and_log_decisions` function. Signed-off-by: J Robert Ray <jrray@imageworks.com> Signed-off-by: J Robert Ray <jrray@jrray.org>
The Solver trait was split into multiple traits with some blanket implementations for refs while chasing compile errors but this may not have actually been necessary. Add the "solver" flags to more commands so the user can choose what solver to use in more cases. Working towards being able to choose between the original solver and the new solver for all operations. More tests now run the test with both solves. Signed-off-by: J Robert Ray <jrray@imageworks.com> Signed-off-by: J Robert Ray <jrray@jrray.org>
Making it possible to choose what solver to use when running spk tests. Signed-off-by: J Robert Ray <jrray@imageworks.com>
However, this can still become a recursive call that blows out the stack if the bounds on Solver don't fit the bounds on the "real" `test` implementation. Signed-off-by: J Robert Ray <jrray@imageworks.com>
In order for `flags::Solver::get_solver` to offer a choice in what solver is returned, it needs to have access to the `solver_to_run` setting in `flags::DecisionFormatterSettings`. This change continues the theme of changing from a DecisionFormatter "containing" a solver to a solver "containing" a DecisionFormatter. Signed-off-by: J Robert Ray <jrray@jrray.org>
Signed-off-by: J Robert Ray <jrray@jrray.org>
`key_entry_names` is unused after it is cloned into `ordered_names`. Signed-off-by: J Robert Ray <jrray@jrray.org>
In order to reuse this logic for the resolvo solver, extract it to an external function. It is not practical for the resolvo solver to directly use a SortedBuildIterator. Signed-off-by: J Robert Ray <jrray@jrray.org>
Potential speedup by avoiding doing the reversal as a separate step. Signed-off-by: J Robert Ray <jrray@jrray.org>
Reuse the same build sorting logic as the original solver in order to get a deterministic result out of the solve. The solve can change drastically based on which build is selected first. Signed-off-by: J Robert Ray <jrray@jrray.org>
This is a public repo. Signed-off-by: J Robert Ray <jrray@imageworks.com>
Signed-off-by: J Robert Ray <jrray@imageworks.com>
When populating the Solution object, embedded packages need to be categorized properly or else when calculating the layers for the solution it ends up with an empty blob as one of the layers, which is an error. Handle source builds in resolvo solve When not building from source. Signed-off-by: J Robert Ray <jrray@imageworks.com>
The case where a stub only depended on the Run component of the parent still needs to declare a dependency to bring it in. Signed-off-by: J Robert Ray <jrray@imageworks.com>
To promote better test coverage, the build_package family of macros now require the name of the solver to use, and all the tests using these macros now run the test against all three solver choices (ignoring "all"). Workaround too many arguments lint and rstest la10736/rstest#226 (comment) Bumped to the latest version of rstest first to see if that would help. Signed-off-by: J Robert Ray <jrray@imageworks.com> Signed-off-by: J Robert Ray <jrray@jrray.org>
The solver tests were not passing if this feature is enabled, and this exposed a few problems in not handling ':all' requests correctly. When generating the "VersionSet" for dependencies, the PkgRequest needs to have the correct component populated. The logic for skipping or not skipping candidates when build from source needed to handle ':all' and it was restructured for clarity. When filtering candidates for a request of a component of a specific build, source builds needed to be filtered out. Signed-off-by: J Robert Ray <jrray@imageworks.com>
Fix commented out code in cmd_test for build stage tests and add a new test that checks the basic behavior of a build stage test that the test environment includes the build dependencies of the package being tested. Lift the old solver's configure_for_build_environment method to the Solver trait. Although the other test stages have code that only lives in the cmd_test crate to configure the solver properly, the build stage uses this method that was defined in the solver itself. While the logic of configure_for_build_environment could be duplicated in cmd_test, it is also reused by other code in the solver so it made sense to preserve the logic as a reusable solver method. Signed-off-by: J Robert Ray <jrray@jrray.org>
🚧 Work in Progress 🚧
It has been frequently requested over the life of this project to adopt a SAT solver in the hopes that it would provide faster solves and/or better messages when things can't solve. The Resolvo looked promising as it supports lazy solving and attempts to present solve errors in a relatively easy to understand format.
I have implemented Resolvo's DependencyProvider trait for spk packages and got enough of the spk package compatibility concepts right that the existing solver tests are all passing when run against the new solver.
I have also started to hard code changing all uses of the original solver into using the new solver just to expedite being able to test the new solver with some real world solves at SPI. There will be more work required to make it possible to choose between these solvers at runtime.
The new solver doesn't return a Graph because it doesn't use Node or State. It doesn't use Decision or Change. It doesn't use the existing validator types since those are designed to validate against a State. Solves aren't run via a SolverRuntime or through a DecisionFormatter. What is similar is the way a Solver is configured, and it still returns a Solution, although the Solution is not necessarily populated with the same details. It does well enough to pass all the tests (we need more tests!).
The high level view of how Resolvo works is that the DependencyProvider needs to be able to return a list of candidates for a request, filter those down based on compatibility, then enumerate all the dependencies of a given candidate. Rather than how our solver validates a package based on the state of the partial solve, Resolvo just needs to know if a given package (build) is compatible with a given request (python/3.11).
One of the first challenges was dealing with global var requests, meaning var requests that have no namespace. Resolvo requires that all requirements are attached to a specific package name. In order to handle global vars, each global var, for example, debug/true, is turned into a pseudo package called "debug". Then, since the DependencyProvider has to return the list of candidates (values) for "debug", all possible values that var can have has to be known in advance. To make that possible, the solve is restarted as new values are discovered. It is likely going to be necessary to maintain a cache that can be reused between solves to minimize the need to restart the solve.
Another challenge I haven't found a better approach for yet is that since all the candidates need to be returned upfront, when getting the candidates for a package, all the builds of all the versions of that package need to be visited, which includes reading in each build's package spec. This would benefit greatly from some kind of package index in the repo so this data could be read in bulk. I tried something where the list of candidates is first just the list of versions available for a package, but then it wasn't giving me the ability to filter those versions later after reading the builds.
What comes next is getting a test build up and running inside SPI and experimenting with some solves.