On śro, 2017-06-07 at 11:56 +0200, Alexis Ballier wrote: > On Wed, 07 Jun 2017 11:27:59 +0200 > Michał Górny <mgo...@gentoo.org> wrote: > > > On śro, 2017-06-07 at 10:17 +0200, Alexis Ballier wrote: > > > > Also, do I presume correctly that for all supported cases (i.e. > > > > those which your nsolve does not reject), solve and nsolve are > > > > compatible? > > > > > > Not sure what you mean here. nsolve does not solve anything, it just > > > validates REQUIRED_USE so that it is guaranteed it can be solved. > > > > What I mean is whether you can guarantee that: > > > > a. for every X that nsolve(X) == ok, solve() will be able to find > > a valid solution, > > yes > > > b. for every X that solve() can solve reliably, nsolve(X) == ok. > > no and that's not really possible
I thought so. To expand it a little, could you confirm whether I
correctly presume that:
a. for all 'good' results, the plain iterative solve() should be able to
find a solution with a single iteration?
b. for all 'need toposort' results, the solve() should be able to find
a solution with n>=1 iterations?
c. all of 'circular' results have at least one USE flag combination that
can not be solved by solve()?
> > > We first need to define properly & formally how to solve requse
> > > constraints if we want ppl to be able to rely on it (or rather write
> > > requse that give the expected result).
> > >
> > > The way I see it, REQUIRED_USE ast looks like:
> > > (assuming ^^ is already expanded to || + ??)
> > >
> > > clause =
> > > AllOf(list of clauses)
> > > | AnyOf(list of clauses)
> > > | AtMostOne(list of clauses)
> > > | Implication(useflag, clause)
> > > | useflag
> > >
> > > Now, portage already has the function 'eval(input, clause)'. We
> > > need to define 'trueify(input, clause)' that modifies input so that
> > > 'eval(input, clause)' is always true afterwards. Since this is SAT,
> > > there is no hope to make this work for all clauses. From the
> > > discussions here, a good algorithm would be:
> > >
> > > trueify(input, clause) = match clause with
> > > AllOf(l) -> for i in l: trueify(input, i)
> > > > AnyOf(l) -> if not eval(input, clause): trueify(input, l[0])
> > > > AtMostOne(l) -> f = (lambda x,y: pass)
> > >
> > > for i in l:
> > > f(input, i)
> > > if eval(input, i): f = falsify
> > > > Implication(useflag, consequence) ->
> > >
> > > if input[useflag]: trueify(input, consequence)
> > > > useflag -> input[useflag] = True
> > >
> > >
> > > Now you see that for the AtMostOne case we need its dual, the
> > > 'falsify(input, clause)' function:
> > >
> > > falsify(input, clause) = match clause with
> > > AllOf(l) -> falsify(input, l[0])
> >
> > That's a debatable case. My solve() actually 'falsifies' all
> > the subexpressions which might be more reliable.
>
> Best way to debate this is probably to write the implication
> translation and feed that to nsolve from a few test cases.
Exactly my thought. Since both algorithms should be kept in sync, it
probably makes sense to figure out the translation first and use
whatever makes it consistent without hacking on the translation hard.
I'll try to figure it out on paper today.
> Intuition is that falsifying all of them adds more pressure on the
> solver and you might end up failing to solve it for no good reason, so
> falsifying only one of them seems safer.
In either case, it's purely a matter of contract. You can't predict
which one will be more correct, and I think it's hard to even predict
which one developers will consider less surprising.
Besides, the all cases we had for this were pretty much meaningless,
and choosing A over B would only result in preferring clause X over Y
;-).
>
> > > > AnyOf(l) -> for i in l: falsify(input, i)
> > > > AtMostOne(l) -> for i in l:
> > >
> > > if eval(input, clause): trueify(input, i)
> >
> > Do I read this correctly that it pretty much implies enabling the
> > first two subexpressions?
>
> or the leftmost first false if one is already true in there, yes
>
> > > > Implication(useflag, consequence) ->
> > >
> > > if not input[useflag]: raise "impossible"
> >
> > Why impossible? Unless I'm missing something, it's false already.
>
> 'foo? bar' is always true if foo is false; so it's impossible to make
> it false
Yes, you are correct. I was actually thinking of 'if LHS is false, we do
not enforce RHS'.
> it's really a corner case as I think we don't allow nested implications
> inside ||, ^^, () or ??, which is the only way to reach that.
Strictly speaking, there's no rule prohibiting that. And I think we
actually have or had used 'foo?' inside '||' at least in dependencies.
The basic idea is that if the flag is disabled, the contents disappear
from the containing '||' block.
Now, this makes a lot of things harder. For plain solve(), it's not
a major problem -- worst case, we put an extra reordering on each
iteration based on enabled USE flags. For nsolve(), it's harder since it
makes the iteration graph PITA. I'll have to think if we can even
translate it reasonably.
> > >
> > > Note how the above favors leftmost in all cases. If it needs to
> > > change something, it always tries to leave the leftmost untouched.
> > > Note also that it processes everything left to right (the AllOf
> > > case where REQUIRED_USE="AllOf(list of clauses)" ).
> >
> > You need to be able to reorder the clauses to handle use.force
> > and use.mask.
>
> Not sure if reorder is the best way. It sure works, but maybe we'd want
> a repoman error if e.g. 'foo? ( bar )' is in REQUIRED_USE, bar is
> masked but not foo. That'd be a matter of eliminating the constants in
> the ast and if we get 'false' for a profile we error out.
Yes, we want that. It makes sense for pure implications. For n-ary
thingies, it's harder than that and I'd rather not require developers to
figure out a specific order to make things work.
Think of the following:
|| ( X Y )
with X being masked on profile A, Y being masked on profile B. You just
can't get it right then.
Of course, this is a bit unrealistic but I think a case when a preferred
(newer) provider is masked on some architectures is realistic. I don't
think we want to prefer a worse solution (or go back to applying
package.use workarounds) because of fringe arches.
Another question is whether we could solve this specific problem via
applying some kind of 'if forced/masked' logic into the AST.
> > > So, the very first thing to do is to agree that the above solver
> > > (the trueify function) is what we want to implement and set this in
> > > stone. There's no point in implementing a proper requse checker if
> > > the algorithm is meant to change. Having a formal definition will
> > > also be necessary to mandate that in future EAPIs.
> > >
> > > Then, and only then, we'd need to have the above solver implemented
> > > into portage (hidden under a FEATURES) and import my nsolve into
> > > repoman (after due cleanup).
> > >
> >
> > Yes, that's my goal. However, before we can set the algorithm in stone
> > we need to verify that it will work in all of the supported cases.
>
> Yep, that's the point of nsolve/classify :)
>
> > Preferably it should also be as simple as possible to avoid putting
> > too much complexity in the spec.
>
> Yes; not sure if anything simpler than the above can be achieved though.
>
Actually, I think we should roughly proceed in the following way:
1. Design the solve() algorithm.
1a. Test solve() on isolated test cases.
1b. Integrate solve() into Portage (as optional feature) and encourage
wider testing.
2. Design the nsolve() verification based on solve().
2a. Test nsolve() separately.
2b. Start fixing simple cases that do not bring any controversy (like
most of the reorderings).
2c. Integrate nsolve() into repoman.
3. Spec the whole thing and decide how to go next.
Assuming that 1* and 2* is to be done simultaneously, and each subpoint
implies that if we hit any walls, we can go back to a previous point and
fix the design.
I think we're mostly past 1a and 2a now. We should try to think a bit
more about the corner cases right now, and when we're done with that,
the next step would be to:
A. start fixing some cases ('need topo sort' at least?) to improve
testing area for the implementation,
B. integrate solve() into Portage,
C. maybe optionally integrate nsolve() into repoman.
However, I don't want to set the spec into stone until we have some live
testing via Portage with FEATURES=solve-required-use or alike. For
repoman, we can add the verification optionally (i.e. with the above
feature or via a separate command-line option) but I don't think we
should enable it by default until we verify it.
--
Best regards,
Michał Górny
signature.asc
Description: This is a digitally signed message part
