Stream: t-cargo/PubGrub

Topic: partial_solution


view this post on Zulip Matthieu Pizenberg (May 22 2021 at 14:44):

I'm in the process of rewriting the partial solution to get rid of the duality history/memory since it's something I had wanted to do for a looong time. I've all ready except the part with satisfiers which I'm dealing with now and giving me a headache ^^. I'll let you know if it goes well later today if I've found my way through.

view this post on Zulip Eh2406 (May 22 2021 at 15:09):

That is very cool! What is the plan?

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:12):

Right now this is my data structure:

/// The partial solution contains all package assignments,
/// organized by package and historically ordered.
#[derive(Clone)]
pub struct PartialSolution<P: Package, V: Version> {
    current_decision_level: DecisionLevel,
    package_assignments: Map<P, PackageAssignments<P, V>>,
}

/// Package assignments contain the potential decision and derivations
/// that have already been made for a given package,
/// as well as the intersection of terms by all of these.
#[derive(Clone)]
struct PackageAssignments<P: Package, V: Version> {
    smallest_decision_level: DecisionLevel,
    highest_decision_level: DecisionLevel,
    dated_derivations: Vec<DatedDerivation<P, V>>,
    assignments_intersection: AssignmentsIntersection<V>,
}

#[derive(Clone)]
pub struct DatedDerivation<P: Package, V: Version> {
    decision_level: DecisionLevel,
    cause: IncompId<P, V>,
}

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:14):

The major advantage is that accessing the right packages during conflict resolution is now a direct access, there is no need to go through the whole history to get packages relevant to a satisfied incompatibility.

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:15):

The main disadvantages that's giving me the headache is that I can't figure out how to actually perform conflict resolution if I don't have a unique reference index for each assignment.

view this post on Zulip Eh2406 (May 22 2021 at 15:17):

Can we use decision_level?

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:17):

I've been thinking quite a lot and I feel it's not easy because if packages are split by key in a map, it's hard to have more precise global order than what the decision level gives

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:17):

and with only decision level, the annoying thing is this:

Find the earliest assignment in the partial solution before satisfier such that incompatibility is satisfied by the partial solution up to and including that assignment plus satisfier. Call this previousSatisfier

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:18):

Because I can only identify "a package that has the same decision level than the satisfier" and not "the satisfier"

view this post on Zulip Eh2406 (May 22 2021 at 15:19):

hmmm....

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:19):

This results in the fact that if two different packages at the same decision level are potential satisfiers, I might end up picking the "wrong one"

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:19):

So I've been thinking "is there a wrong one actually"?

view this post on Zulip Eh2406 (May 22 2021 at 15:20):

I don't think so. the order we find incompats to be almost satisficed is not guaranteed.

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:24):

And there is this situation:

If I pick a2, there will be a previous satisfier since a1 exists, but if the actual satisfier was a2 and I pick b2 I won't find a previous satisfier since there is no package earlier that would satisfy package b ...

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:25):

Does it makes sense?

view this post on Zulip Eh2406 (May 22 2021 at 15:26):

I think so.

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:27):

I could also not bother too much and just store a unique index in addition to the decision level for each assignment. Make it work then improve

view this post on Zulip Eh2406 (May 22 2021 at 15:27):

That seams a resendable pan.

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:28):

If the performance is horrible, that's not by removing that u32 index that miracles will happen. But if it's good, we can think of improvements later

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 15:29):

alright I'll try that

view this post on Zulip Eh2406 (May 22 2021 at 15:31):

elm and synthetic do not have much backtracking. so brake even is a win for them.

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 19:55):

I've pushed what I got even though it does not pass the tests. I must have introduced a bug but my head is not clear enough to spot it anymore. The interesting stuff is in partial_solution_bis. I haven't removed anything, but by the end of this PR, we should be able to remove memory and assignment modules to be left with just partial_solution_bis renamed into partial_solution.

view this post on Zulip Eh2406 (May 22 2021 at 20:32):

A possible debugging approach, add a partial_solution_both that wraps both the old and new versions and asserts that they return the same thing for all methods.

view this post on Zulip Matthieu Pizenberg (May 22 2021 at 20:41):

that's smart! I might try tomorrow if I find the time!

view this post on Zulip Eh2406 (May 24 2021 at 00:45):

Ok looking into witch impl of previous_satisfier is "correct", I looked at:
the blog: https://medium.com/@nex3/pubgrub-2fb6470504f#cbda
the docs: https://github.com/dart-lang/pub/blob/master/doc/solver.md#conflict-resolution
and the impl: https://github.com/dart-lang/pub/blob/291705ca0b9632cb945dd39493dd5b9db41b897a/lib/src/solver/version_solver.dart#L201

and I don't think any two of them are the same thing!

view this post on Zulip Matthieu Pizenberg (May 24 2021 at 08:08):

I've tried to read carefully pub impl and I think it's the same as the docs, just implemented a tiny bit weirdly because she does only one pass and thus need the special treatment at https://github.com/dart-lang/pub/blob/291705ca0b9632cb945dd39493dd5b9db41b897a/lib/src/solver/version_solver.dart#L247 in order to correctly identify that previous satisfier. While we do a second pass where we initialize the accum term with the satisfier term so we don't need that special treatment.

