PubGrub has good error messages, in fact that's one of its main selling points. When resolution fails you get a rich object with all the information to explain why that failure occurred. Specifically it is a derivation tree that proves that the requested resolution is impossible. Each node make some statement about a set of packages that cannot simultaneously be selected and points to two other nodes that when combined proof this note statement. The leaf nodes are statements provided to the solver by the dependency provider. The root node claims that "the requested package cannot be selected". If all of the base facts are true and all of the deductions are valid then this is a valid proof of unsatisfiedability of the requested resolution. But how can we verify that "if"?
Existing tests:
We have tests that model the entire resolution problem in a SAT solver. We use this to verify the high order bit. Namely that if pubgrub found a solution then the SAT solver except that solution, or if pubgrub did not find a solution then the SAT solver also do not find a solution. This tells us that we errored on the right occasions but nothing about the contents of our error object.
Upcoming tests:
129, extends this by looking at our error object to see which facts it depends on then only provides these facts to the SAT solver. Is careful to only remove facts where removing facts make more problems solvable. If the SAT solver cannot find a solution then we know that the error object correctly used a set of facts sufficient to prove the resolution problem impossible. But it tells us nothing about deductions are actually valid.
What else could we be testing:
"Each node make some statement about a set of packages that cannot simultaneously be selected" For every node this should be easy enough to check. In the SAT solver configured to represent the entire dependency resolution problem, for each node one at a time we can encode the term in the node and verify that it is unsat. This verifies that every term in our proof if in fact making a true statement of incompatibility.
"all of the base facts are true" this should also be easy to verify. Check with the dependency provider that the statement is true.
"all of the deductions are valid" this is the hardest to verify. I think we can do it. I think a valid deduction means that any selection that satisfies the node would also satisfy one of its direct children. For each node in a new SAT context encode the nodes statement and encode the statement for each of the nodes direct children, then ask the SAT solver if there's any way to satisfy the root without satisfying either of the children.
PubGrub has good error messages, in fact that's one of its main selling points. When resolution fails you get a rich object with all the information to explain why that failure occurred. Specifically it is a derivation tree that proves that the requested resolution is impossible. Each node make some statement about a set of packages that cannot simultaneously be selected and points to two other nodes that when combined proof this note statement. The leaf nodes are statements provided to the solver by the dependency provider. The root node claims that "the requested package cannot be selected". If all of the base facts are true and all of the deductions are valid then this is a valid proof of unsatisfiedability of the requested resolution. But how can we verify that "if"?
Existing tests:
Upcoming tests:
129, extends this by looking at our error object to see which facts it depends on then only provides these facts to the SAT solver. Is careful to only remove facts where removing facts make more problems solvable. If the SAT solver cannot find a solution then we know that the error object correctly used a set of facts sufficient to prove the resolution problem impossible. But it tells us nothing about deductions are actually valid.
What else could we be testing: