Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This closes #125
I started by adding a panic to the sat solver when it is had a
DependencyOnTheEmptySet
, all tests passed because proptest was not configured to generate them. I modified proptest and confirmed that this test now failed.meta_test_deep_trees_from_strategy
then informed me that I had too many ways for package to be invalid. Removingallow_deps
and reducing the probability of generatingDependencyOnTheEmptySet
made it happy. Then I could get to the meat of the experiment. I removed the code that generatesDependencyOnTheEmptySet
and all test pass. Well prop test passing once don't mean much, so I increased thecases
in theProptestConfig
. It has been running for a long time without finding a problem.Excitement over this progress is a little premature. This library is surprisingly robust against violations of its internal assumptions. In a number of places we filter out and assume that no term of an incompatibility is
Term::any()
, which turns out to be exactly what's generated whenDependencyOnTheEmptySet
. Adding a check for that property inmerge_incompatibility
makes everything unhappy. This is easy enough, when we generate the incompatibility for the dependency just leave off that term. Unfortunately, this causes another problem if the root package has one of these dependencies then it is automatically terminal, leading to the unhelpful error message "Root package depends on itself at a different version?". That check is always been suspect, it even has a comment about removing it. If we do remove it, everything passes. The next call is toadd_version
which does a more complicated check and decides not to add the package. So the loop continues tounit_propagation
which correctly generates a proof of unSAT.