view this post on Zulip Matthieu Pizenberg (May 24 2021 at 08:17):

Also, I tried displaying some stats for the resolution of the package "zuse-Minor(4)-All-FEATURES" and I obtained the following:

With your approach:

    Final state stats:
    Size of the incompatibility store: 152
    Size of saved incompatibilities: 282

    Partial solution stats:
    next_global_index: 174
    Number of derivations: 48

With the approach that choose the "correct" previous decision level:

    Final state stats:
    Size of the incompatibility store: 205
    Size of saved incompatibilities: 393

    Partial solution stats:
    next_global_index: 386
    Number of derivations: 53

So I think the intuition saying that applying a "rule of resolution" to find the previous cause of a satisfier package that is seen for the first time (the behavior change concerns only situations where there is no previous derivation to the one of the satisfier for that package) instead of backtracking (which would happen if some other package has a lower satisfier level) is a good heuristic. Because it essentially says: "try first to find the reason why we have that derived package term that we see for the first time"

view this post on Zulip Matthieu Pizenberg (May 25 2021 at 10:08):

So I think the intuition saying that applying a "rule of resolution" to find the previous cause of a satisfier package that is seen for the first time

Currently, the only way a term can appear for the first time is via an incompatibility (i12) generated by a previous package P1 depending on that package P2 (of the satisfied term). So essentially, if the satisfier is the first term of a given package P2, with the current rules of how terms can be generated, it means that the decision (picking P1) that lead to the incompatibility (i12) that lead to that first satisfier term was probably a wrong decision.

So instead of backtracking right away, we first apply the rule of resolution (https://pubgrub-rs-guide.netlify.app/internals/incompatibilities.html#rule-of-resolution) between the current incompat and the incompat (i12) cause of that satisfier term. Since they both have P2 in common and the term of the new one satisfies the term of the old one, we are in the simple situation of the type (Ta, -Tb) and (Tb, -Tc) implies (Ta, -Tc). And now we pick that derived new incompatibility and continue conflict resolution.

So essentially, the changes you introduced is like a shortcut to more general incompatibilities that works thanks to the fact that the only way a package term can appear for the first time is to be a derived term from the incompatibility generated by a package dependency.

The question is, if eventually we allow more ways for incompatibilities to appear (like just specifying forbidden versions, or whatever) would those new ways will be compatible with that shortcut? Or will it lead to unwanted behaviors (like infinite loop for example)?

view this post on Zulip Eh2406 (May 26 2021 at 13:58):

Let me see if I can talk thru an example.
In order for a incompat to have one term, (and not be root) it must be NoVersions or UnavailableDependencies. Something like Negative(bad=1.0.0).
In order for that to be satisfied the intersected term for bad must be Positive(bad=1.0.0).
In order for there to be only one assignment to the partial solution related to bad, it must be a dependency on bad. Something like foo 1.0.0 depends on bad 1.0.0.
So the "rule of resolution" does seam like the next logical step. In this example giving us Negative(foo=1.0.0)

view this post on Zulip Eh2406 (May 26 2021 at 14:01):

I don't see how that logic will change with any of the other kinds of incompatibilities I can think of adding. But we can change the code here when we add the new incompatibilities if it is making trouble.

view this post on Zulip Eh2406 (Jun 17 2021 at 17:09):

Sorry for going silent about this project for a while. I have been doing research trying to figure out what invariants the code has, buy adding debug_asserts, and by reading up on other SAT solvers. I think I am getting somewhere with understanding previous_satisfier. But can't quite get it in words yet.

view this post on Zulip Matthieu Pizenberg (Jun 19 2021 at 20:53):

no worry ^^. I'm quite silent too. We have had two interns arriving for the summer so I've had a bit more stuff to do than usual anyway. I'll try making progress on the advanced deps provider docs tomorrow. How is your computer doing?

view this post on Zulip Matthieu Pizenberg (Jun 19 2021 at 20:54):

Also, I'll probably be radio silent starting from next weekend until 14th of July

view this post on Zulip Eh2406 (Jun 19 2021 at 21:33):

How is your computer doing?

The tiny little $3 south bridge fan is broken. It is not a standard part. The manufacturer claims that it is absolutely necessary and I should not turn on the computer without it. So they will be happy to send me a replacement, as soon as they get them back in stock. But they don't know when that will be.

view this post on Zulip Eh2406 (Jun 19 2021 at 21:35):

I'll try making progress on the advanced deps provider docs tomorrow.

I am getting distracted by a new plan to impl the RangeTrait for Cargos Semver. I think this may work.

view this post on Zulip Matthieu Pizenberg (Jun 20 2021 at 07:36):

Eh2406 said:

How is your computer doing?

The tiny little $3 south bridge fan is broken. It is not a standard part. The manufacturer claims that it is absolutely necessary and I should not turn on the computer without it. So they will be happy to send me a replacement, as soon as they get them back in stock. But they don't know when that will be.

That sucks :(


Last updated: Oct 21 2021 at 21:46 UTC