Re: [gentoo-dev] [RFC] Forced/automatic USE flag constraints (codename: ENFORCED_USE)

[Alexis Ballier]

On Fri, 09 Jun 2017 11:19:20 +0200
Michał Górny <mgorny@g.o> wrote:

> On śro, 2017-06-07 at 11:56 +0200, Alexis Ballier wrote:
> > On Wed, 07 Jun 2017 11:27:59 +0200
> > Michał Górny <mgorny@g.o> 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?

yes that's the point of it

> b. for all 'need toposort' results, the solve() should be able to find
> a solution with n>=1 iterations?

yes; though n is only bounded by the # of clauses (expanded as
implications) while it can be 1 if reorderer properly; I wouldn't bother
doing several iterations and just reject that at repoman side since it's
easily solved

> c. all of 'circular' results have at least one USE flag combination
> that can not be solved by solve()?

In theory no as that would imply your 1st b. In practice, I've only
seen cases like that.



> > > > 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.

Not sure what you mean by "more correct" but we've seen some
translations are easier to solve than others, while being logically
equivalent.

As for what developers would expect, I think that'd be some kind of
continuity of the solver: for 2 "close" inputs the solver gives "close"
outputs (whatever close means). One way to go towards that is the least
effort / least change from the solver part, which is why I always did
the bare minimum of changes to the input in the algorithm I proposed.

For example, if you negate them all in an AllOf clause, you get cases
where a lot can change:
For '?? ( a ( b c d e f ... z ) )' and USE="a b c ... z", it gives you
USE="a -b -c -d ... -z" changing 25 useflags.
If you just negate the first of the AllOf, you get as output
USE="a -b c d ... z" changing only one useflag.

[...]
> > > > > 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'.

I'm wrong actually. It can be falsified by setting foo to True and bar
to False. More on it below.

> > 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.

Interesting. Then we should, sadly, support that.

Let's think a bit about its meaning.
?? ( X Y ) is "if X then not Y".
?? ( a b? ( c ) ) is "if a then not "b? ( c )", that is, "if a then b
and not c", so that's rewritten as "a? ( b !c )".

That doesn't really seem to match your "basic idea". Instead, this
could be rewritten as:
b? ( ?? ( a c ) ) !b? ( ?? ( a ) )
that is: "b? ( a? ( !c ) )"

"If a and b are enabled then disable c" seems a much better
interpretation than "If a is enabled then enable b and disable c".


Now, we can apply your basic idea to bubble up all the implications so
that they're only at toplevel.

Something([begin Implication(X,Y) end]) is rewritten as:
Implication(X, Something([begin Y end]))
Implication(!X, Something([begin end]))

> 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.


With the above translation they should not make any difference for
nsolve: the two implications have different domain as one is X ->
something and the other is !X -> something.


> > > >
> > > > 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.

I think we're having communication interferences here :) That's exactly
what I'm talking about.

More specifically:

For each profile:
	formula=replace_masks_and_force_by_constants(required_use)
	simplify(formula)
	nsolve(formula)

In your example above, we'd call 'nsolve("|| ( X )")' and 'nsolve("||
( Y )")' (or even simpler, depending on how simplify() is defined). If
both X and Y are masked on a profile, then that'd reduce to
'nsolve("False")' which would rant.

I think that for solve(), reordering is basically equivalent since we
always favour leftmost. However, we have to somehow guarantee that
solve() will never try to enable a masked flag. This is guaranteed by
the above checks on profiles if enforced by repoman. If we apply the
same logic for solve that'd basically be built-in (masked/forced flags
wont appear in solve()'s input anymore), which I believe is better. Keep
in mind that users can mask and force some useflags, so the repoman
check won't catch that.


> > > > 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.
>

Yes, I agree. Since solve() and nsolve() are very related we should
carefully think how to organize the code then in order to avoid
duplication or them getting out of sync.

As for enabling it into repoman, I'm not sure which is best. Safest way
is obviously as you suggest, but a warning is not a blocker, so
enabling it by default can have a nice effect of receiving hate mails
from angry developers if something is wrong.

Alexis.