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

[Michał Górny]

On pią, 2017-06-09 at 13:41 +0200, Alexis Ballier wrote:
> 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

I would prefer not having Portage fail randomly on local ebuilds where
the cost of multiple iterations is practically zero, and certainly it's
not worth the effort to ensure a particular ordering.

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

That was my thought as well. However, I've tested a few of example
failures and all of them broke solve() as well.

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

Well, I'm not sure if it can still plainly apply here but the generic
contract was that in implication clauses only RHS is mutable.

> > > 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]))

Makes sense. Not that I really like cartesian products but since I had
to do it for one thing already, I don't see a major problem splitting
this one as well. I'll try to implement it today.

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

So you're talking about reducing prior to transforming? Yes, that'd
work. As I mentioned in one of the first mails wrt my reference
implementation, I've used reordering (stable sort) instead of reducing
since it was simpler.

If you reduce (simplify), you need to account for special cases like
getting '|| ()' etc. If you reorder only, things just fail the normal
way.

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

There's wisdom in this as well. I'm just a little bit worried that we're
first make developers change their REQUIRED_USE, and then have to change
the algorithm anyway ;-).

-- 
Best regards,
Michał Górny