search

mpizenberg / elm-pubgrub

PubGrub version solving algorithm in elm
https://mpizenberg.github.io/elm-pubgrub/
BSD 3-Clause "New" or "Revised" License
6 stars 2 forks source link

Example 5bis fails #1

Closed malaire closed 4 years ago

malaire commented 4 years ago

Creating an issue for this for notes and discussion.

Example 5bis fails in PubGrub.unitPropagationLoop by PartialSolution.relation priorCause updatedModel.partialSolution returning Satisfies instead of expected AlmostSatisfies.

Here partialSolution is

foo   NOT  1
bar   NOT  [ 2, 3 [
baz   IS   [ 1, 2 [
foo   IS   [ 1, 2 [
root  IS   1

and priorCause is

{ root: IS 1, baz: NOT none }

Manual checking confirms that partialSolution indeed satisfies priorCause, so one of these is wrong.

mpizenberg commented 4 years ago

Thanks for the creation of the issue. I suppose you figured out that the binary tree displayed in the debug output for priorCause is the chain of derivation leading to the actual incompatibility creating the issue.

malaire commented 4 years ago

Yes it's the "Derivation Graph" mentioned at PubGrub documentation[1]. I'm still reading this while comparing it to the implementation.

While current debug output is quite complete, it would be more useful if it used exact same terms as the PubGrub documentation. For example terms changed, package, incompatibility etc. in "Unit Propagation" section.

[1] https://github.com/dart-lang/pub/blob/master/doc/solver.md

malaire commented 4 years ago

PubGrub documentation says that

The process of returning the partial solution to a state where the incompatibility is no longer satisfied is known as conflict resolution.

So error here is in conflictResolution which doesn't return correct value. I see it has some notes about things which are guaranteed, but those are not checked, so adding more error reporting there would be first step to do.

malaire commented 4 years ago

Adding this debug check makes Example 5bis fail earlier, and also makes Examples 3 and 4 fail: https://github.com/malaire/elm-pubgrub/commit/02dc6fc403974fef10f36b9eccc67ba9ab7f6955

p.s. I havn't yet learned how to make pull requests in GitHub.

harrysarson commented 4 years ago

image

:)

malaire commented 4 years ago

Why can't official guide tell simple solution for making PR, but instead has longwinded 8-step process which requires base branches, head forks and compare branches?

Anyway, here's the PR (https://github.com/mpizenberg/elm-pubgrub/pull/2), and I think I'll continue debugging with Example 3 which now fails also and is simpler than 5bis.

mpizenberg commented 4 years ago

So I've done a full re-read of the PubGrub algorithm. The last step of the conflict resolution is to return the current incompatibility of the loop and to backtrack the partial solution. That incompatibility has been obtained through successive "priorCause" computations and should be referred to as the "root cause" to stick to PubGrub namings. If we believe PubGrub unit propagation explanation, the returned root cause should be guaranted to almost satisfy the backtracked partial solution. I'll probably want to verify why that is, but let's assume that is indeed the case (they should know ^^). In that case, these are the things that could go wrong.

I'll want to check those things manually and maybe add unit tests. There are also few remarks:

malaire commented 4 years ago

About {q, r, t1 U t2}: Documentation says

In fact, we can generalize this: given any incompatibilities {t1, q} and {t2, r}, we can derive {q, r, t1 ∪ t2}, since either t1 or t2 is true in every solution in which t1 ∪ t2 is true. This reduces to {q, r} in any case where not t2 ⊆ t1 (that is, where not t2 satisfies t1), including the case above where t1 = t and t2 = not t.

The way I understand this is that {q, r, t1 ∪ t2} is just part of the explanation - it's never actually used in the algorithm. Instead in algorithm {q, r} is used, but only when not t2 satisfies t1.

mpizenberg commented 4 years ago

Yes it is actually used, that's the else block here: https://github.com/mpizenberg/elm-pubgrub/blob/master/src/PubGrub.elm#L331 It's just that the naming of the algorithm calls it "priorCause" even before it is actually a correct prior cause, which I called newIncompat later because I was just out of names and didn't fully understand it yet: https://github.com/mpizenberg/elm-pubgrub/blob/master/src/PubGrub.elm#L346

malaire commented 4 years ago

Ah, true. priorCause is initially set to {q, r}, but the third term can be added a bit later.

Although the added term isn't t1 ∪ t2 but corresponding not (not t2 \ t1).

Note: not (satisfier \ term) corresponds to t1 ∪ t2 above with term = t1 and satisfier = not t2, by the identity (Sᶜ \ T)ᶜ = S ∪ T.

p.s. I'll need to brush up set theory.

malaire commented 4 years ago

But elm-pubgrub is adding the union instead of not (satisfier \ term) as algorithm says?

https://github.com/mpizenberg/elm-pubgrub/blob/3a36cd3ed2dd4c0278fff6316b57b9411c35b1cf/src/PubGrub.elm#L344

mpizenberg commented 4 years ago

The logic is explained just above I believe this is correct

https://github.com/mpizenberg/elm-pubgrub/blob/3a36cd3ed2dd4c0278fff6316b57b9411c35b1cf/src/PubGrub.elm#L339-L341

mpizenberg commented 4 years ago

To expand a bit the explanation. I do not have the \ Set operator but I have the union and intersection operations on ranges Sets, so with A for satisfier and B for term we have:

A \ B == intersection A (not B)
and
union (not A) (B) == not (intersection A (not B))
so
not (A \ B) == union (not A) B
malaire commented 4 years ago

Yes, even the algorithm description says that they correspond to each other. But algorithm description clearly says that the added term is not (satisfier \ term) and not the union. So elm-pubgrub is wrong here.

From https://github.com/dart-lang/pub/blob/master/doc/solver.md#conflict-resolution:

  • If satisfier doesn't satisfy term, add not (satisfier \ term) to priorCause.
    • Note: not (satisfier \ term) corresponds to t1 ∪ t2 above with term = t1 and satisfier = not t2, by the identity (Sᶜ \ T)ᶜ = S ∪ T.
malaire commented 4 years ago

This is the second place I've seen where elm-pubgrub deliberately implements the algorithm incorrectly.

I see no reason to debug elm-pubgrub further as it doesn't even attempt to implement Pubgrub correctly.

mpizenberg commented 4 years ago

I'm sorry if this frustrates you but I'm trying to do the correct implementation (with the time I can put in it) and to strictly follow the PubGrub algorithm, the explanation above that I'm re-adding below seems correct to me so I am actually adding not (satisfier \ term). I cannot just invent out of fin air the \ operator, and if I'd have to add it, I'd just define it as below. If you've seen another place delibarately different than PubGrub, please do tell.

A \ B == intersection A (not B)
and
union (not A) (B) == not (intersection A (not B))
so
not (A \ B) == union (not A) B
malaire commented 4 years ago

If you've seen another place delibarately different than PubGrub, please do tell.

The other place is about expanding/merging version ranges: https://github.com/mpizenberg/elm-pubgrub/issues/3#issuecomment-639600678

... the explanation above that I'm re-adding below seems correct to me so I am actually adding not (satisfier \ term) ...

For one thing you are adding potentially POSITIVE term while algorithm clearly says to add NEGATIVE term.

Also doing things differently than what is said in algorithm makes debugging a lot harder as it's not possible to compare the behavior of your implementation to the exact steps mentioned in documentation.

mpizenberg commented 4 years ago

For one thing you are adding potentially POSITIVE term while algorithm clearly says to add NEGATIVE term.

This isn't sayed anywhere, or it may be your interpretation that differs from mine. I don't see a reason for satisfier or term to be positive terms. Maybe that's my interpretation that's wrong and that's why having a second view is great. satisfier and term could very well be negative terms, and in that case not (satisfier \ term) is positive.

As for the equivalent code in the actual dart pub code base, it turns out the Set complement operator is called difference there and is implemented as follows (exactly how I did).

https://github.com/dart-lang/pub/blob/master/lib/src/solver/term.dart#L149

Also doing things differently than what is said in algorithm makes debugging a lot harder as it's not possible to compare the behavior of your implementation to the exact steps mentioned in documentation.

Sorry about that, I thought the comment just above in the code would suffice to follow easily. Obviously things need to be different between an imperative description and a functional implementation. I didn't thought that line would be much trouble compared to the structural changes to the algorithm required by the Elm language.

The other place is about expanding/merging version ranges: #3 (comment)

I can understand if you consider this deliberately different. Actually the description of the PubGrub algorithm leaves a lot of grey areas where I just have to make some choices, like version choosing heuristics and other things. It also indicates some things as being uneeded for correctness but good for performances. I interpreted this explanation as such one of those performance-only improvements, especially given that no such collapse is part of the algorithm steps below the textual explanation.

Pubgrub collapses identical dependencies from adjacent package versions into individual incompatibilities. This substantially reduces the total number of incompatibilities and makes it much easier for Pubgrub to reason about multiple versions of packages at once. For example, rather than representing foo 1.0.0 depends on bar ^1.0.0 and foo 1.1.0 depends on bar ^1.0.0 as two separate incompatibilities, they're collapsed together into the single incompatibility {foo ^1.0.0, not bar ^1.0.0}.

Since I have a limited time implementing all this, I've reduced things to what needs to be done, and added some TODOS in the code base for those as in that example you point out:

https://github.com/mpizenberg/elm-pubgrub/blob/master/src/Incompatibility.elm#L190

But again, if this is a misinterpretation on my part, you're right and that's why I've added your point to the things to check in this issue (see "absence of smart merging" there: https://github.com/mpizenberg/elm-pubgrub/issues/1#issuecomment-640913440)

Anyway, I just thought that your comment was a bit harsh and wanted to let you know that it hurt me. If you do not feel like helping anymore I totally understand.

malaire commented 4 years ago

When I mentioned following the steps, I meant the steps in Examples section.

malaire commented 4 years ago

But again, if this is a misinterpretation on my part, you're right and that's why I've added your point to the things to check in this issue (see "absence of smart merging" there: #1 (comment))

Can you confirm whether relation-checking at any point has access to the list of all available versions? Because if not, then current implementation of elm-pubgrub can't work correctly, as I said in the other thread (https://github.com/mpizenberg/elm-pubgrub/issues/3#issuecomment-639641827), and so this clear bug should be at top of the list of things to check and not the last item to check.

malaire commented 4 years ago

As for the equivalent code in the actual dart pub code base, it turns out the Set complement operator is called difference there and is implemented as follows (exactly how I did).

I was wrong here then. I thought it was important when algorithm description clearly made the point that different term needs to be used instead of union.

mpizenberg commented 4 years ago

Can you confirm whether relation-checking at any point has access to the list of all available versions? Because if not, then current implementation of elm-pubgrub can't work correctly, as I said in the other thread (#3 (comment)).

It doesn't. And it appears that pub also doesn't have access at that time:

https://github.com/dart-lang/pub/blob/master/lib/src/solver/version_solver.dart#L156

Then I suppose this means that incompatibilities should be more descriptive and collapsing is needed? Merging a new incompatibility (Incompatibility.merge and in PubGrub.backtrack that should use Incompatibility.merge) is a place where this could be done I suppose. I didn't take the time yet to check that since I wanted to first get a better overview of the algorithm.

I'll take some time next weekend on specifically this issue https://github.com/mpizenberg/elm-pubgrub/issues/3#issuecomment-639641827 that you pointed out.

malaire commented 4 years ago

I'll expand on my understanding of bar any vs. bar 1.0.0 issue if you didn't understand what I think is wrong here.

Basic question in conflict resolution is whether certain term satisfies another term.

IN ALGORITHM

In Example 3 the question is whether bar ^1.0.0 satisfies bar any.

In other words the question is: If bar is 1.0.0 <= x < 2.0.0 is true, does that mean bar is any version is always true? Clearly answer is YES, because if bar is a version within range 1.0.0 <= x < 2.0.0 then bar does have a version.

In terms of sets we can say that bar ^1.0.0 is SUBSET of bar any.

IN ELM-PUBGRUB

elm-pubgrub uses bar 1.0.0 instead of bar any. Let's see how this works out:

The question now is whether bar ^1.0.0 satisfies bar 1.0.0.

In other words the question is: If bar is 1.0.0 <= x < 2.0.0 is true, does that mean bar is version 1.0.0 is always true? Clearly answer is NO, because if bar is a version within range 1.0.0 <= x < 2.0.0 then bar could be for example 1.5.0 which is not 1.0.0.

In terms of sets we can say that bar ^1.0.0 is SUPERSET of bar 1.0.0.

THE BUG

So by deciding to use bar 1.0.0 instead of bar any, elm-pubgrub arrives at completely wrong conclusion IF it only uses set operations to check for set relations.

HOWEVER if elm-pubgrub uses list of available versions when checking set relations, then and only then, can it conclude that in Example 3 bar ^1.0.0 actually is same as bar 1.0.0 because there is only one version of bar, and so answer is YES.

malaire commented 4 years ago

And it appears that pub also doesn't have access at that time:

pub doesn't need to because it would only be needed when not merging/expanding version ranges.

malaire commented 4 years ago

Note that bar ^1.0.0 above comes from dependencies, so it's range both in pub and elm-pubgrub.

So stated another way:

in pub:

termFromDepencencies: bar ^1.0.0 termFromPickedVersion: bar any

in elm-pubgrub:

termFromDepencencies: bar ^1.0.0 termFromPickedVersion: bar 1.0.0

Problem:

However you implement relations-checking, it must conclude that in context of Example 3, termFromDepencencies satisfies termFromPickedVersion.

In case of pub this can be done using only set operations, without context.

In case of elm-pubgrub this can't be done using only set operations, without context, but needs to use context (i.e. the set of available versions).

p.s. It's not actually relevant that range is any. This issue would arise also with smaller range than any which is still superset of ^1.0.0.

malaire commented 4 years ago

You could also say that pub takes the context of other available versions into account when merging/expanding picked version to a range.

elm-pubgrub doesn't take this context into account at that point, so it must take that context into account at some other point. Currently it doesn't, which is why relation checking, and in extension conflict resolution, doesn't work.

While this was from Example 3, I believe it's highly likely that this is also behind this issue of Example 5bis failing.

mpizenberg commented 4 years ago

I'm pretty confident I've identified the issue. It has to do with prior cause computation but not what we thought on collapsing incompatibilities.

First the issue you raised is actually not a problem it turns out. In fact the step-by-step examples are a little bit idealized to be more easily readable. In practice, there is another kind of incompatibility in the algorithm that is left out of the explanations for matters of simplicity. These are "noVersion" incompatibilities and are mentioned in the detailed algorithm in the following decision making step:

If there is no such version, add an incompatibility {term} to the incompatibility set and return package's name. This tells Pubgrub to avoid this range of versions in the future.

In pub code this appears here: https://github.com/dart-lang/pub/blob/master/lib/src/solver/version_solver.dart#L380. In elm-pubgrub this corresponds to the Unknown variant of an incompatibility kind that should be renamed to NoVersion (or better, there should be some changes in the Incompatibility type).

What's interesting is that a non-optimal incompatibility (such as { bar 1, foo not (1 <=v < 2) }) will later trigger search for a version of bar in the range 1.0.1 <= v < 2 that is the rest of the search space. At the time of picking a version, which has access to packages and versions it will realize that no such version exist. As such, a new incompatibility will be generated of the form { bar : the rest of the search space }. This is what happens in the debug logs here:

   bar: 1.0.0 <= v < 2.0.0, foo: Not ( 1.0.0 <= v < 2.0.0 )  <<<  derived from:
      bar: 1.0.0, foo: Not ( 1.0.0 <= v < 2.0.0 )  <<<  from dependency of bar at version 1.0.0
      bar: 1.0.1 <= v < 2.0.0  <<<  from unknown reason ...: ""

Now onto the issue.

Remember the question whether or not the satisfier term has to be added to the initialization of the prior cause with both incompatibilities without their terms related to satisfier package? It turns out the same should be done for any package. Let me develop that. In example 5bis, after getting through the transitive bar dependency, the algorithm realizes that it will not be possible. At that point the following detailed logs for prior cause computation give:

previousLevel == satisfierLevel: ""
   satisfier bar Not ( 2.0.0 ): ""
   cause
      bar: 2.0.0, baz: Not ( 3.0.0 <= v < 4.0.0 )  <<<  from dependency of bar at version 2.0.0: ""
   incompat
      bar: 2.0.1 <= v < 3.0.0, baz: Not ( 2.0.0 <= v < 3.0.0 )  <<<  derived from:
         bar: 2.1.0, baz: Not ( 2.0.0 <= v < 3.0.0 )  <<<  from dependency of bar at version 2.1.0
         bar: [ 2.0.1, 2.1.0 [  [ 2.1.1, 3.0.0 [  <<<  from unknown reason ...: ""
   priorCause
   bar: 2.0.0 <= v < 3.0.0, baz: Not ( ∅ )  <<<  derived from:
      bar: 2.0.0, baz: Not ( 3.0.0 <= v < 4.0.0 )  <<<  from dependency of bar at version 2.0.0
      bar: 2.0.1 <= v < 3.0.0, baz: Not ( 2.0.0 <= v < 3.0.0 )  <<<  derived from:
         bar: 2.1.0, baz: Not ( 2.0.0 <= v < 3.0.0 )  <<<  from dependency of bar at version 2.1.0
         bar: [ 2.0.1, 2.1.0 [  [ 2.1.1, 3.0.0 [  <<<  from unknown reason ...: ""

Here the satisfier package is bar so the rest of the two incompatibilities used for priorCause initialization are

{ baz: Not ( 3.0.0 <= v < 4.0.0 ) }
and
{ baz: Not ( 2.0.0 <= v < 3.0.0 ) }

And the union of those to terms (logical "or") gives "not none". Actually, it turns out "not none" is always satisfied. Indeed it is satisfied if no version is selected (because it's negative) and it is satisfied if any version is selected. Instead, just like for the satisfier term that we do not add when not t1 is included in t2, we should not add a term to an incompatibility when the union is "not none". This is actually exactly the same thing, just expressed differently (here we could say that not (not (3 <= v < 4)) which is 3 <= v < 4 is included in not (2 <= v < 3)).

Because we do not do that, we have the incompatibility {bar: 2.0.0 <= v < 3.0.0, baz: Not ( ∅ )} in our set instead of just {bar: 2.0.0 <= v < 3.0.0}. And that incompatibility propagates later to {root: 1.0.0, baz: Not ( ∅ )} just before reaching the impossible state. Indeed the incompatibility {root: 1.0.0, baz: Not ( ∅ )} is a disguised terminal case, that would have been detected by the first condition of conflictResolution if it was in its canonical form {root: 1.0.0}.

if Dict.isEmpty (Incompatibility.asDict incompat) || Incompatibility.singlePositive root incompat then

I'm very confident that this will solve that issue. I just started to add notes to the code for places that need to change. Next weekend I can't work on this, the weekend after it all should be solved. Then there will only be error reporting left :)

mpizenberg commented 4 years ago

Actually the fix is pretty trivial, I just replaced the Incompatibility.fuse code by

fuse : String -> Term -> Term -> Incompatibility -> Incompatibility
fuse name t1 t2 incompatibility =
    let
        termUnion =
            Term.union t1 t2
    in
    if termUnion == Term.Negative Range.none then
        incompatibility

    else
        insert name (Term.union t1 t2) incompatibility

And it works on example 5bis, i.e. it stops and identify that root package can't be selected before reaching any impossible state.

mpizenberg commented 4 years ago

Also PS, there was a bug in Term.union. It was returning a positive term instead of a negative term when we have one of each. I've fixed it by union t1 t2 = not ( intersection (not t1) (not t2)). I'll also fix that properly in git in two weekends.

harrysarson commented 4 years ago

wow, this pubgrub is really tricky endevour. I guess this should not be too suprising as it is NP-hard. Is very impressive the progress made so far :+1:

mpizenberg commented 4 years ago

Solved in https://github.com/mpizenberg/elm-pubgrub/pull/5

malaire commented 4 years ago

I should just stick with the math I know. This algorithm is far too complex for me.