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

["Michał Górny" <mgorny@gentoo.org>]

[-- Attachment #1: Type: text/plain, Size: 6023 bytes --]

(cut off the parts where I agree and there's nothing to add)

On pią, 2017-06-09 at 16:16 +0200, Alexis Ballier wrote:
> [...]
> > > 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.
> 
> While the reordering idea seems nice as it factors both user
> preference and masks, the problem with reordering is that nothing
> guarantees that the solver won't try to enable a masked flag. We'd have
> to deal with that somehow.

Well, yes and no.

The algorithm always needs to account for the possibility of constraints
altering immutable flags. Of course, there's more than one way of doing
it.

AFAIU you are aiming for separate processing of immutable flags
and explicit failure if the constraints would attempt to force value of
those flags. That surely makes sense for verification.

My approach was simpler -- marking the flags immutable, and failing if
something actually tries to alter their value. I think it's a simpler
solution for the plain solver and it works as well. After all, we do not
want the solver to attempt to find workarounds for the problem but just
fail.

The above applies clearly to the plain conflicts such as:

  foo? ( bar )

where bar is immutable. The n-ary operators can be flexed a little.
That's what reordering achieves -- it makes sure they come as the most
or the least preferred as appropriate. Which means that the same
algorithm either succeeds (by not having to touch them) or fails at
attempting to flip them.

Think of:

  ?? ( a b c )

with both b&c in use.force. This gets reordered to:

  ?? ( b c a )

The order between b&c doesn't matter. Since b comes first now, it forces
c being disabled. Since c is immutable, the solver fails with
ImmutabilityError. We solve the problem with minimal code redundancy.


> I think reordering should be kept for user preferences
> (soft-enable/soft-disable) while masks for hard-no's or hard-yes'es.
> 
> 
> Be careful with reordering though:
> '^^ ( a b ) b? ( a )' can be solved in one pass.
> (it disables b if both are set and enables a if none are set)
> 
> while:
> '^^ ( b a ) b? ( a )' loops
> (if both are set it disables 'a' for the 1st clause but then enables it
> for the 2nd)
> 
> This is not checked by nsolve().

Yes, this is a problem I was considering. I planned to think a bit if we
could possibly generate some more complex transformations to trigger
nsolve to notice this kind of issues.


And now two updates on other matters.

Firstly, all-of inside ??. Per the construct:

  ?? ( ( a b ) c )

the expansion would be:

  [a b]? ( !c ) c? ( ![a b] )

which means we should be able to easily affect the effective behavior of
both implementations by defining how to handle/expand negations of all-
of groups.

It's then a matter of replacing it with:

a. !a, or

b. !a !b.

As you pointed out, a. has the advantage that we alter less flags. b.
has the advantage that we alter more flags -- so it's less likely we'll
actually leave some unused flag enabled. Whichever we choose, it
probably doesn't matter as I can't think of a valid use case for this
constraint that would clearly define the result.


Secondly, nested n-ary operators. I have taken the following snippet as
a simple example:

  || ( a || ( b c ) )

Logically (and per constraint checking algo), this should be equivalent
to:

  || ( a b c )

However, if we expand it to implication form, we get:

  ![ || ( b c ) ] => a

  ![ !c => b ] => a

At this point, we already see some contract problem/ambiguity. Per
contract, we are supposed not to alter any flags on LHS of implication.
However, we have another implication there, so it is unclear if RHS of
that nested implication should be mutable or not.

Let's consider the nested implication first:

  !c => b

Per the constraint checking rules, this constraint is met (evaluates to
true) either if c is enabled, or both c is disabled and b is enabled.
In other words, it fails (evaluates to false) only if both b and c are
disabled. Putting that into a table we get:

  b c | ?
  0 0 | 0 (fail -- LHS matches, RHS does not)
  0 1 | 1 (LHS does not match)
  1 0 | 1 (LHS & RHS matches)
  1 1 | 1 (LHS does not match)

Per the solving rules, in the only failing case we should enforce RHS --
i.e. enable b.

Now, let's consider its negation:

  ![ !c => b ]

Per the rules of logic, it is true (= matches the constraint) only if
both b and c are disabled. While it is unclear if we should be enforcing
RHS inside negation, logically saying I don't think it can actually
happen. Because:

1. if b=c=0, the whole negated constraint is satisfied, so we shouldn't
apply any solving to it (attempting to solve it would be inconsistent
with the case where whole REQUIRED_USE is satisfied immediately),

2. in any other case, the inner constraint is satisfied, so there's no
change to be applied.

That considered, I think we could reasonably replace the negation of
implication with plain conjunction of LHS and negation of RHS:

  [ !c !b ]

This would render the outer expression as:

  [ !c !b ] => a

which is equivalent to || ( a b c ).

The question is whether applying that rule for implications nested on
LHS of another implication is going to work fine for all our expansions.

-- 
Best regards,
Michał Górny

[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 988 bytes --]