Tests fail when using semantic Eq for Term about pubgrub HOT 7 CLOSED

This took me a few attempts to get my head around when I was first optimizing the code base. I think I had a branch where I entirely removed Term and used VS directly - removing tests to make things work - until the prop tests pointed out that I was getting the wrong answer.

If a version is selected then Positive(r) <=> Negative(r.complement()), but they have different semantics when no version is selected. A Positive term in the partial solution requires a version to be selected. But a Negative term allows for a solution that does not have that package selected.

For example the incompatibility for not root is Negative(singleton(version)). Interpreted as "there shall be no solution (this negation from the definition of incompatibility) where root is different from version or where root is unselected". Whereas the incompatibility for no versions is the very similar Positive(set). Interpreted as "there shall be no solution where p is in set but if p is unselected that's fine". The proposed definition of equality means that the incompatibilities for "we require package p @ v" and "v is the only version of p" are equivalent. This builds up to bugs because "v is the only version of p" implies "we require package p @ v" implies "we need to select versions that match the dependencies of p @ v".

Here's a totally different way to think about it.
A VS has the basic operation contains, which takes a V and returns a bool. A VS is a Set<V>, a set whose members are Vs. It takes a version and decides whether it's happy with that version.
If Term had a contains operation, it would take an Option<V> and return a bool. A Term is a Set<Option<V>>, a set whose members are Option<V>s. It takes a (version|None) and decides whether it's happy with it.
Because Term handles one more potential input than its underlying VS, Term needs to maintain one bit of additional data. The current implementation stores that bit in the Enum discriminate.

I have thought about adding contains to Term, or implementing VersionSet on Term, to hang this documentation on and make it clear to the next contributor what the differences. But I have not found a use for that method that is important enough for the next zealous contributor not to remove/ignore while simplifying things.
I am open to additional code or a different representation if it makes these important distinctions easier to remember.

from pubgrub.

The question for me is, how should this behave through T1 <op> T2? E.g. for intersection and union we have on dev:

Intersection:

Positive, Positive -> Positive
Positive, Negative -> Positive
Negative, Positive -> Positive
Negative, Negative -> Negative

Union (First equals by dev definition):

Union(Positive, Positive) = Not (Intersection(Not Positive, Not Positive)) -> Not (Negative) -> Positive
Union(Positive, Negative) = Not (Intersection(Not Positive, Not Negative)) -> Not (Positive) -> Negative
Union(Negative, Positive) = Not (Intersection(Not Negative, Not Positive)) -> Not (Positive) -> Negative
Union(Negative, Negative) = Not (Intersection(Not Negative, Not Negative)) -> Not (Positive) -> Negative

But even when upholding that and using the derived equals definition, i'm getting failing tests.

from pubgrub.

By careful use of re-factor>in-line and repeatedly running tests, this seems to work:

    pub(crate) fn union(&self, other: &Self) -> Self {
        use self::Term::*;
        match (self, other) {
            (Positive(r1), Positive(r2)) => Positive(r1.union(r2)),
            (Positive(r1), Negative(r2)) => Negative(r1.complement().intersection(r2)),
            (Negative(r1), Positive(r2)) => Negative(r1.intersection(&r2.complement())),
            (Negative(r1), Negative(r2)) => Negative(r1.intersection(r2)),
        }
    }

This makes some amount of intuitive sense. The definition of union is that if an input is contained in either one, that must be contained in the union. And if either term is Negative then None is an included version and so must be included in the union.

from pubgrub.

I figured out why the tests still failed, is_disjoint has to return false for negative ∩ negative since it can never be a positive empty term.

Should we document the expectations on intersection and union?

from pubgrub.

I'm always up for more documentation or tests!

from pubgrub.

What i haven't fully understood yet, where a new positive or negative terms "minted", and how do the rules for intersections follow from this?

from pubgrub.

What i haven't fully understood yet, where a new positive or negative terms "minted"

They are constructed in the creation of incompatibilities. For example both kinds are used in the normal construction of a dependency incompatibility https://github.com/pubgrub-rs/pubgrub/blob/dev/src/internal/incompatibility.rs#L117

and how do the rules for intersections follow from this?

The definition of intersection is that an input is only contained in the intersection if it is contained in both. And if either term is Negative then None is an excluded version and so must be excluded in the intersection.

from pubgrub.