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

[Alexis Ballier]

On Thu, 15 Jun 2017 18:48:42 +0100
Ciaran McCreesh  wrote:

> On Thu, 15 Jun 2017 19:30:02 +0200
> Alexis Ballier  wrote:
> > On Thu, 15 Jun 2017 18:04:35 +0100
> > Ciaran McCreesh  wrote:  
> > > On Thu, 15 Jun 2017 18:55:45 +0200
> > > Alexis Ballier  wrote:
> > > > The guarantee comes from the fact that the output is always in
> > > > the space of all possible inputs from the user. So, if some
> > > > output will kill a kitten, so does some input.  
> > > 
> > > USE=minimal
> > > USE=mips
> > > USE=-ssl
> > > 
> > 
> > So what?  
> 
> So, if the aim of this solution is to make things better for the user,
> what are you doing to establish that this will make things better for
> the user instead of recommending something awful?
> 

Considering that the way you write REQUIRED_USE defines how the solver
behaves, your problem is ill defined.

If I try to ask my crystal ball, I would say: USE=mips is either masked
or forced so never an option. Developer would not want USE=minimal to
be toggled randomly so would write a constraint so that it always
appears e.g. on the left part of an implication.

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

[Alexis Ballier]

On Thu, 15 Jun 2017 19:38:48 +0200
Michał Górny  wrote:

> On czw, 2017-06-15 at 18:07 +0200, Alexis Ballier wrote:
> > On Thu, 15 Jun 2017 17:59:13 +0200
> > Michał Górny  wrote:
> >   
> > > On śro, 2017-06-14 at 16:09 +0200, Alexis Ballier wrote:  
> > > > On Wed, 14 Jun 2017 15:57:38 +0200
> > > > Michał Górny  wrote:
> > > > [...]
> > > > > > [...]  
> > > > > > > > > > > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse  
> > > > > > > > > > > 
> > > > > > > > > > 
> > > > > > > > > > I really don't like the reordering thing. Even the
> > > > > > > > > > restricted syntax does not fix the issue with '^^
> > > > > > > > > > ( a b ) b? ( a )' already mentioned here. It'd be
> > > > > > > > > > much better and simpler for the spec just to assign
> > > > > > > > > > a fixed value and use the solving rules with
> > > > > > > > > > those.  
> > > > > > > > > 
> > > > > > > > > You're not going to convince me by providing examples
> > > > > > > > > that are utterly broken by design and
> > > > > > > > > meaningless ;-).
> > > > > > > > 
> > > > > > > > Well... if it's so obvious that the example is broken by
> > > > > > > > design that you don't even bother to explain why, I
> > > > > > > > assume you have an algorithm for that. Where is the
> > > > > > > > code ? What are the numbers ? How many ebuilds might
> > > > > > > > fail after reordering ? How can this be
> > > > > > > > improved ?
> > > > > > > 
> > > > > > > Are you arguing for the sake of arguing here? I just
> > > > > > > presumed that this example is so obviously broken there
> > > > > > > is no point wasting any more time on it. The code of
> > > > > > > nsolve clearly detects that, so I don't really understand
> > > > > > > what you're trying to prove here.  
> > > > > > 
> > > > > > Those are real questions. You should take breath, think a
> > > > > > bit about it, and try to run the 2 possible orderings of
> > > > > > the ^^ through nsolve or even solve.py. They both are very
> > > > > > happy (and are right to be) with the above ordering. You
> > > > > > might want to think a bit more about what is the relation
> > > > > > between this broken 10 chars example and the 10 lines
> > > > > > python targets one below.
> > > > > > 
> > > > > > You should also realize that all the above questions have
> > > > > > already been answered in length if you do as I
> > > > > > suggest.  
> > > > > 
> > > > > No. I have already spent too much time on this. We're already
> > > > > long past all useful use cases, and now I feel like you're
> > > > > going to argue to death just to find a perfect algorithm that
> > > > > supports every absurd construct anyone can even write, if
> > > > > only to figure out the construct is completely useless.
> > > > 
> > > > I'm not going to argue to death. It's already proven reordering
> > > > is broken.
> > > > 
> > > > > If you want to play with it more, then please by all means do
> > > > > so.
> > > > 
> > > > There is nothing to do for reordering. It's broken by design.
> > > > 
> > > > > However, do not expect me to waste any more of my time on it.
> > > > > I've done my part, the code works for all reasonable use
> > > > > cases and solves all the problems I needed solving. If you
> > > > > want more, then it's your job to do it and solve the
> > > > > resulting issues.
> > > > 
> > > > Like... writing code handling all the cases and describing how
> > > > it works ? We're past that. The only thing we're not past is
> > > > that you fail to understand it and attempt to block it.
> > > > 
> > > 
> > > Then please provide a single valid example that:  
> > 
> > app-text/wklej-0.2.1-r1 ^^ ( python_single_target_pypy
> > python_single_target_pypy3 python_single_target_python2_7
> > python_single_target_python3_4 python_single_target_python3_5
> > python_single_target_python3_6 ) python_single_target_pypy?
> > ( python_targets_pypy ) python_single_target_pypy3?
> > ( python_targets_pypy3 ) python_single_target_python2_7?
> > ( python_targets_python2_7 ) python_single_target_python3_4?
> > ( python_targets_python3_4 ) python_single_target_python3_5?
> > ( python_targets_python3_5 ) python_single_target_python3_6?
> > ( python_targets_python3_6 ) vim? ( ^^
> > ( python_single_target_python2_7 ) )
> > 
> > 
> > Simplified as:
> > ^^ ( a b ) c? ( b )
> > 
> > (see the pattern now ? :) )
> >   
> > > a. is completely 'correct' (that is, provides a valid, predictable
> > > and acceptable solution) with the default ordering O_a,  
> > 
> > c? ( b ) ^^ ( b a )
> > 
> >   
> > > b. is not 'correct' with at least one reordering O_b (assuming
> > > only  
> > > > > , ^^, ?? is subject to reordering),  
> > 
> > c? ( b ) ^^ ( a b )
> >   
> > > 
> > > c. nsolve reports O_a as all good, and O_b as not good.  
> > 
> > I'll let you run this. It does.
> >   
> > > The best way to convince me is 

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

[Ciaran McCreesh]

On Thu, 15 Jun 2017 19:30:02 +0200
Alexis Ballier  wrote:
> On Thu, 15 Jun 2017 18:04:35 +0100
> Ciaran McCreesh  wrote:
> > On Thu, 15 Jun 2017 18:55:45 +0200
> > Alexis Ballier  wrote:  
> > > The guarantee comes from the fact that the output is always in the
> > > space of all possible inputs from the user. So, if some output
> > > will kill a kitten, so does some input.
> > 
> > USE=minimal
> > USE=mips
> > USE=-ssl
> >   
> 
> So what?

So, if the aim of this solution is to make things better for the user,
what are you doing to establish that this will make things better for
the user instead of recommending something awful?

-- 
Ciaran McCreesh

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

[Michał Górny]

On czw, 2017-06-15 at 18:07 +0200, Alexis Ballier wrote:
> On Thu, 15 Jun 2017 17:59:13 +0200
> Michał Górny  wrote:
> 
> > On śro, 2017-06-14 at 16:09 +0200, Alexis Ballier wrote:
> > > On Wed, 14 Jun 2017 15:57:38 +0200
> > > Michał Górny  wrote:
> > > [...]  
> > > > > [...]
> > > > > > > > > > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse
> > > > > > > > > > 
> > > > > > > > > 
> > > > > > > > > I really don't like the reordering thing. Even the
> > > > > > > > > restricted syntax does not fix the issue with '^^ ( a b
> > > > > > > > > ) b? ( a )' already mentioned here. It'd be much better
> > > > > > > > > and simpler for the spec just to assign a fixed value
> > > > > > > > > and use the solving rules with those.
> > > > > > > > 
> > > > > > > > You're not going to convince me by providing examples
> > > > > > > > that are utterly broken by design and
> > > > > > > > meaningless ;-).  
> > > > > > > 
> > > > > > > Well... if it's so obvious that the example is broken by
> > > > > > > design that you don't even bother to explain why, I assume
> > > > > > > you have an algorithm for that. Where is the code ? What
> > > > > > > are the numbers ? How many ebuilds might fail after
> > > > > > > reordering ? How can this be improved ?  
> > > > > > 
> > > > > > Are you arguing for the sake of arguing here? I just presumed
> > > > > > that this example is so obviously broken there is no point
> > > > > > wasting any more time on it. The code of nsolve clearly
> > > > > > detects that, so I don't really understand what you're trying
> > > > > > to prove here.
> > > > > 
> > > > > Those are real questions. You should take breath, think a bit
> > > > > about it, and try to run the 2 possible orderings of the ^^
> > > > > through nsolve or even solve.py. They both are very happy (and
> > > > > are right to be) with the above ordering. You might want to
> > > > > think a bit more about what is the relation between this broken
> > > > > 10 chars example and the 10 lines python targets one below.
> > > > > 
> > > > > You should also realize that all the above questions have
> > > > > already been answered in length if you do as I suggest.
> > > > 
> > > > No. I have already spent too much time on this. We're already long
> > > > past all useful use cases, and now I feel like you're going to
> > > > argue to death just to find a perfect algorithm that supports
> > > > every absurd construct anyone can even write, if only to figure
> > > > out the construct is completely useless.  
> > > 
> > > I'm not going to argue to death. It's already proven reordering is
> > > broken.
> > >   
> > > > If you want to play with it more, then please by all means do
> > > > so.  
> > > 
> > > There is nothing to do for reordering. It's broken by design.
> > >   
> > > > However, do not expect me to waste any more of my time on it. I've
> > > > done my part, the code works for all reasonable use cases and
> > > > solves all the problems I needed solving. If you want more, then
> > > > it's your job to do it and solve the resulting issues.  
> > > 
> > > Like... writing code handling all the cases and describing how it
> > > works ? We're past that. The only thing we're not past is that you
> > > fail to understand it and attempt to block it.
> > >   
> > 
> > Then please provide a single valid example that:
> 
> app-text/wklej-0.2.1-r1 ^^ ( python_single_target_pypy
> python_single_target_pypy3 python_single_target_python2_7
> python_single_target_python3_4 python_single_target_python3_5
> python_single_target_python3_6 ) python_single_target_pypy?
> ( python_targets_pypy ) python_single_target_pypy3?
> ( python_targets_pypy3 ) python_single_target_python2_7?
> ( python_targets_python2_7 ) python_single_target_python3_4?
> ( python_targets_python3_4 ) python_single_target_python3_5?
> ( python_targets_python3_5 ) python_single_target_python3_6?
> ( python_targets_python3_6 ) vim? ( ^^ ( python_single_target_python2_7
> ) )
> 
> 
> Simplified as:
> ^^ ( a b ) c? ( b )
> 
> (see the pattern now ? :) )
> 
> > a. is completely 'correct' (that is, provides a valid, predictable
> > and acceptable solution) with the default ordering O_a,
> 
> c? ( b ) ^^ ( b a )
> 
> 
> > b. is not 'correct' with at least one reordering O_b (assuming only
> > > > , ^^, ?? is subject to reordering),
> 
> c? ( b ) ^^ ( a b )
> 
> > 
> > c. nsolve reports O_a as all good, and O_b as not good.
> 
> I'll let you run this. It does.
> 
> > The best way to convince me is through valid examples.
> 
> 
> It is also easier to be convinced when you try to understand and ask
> for clarifications instead of just rejecting without thinking :)
> 

Ok, now I get your point. Not that I like it but I don't see any sane
way around it.

The question then is, how can you reliably ensure that developers will
use the same ordering in cross-relevant packages? For example, consider
the 

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

[Alexis Ballier]

On Thu, 15 Jun 2017 18:04:35 +0100
Ciaran McCreesh  wrote:

> On Thu, 15 Jun 2017 18:55:45 +0200
> Alexis Ballier  wrote:
> > The guarantee comes from the fact that the output is always in the
> > space of all possible inputs from the user. So, if some output will
> > kill a kitten, so does some input.  
> 
> USE=minimal
> USE=mips
> USE=-ssl
> 

So what?

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

[Ciaran McCreesh]

On Thu, 15 Jun 2017 18:55:45 +0200
Alexis Ballier  wrote:
> The guarantee comes from the fact that the output is always in the
> space of all possible inputs from the user. So, if some output will
> kill a kitten, so does some input.

USE=minimal
USE=mips
USE=-ssl

-- 
Ciaran McCreesh

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

[Alexis Ballier]

On Thu, 15 Jun 2017 17:45:09 +0100
Ciaran McCreesh  wrote:

> On Thu, 15 Jun 2017 18:37:16 +0200
> Alexis Ballier  wrote:
> > > So you're saying that at the end of this, there's an ENFORCED_USE
> > > solver that spits out some answer that may or may not be in any
> > > way a sane solution to the conflict.
> > > 
> > > I don't see how that's helpful to a user.  
> > 
> > Define sane.
> > The definition of the solver is made to change the least possible of
> > the inputs and is completely and easily predictable by the person
> > writing the constraint. That is something I would call sane.  
> 
> The problem is not just writing a resolver that spits out a valid
> output. The problem is writing a resolver which will never go and
> uninstall bash as a result of unintended combinations of inputs (which
> Portage used to do, but there's now a special exception for system
> packages, so it will only occasionally unexpectedly uninstall critical
> packages that aren't explicitly in system due to virtuals instead).
> This is *hard*.

We're not talking about solving deps here.

> A bad suggestion to the user is worse than no suggestion at all.
> Unless you can safely determine that there aren't any unintended
> consequences of your rule, the focus needs to be on producing good
> error messages so the user can figure the problem out, not on
> producing bad solutions that will confuse things even more.

The guarantee comes from the fact that the output is always in the
space of all possible inputs from the user. So, if some output will
kill a kitten, so does some input.

Of course, implementation can decide to error out and propose a
solution, to continue but print big fat warnings, etc. I like the
initial proposal in that regard.


Alexis.

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

[Ciaran McCreesh]

On Thu, 15 Jun 2017 18:37:16 +0200
Alexis Ballier  wrote:
> > So you're saying that at the end of this, there's an ENFORCED_USE
> > solver that spits out some answer that may or may not be in any way
> > a sane solution to the conflict.
> > 
> > I don't see how that's helpful to a user.
> 
> Define sane.
> The definition of the solver is made to change the least possible of
> the inputs and is completely and easily predictable by the person
> writing the constraint. That is something I would call sane.

The problem is not just writing a resolver that spits out a valid
output. The problem is writing a resolver which will never go and
uninstall bash as a result of unintended combinations of inputs (which
Portage used to do, but there's now a special exception for system
packages, so it will only occasionally unexpectedly uninstall critical
packages that aren't explicitly in system due to virtuals instead).
This is *hard*.

A bad suggestion to the user is worse than no suggestion at all. Unless
you can safely determine that there aren't any unintended consequences
of your rule, the focus needs to be on producing good error messages
so the user can figure the problem out, not on producing bad solutions
that will confuse things even more.

-- 
Ciaran McCreesh 

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

[Alexis Ballier]

On Thu, 15 Jun 2017 17:32:40 +0100
Ciaran McCreesh  wrote:

> On Thu, 15 Jun 2017 18:30:10 +0200
> Alexis Ballier  wrote:
> > On Thu, 15 Jun 2017 17:22:26 +0100
> > Ciaran McCreesh  wrote:  
> > > On Thu, 15 Jun 2017 18:19:04 +0200
> > > Alexis Ballier  wrote:
> > > > On Thu, 15 Jun 2017 17:13:57 +0100
> > > > Ciaran McCreesh  wrote:  
> > > > > On Thu, 15 Jun 2017 18:07:00 +0200
> > > > > Alexis Ballier  wrote:
> > > > > > > The best way to convince me is through valid
> > > > > > > examples.
> > > > > > 
> > > > > > It is also easier to be convinced when you try to understand
> > > > > > and ask for clarifications instead of just rejecting without
> > > > > > thinking :)  
> > > > > 
> > > > > The problem with this entire proposal is that it's still in
> > > > > "well I can't think of how it could possibly go wrong"
> > > > > territory. We need a formal proof that it's sound. History has
> > > > > shown that if something can be abused by Gentoo developers, it
> > > > > will be abused...
> > > > 
> > > > Had you read the thread you would have noticed that I provided
> > > > an algorithm giving sufficient conditions for the solver to
> > > > work. That is, if developers pay attention to repoman
> > > > warnings/errors, it will never fail. Obviously, since we're
> > > > still in the SAT space, you can ignore the errors and make it
> > > > fail, but it'll never be worse than what we currently
> > > > have.  
> > > 
> > > You have shown that you produce a solution, not the solution
> > > that's actually wanted.  
> > 
> > Since 'wanted' is still undefined, I'd say it produces the defined
> > solution and you can adapt to the definition to get what you want.  
> 
> So you're saying that at the end of this, there's an ENFORCED_USE
> solver that spits out some answer that may or may not be in any way a
> sane solution to the conflict.
> 
> I don't see how that's helpful to a user.
> 

Define sane.
The definition of the solver is made to change the least possible of
the inputs and is completely and easily predictable by the person
writing the constraint. That is something I would call sane.

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

[Ciaran McCreesh]

On Thu, 15 Jun 2017 18:30:10 +0200
Alexis Ballier  wrote:
> On Thu, 15 Jun 2017 17:22:26 +0100
> Ciaran McCreesh  wrote:
> > On Thu, 15 Jun 2017 18:19:04 +0200
> > Alexis Ballier  wrote:  
> > > On Thu, 15 Jun 2017 17:13:57 +0100
> > > Ciaran McCreesh  wrote:
> > > > On Thu, 15 Jun 2017 18:07:00 +0200
> > > > Alexis Ballier  wrote:  
> > > > > > The best way to convince me is through valid
> > > > > > examples.  
> > > > > 
> > > > > It is also easier to be convinced when you try to understand
> > > > > and ask for clarifications instead of just rejecting without
> > > > > thinking :)
> > > > 
> > > > The problem with this entire proposal is that it's still in
> > > > "well I can't think of how it could possibly go wrong"
> > > > territory. We need a formal proof that it's sound. History has
> > > > shown that if something can be abused by Gentoo developers, it
> > > > will be abused...  
> > > 
> > > Had you read the thread you would have noticed that I provided an
> > > algorithm giving sufficient conditions for the solver to work.
> > > That is, if developers pay attention to repoman warnings/errors,
> > > it will never fail. Obviously, since we're still in the SAT
> > > space, you can ignore the errors and make it fail, but it'll
> > > never be worse than what we currently have.
> > 
> > You have shown that you produce a solution, not the solution that's
> > actually wanted.
> 
> Since 'wanted' is still undefined, I'd say it produces the defined
> solution and you can adapt to the definition to get what you want.

So you're saying that at the end of this, there's an ENFORCED_USE
solver that spits out some answer that may or may not be in any way a
sane solution to the conflict.

I don't see how that's helpful to a user.

-- 
Ciaran mcCreesh

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

[Alexis Ballier]

On Thu, 15 Jun 2017 17:22:26 +0100
Ciaran McCreesh  wrote:

> On Thu, 15 Jun 2017 18:19:04 +0200
> Alexis Ballier  wrote:
> > On Thu, 15 Jun 2017 17:13:57 +0100
> > Ciaran McCreesh  wrote:  
> > > On Thu, 15 Jun 2017 18:07:00 +0200
> > > Alexis Ballier  wrote:
> > > > > The best way to convince me is through valid examples.
> > > > 
> > > > It is also easier to be convinced when you try to understand and
> > > > ask for clarifications instead of just rejecting without
> > > > thinking :)  
> > > 
> > > The problem with this entire proposal is that it's still in "well
> > > I can't think of how it could possibly go wrong" territory. We
> > > need a formal proof that it's sound. History has shown that if
> > > something can be abused by Gentoo developers, it will be
> > > abused...
> > 
> > Had you read the thread you would have noticed that I provided an
> > algorithm giving sufficient conditions for the solver to work. That
> > is, if developers pay attention to repoman warnings/errors, it will
> > never fail. Obviously, since we're still in the SAT space, you can
> > ignore the errors and make it fail, but it'll never be worse than
> > what we currently have.  
> 
> You have shown that you produce a solution, not the solution that's
> actually wanted.
> 

Since 'wanted' is still undefined, I'd say it produces the defined
solution and you can adapt to the definition to get what you want.

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

[Ciaran McCreesh]

On Thu, 15 Jun 2017 18:19:04 +0200
Alexis Ballier  wrote:
> On Thu, 15 Jun 2017 17:13:57 +0100
> Ciaran McCreesh  wrote:
> > On Thu, 15 Jun 2017 18:07:00 +0200
> > Alexis Ballier  wrote:  
> > > > The best way to convince me is through valid examples.  
> > > 
> > > It is also easier to be convinced when you try to understand and
> > > ask for clarifications instead of just rejecting without
> > > thinking :)
> > 
> > The problem with this entire proposal is that it's still in "well I
> > can't think of how it could possibly go wrong" territory. We need a
> > formal proof that it's sound. History has shown that if something
> > can be abused by Gentoo developers, it will be abused...  
> 
> Had you read the thread you would have noticed that I provided an
> algorithm giving sufficient conditions for the solver to work. That
> is, if developers pay attention to repoman warnings/errors, it will
> never fail. Obviously, since we're still in the SAT space, you can
> ignore the errors and make it fail, but it'll never be worse than what
> we currently have.

You have shown that you produce a solution, not the solution that's
actually wanted.

-- 
Ciaran McCreesh

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

[Alexis Ballier]

On Thu, 15 Jun 2017 17:13:57 +0100
Ciaran McCreesh  wrote:

> On Thu, 15 Jun 2017 18:07:00 +0200
> Alexis Ballier  wrote:
> > > The best way to convince me is through valid examples.
> > 
> > It is also easier to be convinced when you try to understand and ask
> > for clarifications instead of just rejecting without thinking :)  
> 
> The problem with this entire proposal is that it's still in "well I
> can't think of how it could possibly go wrong" territory. We need a
> formal proof that it's sound. History has shown that if something can
> be abused by Gentoo developers, it will be abused...

Had you read the thread you would have noticed that I provided an
algorithm giving sufficient conditions for the solver to work. That
is, if developers pay attention to repoman warnings/errors, it will
never fail. Obviously, since we're still in the SAT space, you can
ignore the errors and make it fail, but it'll never be worse than what
we currently have.

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

[Ciaran McCreesh]

On Thu, 15 Jun 2017 18:07:00 +0200
Alexis Ballier  wrote:
> > The best way to convince me is through valid examples.  
> 
> It is also easier to be convinced when you try to understand and ask
> for clarifications instead of just rejecting without thinking :)

The problem with this entire proposal is that it's still in "well I
can't think of how it could possibly go wrong" territory. We need a
formal proof that it's sound. History has shown that if something can
be abused by Gentoo developers, it will be abused...

-- 
Ciaran McCreesh

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

[Alexis Ballier]

On Thu, 15 Jun 2017 17:59:13 +0200
Michał Górny  wrote:

> On śro, 2017-06-14 at 16:09 +0200, Alexis Ballier wrote:
> > On Wed, 14 Jun 2017 15:57:38 +0200
> > Michał Górny  wrote:
> > [...]  
> > > > [...]
> > > > > > > > > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse  
> > > > > > > > >   
> > > > > > > > 
> > > > > > > > I really don't like the reordering thing. Even the
> > > > > > > > restricted syntax does not fix the issue with '^^ ( a b
> > > > > > > > ) b? ( a )' already mentioned here. It'd be much better
> > > > > > > > and simpler for the spec just to assign a fixed value
> > > > > > > > and use the solving rules with those.
> > > > > > > 
> > > > > > > You're not going to convince me by providing examples
> > > > > > > that are utterly broken by design and
> > > > > > > meaningless ;-).  
> > > > > > 
> > > > > > Well... if it's so obvious that the example is broken by
> > > > > > design that you don't even bother to explain why, I assume
> > > > > > you have an algorithm for that. Where is the code ? What
> > > > > > are the numbers ? How many ebuilds might fail after
> > > > > > reordering ? How can this be improved ?  
> > > > > 
> > > > > Are you arguing for the sake of arguing here? I just presumed
> > > > > that this example is so obviously broken there is no point
> > > > > wasting any more time on it. The code of nsolve clearly
> > > > > detects that, so I don't really understand what you're trying
> > > > > to prove here.
> > > > 
> > > > Those are real questions. You should take breath, think a bit
> > > > about it, and try to run the 2 possible orderings of the ^^
> > > > through nsolve or even solve.py. They both are very happy (and
> > > > are right to be) with the above ordering. You might want to
> > > > think a bit more about what is the relation between this broken
> > > > 10 chars example and the 10 lines python targets one below.
> > > > 
> > > > You should also realize that all the above questions have
> > > > already been answered in length if you do as I suggest.
> > > 
> > > No. I have already spent too much time on this. We're already long
> > > past all useful use cases, and now I feel like you're going to
> > > argue to death just to find a perfect algorithm that supports
> > > every absurd construct anyone can even write, if only to figure
> > > out the construct is completely useless.  
> > 
> > I'm not going to argue to death. It's already proven reordering is
> > broken.
> >   
> > > If you want to play with it more, then please by all means do
> > > so.  
> > 
> > There is nothing to do for reordering. It's broken by design.
> >   
> > > However, do not expect me to waste any more of my time on it. I've
> > > done my part, the code works for all reasonable use cases and
> > > solves all the problems I needed solving. If you want more, then
> > > it's your job to do it and solve the resulting issues.  
> > 
> > Like... writing code handling all the cases and describing how it
> > works ? We're past that. The only thing we're not past is that you
> > fail to understand it and attempt to block it.
> >   
> 
> Then please provide a single valid example that:

app-text/wklej-0.2.1-r1 ^^ ( python_single_target_pypy
python_single_target_pypy3 python_single_target_python2_7
python_single_target_python3_4 python_single_target_python3_5
python_single_target_python3_6 ) python_single_target_pypy?
( python_targets_pypy ) python_single_target_pypy3?
( python_targets_pypy3 ) python_single_target_python2_7?
( python_targets_python2_7 ) python_single_target_python3_4?
( python_targets_python3_4 ) python_single_target_python3_5?
( python_targets_python3_5 ) python_single_target_python3_6?
( python_targets_python3_6 ) vim? ( ^^ ( python_single_target_python2_7
) )


Simplified as:
^^ ( a b ) c? ( b )

(see the pattern now ? :) )

> a. is completely 'correct' (that is, provides a valid, predictable
> and acceptable solution) with the default ordering O_a,

c? ( b ) ^^ ( b a )


> b. is not 'correct' with at least one reordering O_b (assuming only
> ||, ^^, ?? is subject to reordering),

c? ( b ) ^^ ( a b )

> 
> c. nsolve reports O_a as all good, and O_b as not good.

I'll let you run this. It does.

> The best way to convince me is through valid examples.


It is also easier to be convinced when you try to understand and ask
for clarifications instead of just rejecting without thinking :)

Alexis.

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

[Michał Górny]

On śro, 2017-06-14 at 16:09 +0200, Alexis Ballier wrote:
> On Wed, 14 Jun 2017 15:57:38 +0200
> Michał Górny  wrote:
> [...]
> > > [...]  
> > > > > > > > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse  
> > > > > > > 
> > > > > > > I really don't like the reordering thing. Even the
> > > > > > > restricted syntax does not fix the issue with '^^ ( a b )
> > > > > > > b? ( a )' already mentioned here. It'd be much better and
> > > > > > > simpler for the spec just to assign a fixed value and use
> > > > > > > the solving rules with those.  
> > > > > > 
> > > > > > You're not going to convince me by providing examples that are
> > > > > > utterly broken by design and meaningless ;-).
> > > > > 
> > > > > Well... if it's so obvious that the example is broken by design
> > > > > that you don't even bother to explain why, I assume you have an
> > > > > algorithm for that. Where is the code ? What are the numbers ?
> > > > > How many ebuilds might fail after reordering ? How can this be
> > > > > improved ?
> > > > 
> > > > Are you arguing for the sake of arguing here? I just presumed that
> > > > this example is so obviously broken there is no point wasting any
> > > > more time on it. The code of nsolve clearly detects that, so I
> > > > don't really understand what you're trying to prove here.  
> > > 
> > > Those are real questions. You should take breath, think a bit about
> > > it, and try to run the 2 possible orderings of the ^^ through
> > > nsolve or even solve.py. They both are very happy (and are right to
> > > be) with the above ordering. You might want to think a bit more
> > > about what is the relation between this broken 10 chars example and
> > > the 10 lines python targets one below.
> > > 
> > > You should also realize that all the above questions have already
> > > been answered in length if you do as I suggest.  
> > 
> > No. I have already spent too much time on this. We're already long
> > past all useful use cases, and now I feel like you're going to argue
> > to death just to find a perfect algorithm that supports every absurd
> > construct anyone can even write, if only to figure out the construct
> > is completely useless.
> 
> I'm not going to argue to death. It's already proven reordering is
> broken.
> 
> > If you want to play with it more, then please by all means do so.
> 
> There is nothing to do for reordering. It's broken by design.
> 
> > However, do not expect me to waste any more of my time on it. I've
> > done my part, the code works for all reasonable use cases and solves
> > all the problems I needed solving. If you want more, then it's your
> > job to do it and solve the resulting issues.
> 
> Like... writing code handling all the cases and describing how it
> works ? We're past that. The only thing we're not past is that you fail
> to understand it and attempt to block it.
> 

Then please provide a single valid example that:

a. is completely 'correct' (that is, provides a valid, predictable
and acceptable solution) with the default ordering O_a,

b. is not 'correct' with at least one reordering O_b (assuming only ||,
^^, ?? is subject to reordering),

c. nsolve reports O_a as all good, and O_b as not good.

The best way to convince me is through valid examples.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Wed, 14 Jun 2017 15:57:38 +0200
Michał Górny  wrote:

> No. I have already spent too much time on this. We're already long
> past all useful use cases

Also, if you feel that way, then please stop working on this entirely
for now. You're not bringing any good to anyone, yourself first, by
pushing yourself when you don't have the will to reach a proper
solution. You'll only end up with a solution having the same kind of
problems you're trying to fix with required use.

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

[Alexis Ballier]

On Wed, 14 Jun 2017 15:57:38 +0200
Michał Górny  wrote:
[...]
> > [...]  
> > > > > > > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse  
> > > > > > 
> > > > > > I really don't like the reordering thing. Even the
> > > > > > restricted syntax does not fix the issue with '^^ ( a b )
> > > > > > b? ( a )' already mentioned here. It'd be much better and
> > > > > > simpler for the spec just to assign a fixed value and use
> > > > > > the solving rules with those.  
> > > > > 
> > > > > You're not going to convince me by providing examples that are
> > > > > utterly broken by design and meaningless ;-).
> > > > 
> > > > Well... if it's so obvious that the example is broken by design
> > > > that you don't even bother to explain why, I assume you have an
> > > > algorithm for that. Where is the code ? What are the numbers ?
> > > > How many ebuilds might fail after reordering ? How can this be
> > > > improved ?
> > > 
> > > Are you arguing for the sake of arguing here? I just presumed that
> > > this example is so obviously broken there is no point wasting any
> > > more time on it. The code of nsolve clearly detects that, so I
> > > don't really understand what you're trying to prove here.  
> > 
> > Those are real questions. You should take breath, think a bit about
> > it, and try to run the 2 possible orderings of the ^^ through
> > nsolve or even solve.py. They both are very happy (and are right to
> > be) with the above ordering. You might want to think a bit more
> > about what is the relation between this broken 10 chars example and
> > the 10 lines python targets one below.
> > 
> > You should also realize that all the above questions have already
> > been answered in length if you do as I suggest.  
> 
> No. I have already spent too much time on this. We're already long
> past all useful use cases, and now I feel like you're going to argue
> to death just to find a perfect algorithm that supports every absurd
> construct anyone can even write, if only to figure out the construct
> is completely useless.

I'm not going to argue to death. It's already proven reordering is
broken.

> If you want to play with it more, then please by all means do so.

There is nothing to do for reordering. It's broken by design.

> However, do not expect me to waste any more of my time on it. I've
> done my part, the code works for all reasonable use cases and solves
> all the problems I needed solving. If you want more, then it's your
> job to do it and solve the resulting issues.

Like... writing code handling all the cases and describing how it
works ? We're past that. The only thing we're not past is that you fail
to understand it and attempt to block it.


Alexis.

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

[Michał Górny]

On śro, 2017-06-14 at 15:16 +0200, Alexis Ballier wrote:
> On Wed, 14 Jun 2017 14:24:48 +0200
> Michał Górny  wrote:
> 
> > On śro, 2017-06-14 at 11:06 +0200, Alexis Ballier wrote:
> > > On Wed, 14 Jun 2017 00:13:42 +0200
> > > Michał Górny  wrote:
> > >   
> > > > On wto, 2017-06-13 at 12:27 +0200, Alexis Ballier wrote:  
> > > > > On Mon, 12 Jun 2017 21:17:16 +0200
> > > > > Michał Górny  wrote:
> > > > > 
> > > > > > I've actually started typing the initial specification
> > > > > > yesterday [1]. As you can see, banning the extra constraints
> > > > > > has made the algorithms much simpler. In particular:
> > > > > > 
> > > > > > 1. You do not have to define 'falsify' for anything other than
> > > > > > pure flags -- which makes it easy to inline it.
> > > > > > 
> > > > > > 2. ||, ??, ^^ groups are only flat lists of flags -- which
> > > > > > makes reordering and processing them trivial.
> > > > > > 
> > > > > > 3. The algorithm is recursive only on USE-conditional groups.
> > > > > > This makes it trivial to make it iterative. Optimizations
> > > > > > become trivially possible.
> > > > > 
> > > > > 
> > > > > While you're right in one sense, you're mixing two different
> > > > > things here. What you wrote *is* recursive. It does not recurse
> > > > > just because you're assuming a restricted syntax. You're only
> > > > > saving two things: you don't need to define how to enforce to
> > > > > false (that is 3 lines not 3 pages :=) ) and you're avoiding
> > > > > the nested use conditionals that are already ill defined per
> > > > > the current spec (foo? bar is equivalent to && ( foo bar ) when
> > > > > nested) which I believe is already another problem.
> > > > > 
> > > > > Then, remember how I wanted to be much more drastic than you in
> > > > > the beginning by killing all ||,&&,^^ etc. and keep only use
> > > > > conditionals in REQUIRED_USE ?  Well, that's where the
> > > > > complexity comes. The whole deal then is to define rewriting
> > > > > rules for the AST so that the algorithm you describe executes
> > > > > the exact same instructions but the new AST only has use
> > > > > conditionals. This is more like writing a compiler for the
> > > > > spec, so this does not belong to the spec and there is no issue
> > > > > here.
> > > > 
> > > > I'm looking for a compromise here. Killing those groups
> > > > completely is going to make things harder for users. Keeping them
> > > > with functionality limited to what's used in ~99.9% ebuilds
> > > > (based on your numbers) is IMO a better choice.  
> > > 
> > > I already said I see the limited syntax as a good thing because it
> > > forces devs to write constraints that have a natural interpretation
> > > in how it is solved. However, you can't limit the syntax without a
> > > new EAPI, and more importantly, properly solving does not even
> > > require limiting the syntax.  
> > 
> > Actually, you can, via a Gentoo policy. Since solving is not required
> > by the PMS, there is no rule saying it has to work for every
> > constraint allowed by the PMS.
> 
> Indeed. But you're trying to make rules that it has *not* to work for
> some of them for reasons that look more like laziness in trying to
> understand the problem than anything else.

Wrong. I'm making a rule that it does not have to be implemented for
this corner case.

> > > > > [BTW: checking the rewrite rules behave properly is what I
> > > > > meant by rebasing solve() on top of it and being happy with
> > > > > it]
> > > > 
> > > > Could you reiterate the current solving rules (trueify/falsify)?
> > > > Are they equal to the ones you listed last, or does the current
> > > > implementation change anything?  
> > > 
> > > Let's recap a bit. nsolve() is poorly named and does not solve
> > > anything. It translates to implications and checks whether the
> > > implications solver will always provide a valid result in one pass.
> > > So, if you only care about solving rules, read your spec man. For
> > > the more general case it should behave like those trueify/falsify
> > > with the change that nested implications are interpreted as && (so
> > > no more !(a -> b) crap to worry about).  
> > 
> > How are && ( a b... ) falsified now? Leftmost only?
> 
> $ python3 to_impl.py '?? ( a ( b c ) )'
> Normalized: [|| [!b, !c, !a]]
> List of implications:
>   [[c, a]? => !b]
> 
> Sounds like it. This is the only "stable" way anyway.

Changed that already.

> > > If you take solve() as an implementation of your spec, you have:
> > > solve(x) <=> solve(to_impl.convert_to_implications(x)) when solve(x)
> > > is defined; with the added benefit that
> > > 'solve(to_impl.convert_to_implications(x))' is defined and should
> > > provide proper results on the whole REQUIRED_USE syntax as currently
> > > defined (granted that nsolve(x) does not report anything wrong).  
> > 
> > The point is, solve() is supposed to work without any 

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

[Alexis Ballier]

On Wed, 14 Jun 2017 14:24:48 +0200
Michał Górny  wrote:

> On śro, 2017-06-14 at 11:06 +0200, Alexis Ballier wrote:
> > On Wed, 14 Jun 2017 00:13:42 +0200
> > Michał Górny  wrote:
> >   
> > > On wto, 2017-06-13 at 12:27 +0200, Alexis Ballier wrote:  
> > > > On Mon, 12 Jun 2017 21:17:16 +0200
> > > > Michał Górny  wrote:
> > > > 
> > > > > I've actually started typing the initial specification
> > > > > yesterday [1]. As you can see, banning the extra constraints
> > > > > has made the algorithms much simpler. In particular:
> > > > > 
> > > > > 1. You do not have to define 'falsify' for anything other than
> > > > > pure flags -- which makes it easy to inline it.
> > > > > 
> > > > > 2. ||, ??, ^^ groups are only flat lists of flags -- which
> > > > > makes reordering and processing them trivial.
> > > > > 
> > > > > 3. The algorithm is recursive only on USE-conditional groups.
> > > > > This makes it trivial to make it iterative. Optimizations
> > > > > become trivially possible.
> > > > 
> > > > 
> > > > While you're right in one sense, you're mixing two different
> > > > things here. What you wrote *is* recursive. It does not recurse
> > > > just because you're assuming a restricted syntax. You're only
> > > > saving two things: you don't need to define how to enforce to
> > > > false (that is 3 lines not 3 pages :=) ) and you're avoiding
> > > > the nested use conditionals that are already ill defined per
> > > > the current spec (foo? bar is equivalent to && ( foo bar ) when
> > > > nested) which I believe is already another problem.
> > > > 
> > > > Then, remember how I wanted to be much more drastic than you in
> > > > the beginning by killing all ||,&&,^^ etc. and keep only use
> > > > conditionals in REQUIRED_USE ?  Well, that's where the
> > > > complexity comes. The whole deal then is to define rewriting
> > > > rules for the AST so that the algorithm you describe executes
> > > > the exact same instructions but the new AST only has use
> > > > conditionals. This is more like writing a compiler for the
> > > > spec, so this does not belong to the spec and there is no issue
> > > > here.
> > > 
> > > I'm looking for a compromise here. Killing those groups
> > > completely is going to make things harder for users. Keeping them
> > > with functionality limited to what's used in ~99.9% ebuilds
> > > (based on your numbers) is IMO a better choice.  
> > 
> > I already said I see the limited syntax as a good thing because it
> > forces devs to write constraints that have a natural interpretation
> > in how it is solved. However, you can't limit the syntax without a
> > new EAPI, and more importantly, properly solving does not even
> > require limiting the syntax.  
> 
> Actually, you can, via a Gentoo policy. Since solving is not required
> by the PMS, there is no rule saying it has to work for every
> constraint allowed by the PMS.

Indeed. But you're trying to make rules that it has *not* to work for
some of them for reasons that look more like laziness in trying to
understand the problem than anything else.

> Much like, you can't force a particular ordering or forbid circular
> constraints without a new EAPI. Yet you do it because it gives
> a practical improvement.

I don't see this being enforced by a new EAPI. It's more a matter of QA
tools like repoman. The main difference is that there are real reasons
for forbidding circular constraints: For true circular ones, no solver
will ever be able to solve it...

[...]
> >   
> > > > [BTW: checking the rewrite rules behave properly is what I
> > > > meant by rebasing solve() on top of it and being happy with
> > > > it]
> > > 
> > > Could you reiterate the current solving rules (trueify/falsify)?
> > > Are they equal to the ones you listed last, or does the current
> > > implementation change anything?  
> > 
> > Let's recap a bit. nsolve() is poorly named and does not solve
> > anything. It translates to implications and checks whether the
> > implications solver will always provide a valid result in one pass.
> > So, if you only care about solving rules, read your spec man. For
> > the more general case it should behave like those trueify/falsify
> > with the change that nested implications are interpreted as && (so
> > no more !(a -> b) crap to worry about).  
> 
> How are && ( a b... ) falsified now? Leftmost only?

$ python3 to_impl.py '?? ( a ( b c ) )'
Normalized: [|| [!b, !c, !a]]
List of implications:
  [[c, a]? => !b]

Sounds like it. This is the only "stable" way anyway.


> > If you take solve() as an implementation of your spec, you have:
> > solve(x) <=> solve(to_impl.convert_to_implications(x)) when solve(x)
> > is defined; with the added benefit that
> > 'solve(to_impl.convert_to_implications(x))' is defined and should
> > provide proper results on the whole REQUIRED_USE syntax as currently
> > defined (granted that nsolve(x) does not report anything wrong).  

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

[Michał Górny]

On śro, 2017-06-14 at 11:06 +0200, Alexis Ballier wrote:
> On Wed, 14 Jun 2017 00:13:42 +0200
> Michał Górny  wrote:
> 
> > On wto, 2017-06-13 at 12:27 +0200, Alexis Ballier wrote:
> > > On Mon, 12 Jun 2017 21:17:16 +0200
> > > Michał Górny  wrote:
> > >   
> > > > I've actually started typing the initial specification yesterday
> > > > [1]. As you can see, banning the extra constraints has made the
> > > > algorithms much simpler. In particular:
> > > > 
> > > > 1. You do not have to define 'falsify' for anything other than
> > > > pure flags -- which makes it easy to inline it.
> > > > 
> > > > 2. ||, ??, ^^ groups are only flat lists of flags -- which makes
> > > > reordering and processing them trivial.
> > > > 
> > > > 3. The algorithm is recursive only on USE-conditional groups. This
> > > > makes it trivial to make it iterative. Optimizations become
> > > > trivially possible.  
> > > 
> > > 
> > > While you're right in one sense, you're mixing two different things
> > > here. What you wrote *is* recursive. It does not recurse just
> > > because you're assuming a restricted syntax. You're only saving two
> > > things: you don't need to define how to enforce to false (that is 3
> > > lines not 3 pages :=) ) and you're avoiding the nested use
> > > conditionals that are already ill defined per the current spec
> > > (foo? bar is equivalent to && ( foo bar ) when nested) which I
> > > believe is already another problem.
> > > 
> > > Then, remember how I wanted to be much more drastic than you in the
> > > beginning by killing all ||,&&,^^ etc. and keep only use
> > > conditionals in REQUIRED_USE ?  Well, that's where the complexity
> > > comes. The whole deal then is to define rewriting rules for the AST
> > > so that the algorithm you describe executes the exact same
> > > instructions but the new AST only has use conditionals. This is
> > > more like writing a compiler for the spec, so this does not belong
> > > to the spec and there is no issue here.  
> > 
> > I'm looking for a compromise here. Killing those groups completely is
> > going to make things harder for users. Keeping them with functionality
> > limited to what's used in ~99.9% ebuilds (based on your numbers) is
> > IMO a better choice.
> 
> I already said I see the limited syntax as a good thing because it
> forces devs to write constraints that have a natural interpretation in
> how it is solved. However, you can't limit the syntax without a new
> EAPI, and more importantly, properly solving does not even require
> limiting the syntax.

Actually, you can, via a Gentoo policy. Since solving is not required by
the PMS, there is no rule saying it has to work for every constraint
allowed by the PMS.

Much like, you can't force a particular ordering or forbid circular
constraints without a new EAPI. Yet you do it because it gives
a practical improvement.

> BTW, I don't know how you get that info from my data because I never
> voluntarily checked for a restricted syntax :)

I took the totals from your data, and subtracted the counts for invalid
constraints from mine ;-).

> 
> > > [BTW: checking the rewrite rules behave properly is what I meant by
> > > rebasing solve() on top of it and being happy with it]  
> > 
> > Could you reiterate the current solving rules (trueify/falsify)? Are
> > they equal to the ones you listed last, or does the current
> > implementation change anything?
> 
> Let's recap a bit. nsolve() is poorly named and does not solve
> anything. It translates to implications and checks whether the
> implications solver will always provide a valid result in one pass.
> So, if you only care about solving rules, read your spec man. For the
> more general case it should behave like those trueify/falsify with
> the change that nested implications are interpreted as && (so no
> more !(a -> b) crap to worry about).

How are && ( a b... ) falsified now? Leftmost only?

> If you take solve() as an implementation of your spec, you have:
> solve(x) <=> solve(to_impl.convert_to_implications(x)) when solve(x)
> is defined; with the added benefit that
> 'solve(to_impl.convert_to_implications(x))' is defined and should
> provide proper results on the whole REQUIRED_USE syntax as currently
> defined (granted that nsolve(x) does not report anything wrong).

The point is, solve() is supposed to work without any additional
transformations. So the rules need to be consistent. As a matter of
fact, I want to add a little extra test to solve.py that verifies that
the result without and with transformation is the same.

> > > > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse  
> > > 
> > > I really don't like the reordering thing. Even the restricted
> > > syntax does not fix the issue with '^^ ( a b ) b? ( a )' already
> > > mentioned here. It'd be much better and simpler for the spec just to
> > > assign a fixed value and use the solving rules with those.  
> > 
> > You're not going to convince me 

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

[Alexis Ballier]

On Wed, 14 Jun 2017 00:13:42 +0200
Michał Górny  wrote:

> On wto, 2017-06-13 at 12:27 +0200, Alexis Ballier wrote:
> > On Mon, 12 Jun 2017 21:17:16 +0200
> > Michał Górny  wrote:
> >   
> > > I've actually started typing the initial specification yesterday
> > > [1]. As you can see, banning the extra constraints has made the
> > > algorithms much simpler. In particular:
> > > 
> > > 1. You do not have to define 'falsify' for anything other than
> > > pure flags -- which makes it easy to inline it.
> > > 
> > > 2. ||, ??, ^^ groups are only flat lists of flags -- which makes
> > > reordering and processing them trivial.
> > > 
> > > 3. The algorithm is recursive only on USE-conditional groups. This
> > > makes it trivial to make it iterative. Optimizations become
> > > trivially possible.  
> > 
> > 
> > While you're right in one sense, you're mixing two different things
> > here. What you wrote *is* recursive. It does not recurse just
> > because you're assuming a restricted syntax. You're only saving two
> > things: you don't need to define how to enforce to false (that is 3
> > lines not 3 pages :=) ) and you're avoiding the nested use
> > conditionals that are already ill defined per the current spec
> > (foo? bar is equivalent to && ( foo bar ) when nested) which I
> > believe is already another problem.
> > 
> > Then, remember how I wanted to be much more drastic than you in the
> > beginning by killing all ||,&&,^^ etc. and keep only use
> > conditionals in REQUIRED_USE ?  Well, that's where the complexity
> > comes. The whole deal then is to define rewriting rules for the AST
> > so that the algorithm you describe executes the exact same
> > instructions but the new AST only has use conditionals. This is
> > more like writing a compiler for the spec, so this does not belong
> > to the spec and there is no issue here.  
> 
> I'm looking for a compromise here. Killing those groups completely is
> going to make things harder for users. Keeping them with functionality
> limited to what's used in ~99.9% ebuilds (based on your numbers) is
> IMO a better choice.

I already said I see the limited syntax as a good thing because it
forces devs to write constraints that have a natural interpretation in
how it is solved. However, you can't limit the syntax without a new
EAPI, and more importantly, properly solving does not even require
limiting the syntax.

BTW, I don't know how you get that info from my data because I never
voluntarily checked for a restricted syntax :)

> > [BTW: checking the rewrite rules behave properly is what I meant by
> > rebasing solve() on top of it and being happy with it]  
> 
> Could you reiterate the current solving rules (trueify/falsify)? Are
> they equal to the ones you listed last, or does the current
> implementation change anything?

Let's recap a bit. nsolve() is poorly named and does not solve
anything. It translates to implications and checks whether the
implications solver will always provide a valid result in one pass.
So, if you only care about solving rules, read your spec man. For the
more general case it should behave like those trueify/falsify with
the change that nested implications are interpreted as && (so no
more !(a -> b) crap to worry about).

If you take solve() as an implementation of your spec, you have:
solve(x) <=> solve(to_impl.convert_to_implications(x)) when solve(x)
is defined; with the added benefit that
'solve(to_impl.convert_to_implications(x))' is defined and should
provide proper results on the whole REQUIRED_USE syntax as currently
defined (granted that nsolve(x) does not report anything wrong).

> > > Nevertheless, feel free to play with the full implementation. If
> > > you're interested, you can play with the complex cases more. In
> > > particular, I'm wondering whether nsolve will actually consider
> > > most of them solvable.
> > > 
> > > As for the results, I think it is the point where we start
> > > preparing pull requests with REQUIRED_USE changes to see whether
> > > the developers agree with such changes.  
> > 
> > If by that you also include code cleanup and writing tests then
> > yes :)  
> 
> I'm not sure if we're talking about the same thing. I'm talking about
> filing pull requests against ebuilds whose REQUIRED_USE is rejected by
> nsolve. I think it'd serve as a reasonable field test for whether
> developers agree with the imposed restrictions.

I was talking about PRs against portage & repoman.

> > > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse  
> > 
> > I really don't like the reordering thing. Even the restricted
> > syntax does not fix the issue with '^^ ( a b ) b? ( a )' already
> > mentioned here. It'd be much better and simpler for the spec just to
> > assign a fixed value and use the solving rules with those.  
> 
> You're not going to convince me by providing examples that are utterly
> broken by design and meaningless ;-).

Well... if it's so obvious that the 

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

[Michał Górny]

On wto, 2017-06-13 at 12:27 +0200, Alexis Ballier wrote:
> On Mon, 12 Jun 2017 21:17:16 +0200
> Michał Górny  wrote:
> 
> > I've actually started typing the initial specification yesterday [1].
> > As you can see, banning the extra constraints has made the algorithms
> > much simpler. In particular:
> > 
> > 1. You do not have to define 'falsify' for anything other than pure
> > flags -- which makes it easy to inline it.
> > 
> > 2. ||, ??, ^^ groups are only flat lists of flags -- which makes
> > reordering and processing them trivial.
> > 
> > 3. The algorithm is recursive only on USE-conditional groups. This
> > makes it trivial to make it iterative. Optimizations become trivially
> > possible.
> 
> 
> While you're right in one sense, you're mixing two different things
> here. What you wrote *is* recursive. It does not recurse just because
> you're assuming a restricted syntax. You're only saving two things:
> you don't need to define how to enforce to false (that is 3 lines not 3
> pages :=) ) and you're avoiding the nested use conditionals that are
> already ill defined per the current spec (foo? bar is equivalent to
> && ( foo bar ) when nested) which I believe is already another problem.
> 
> Then, remember how I wanted to be much more drastic than you in the
> beginning by killing all ||,&&,^^ etc. and keep only use
> conditionals in REQUIRED_USE ?  Well, that's where the complexity comes.
> The whole deal then is to define rewriting rules for the AST so that
> the algorithm you describe executes the exact same instructions but the
> new AST only has use conditionals. This is more like writing a compiler
> for the spec, so this does not belong to the spec and there is no
> issue here.

I'm looking for a compromise here. Killing those groups completely is
going to make things harder for users. Keeping them with functionality
limited to what's used in ~99.9% ebuilds (based on your numbers) is IMO
a better choice.

> [BTW: checking the rewrite rules behave properly is what I meant by
> rebasing solve() on top of it and being happy with it]

Could you reiterate the current solving rules (trueify/falsify)? Are
they equal to the ones you listed last, or does the current
implementation change anything?

> > Nevertheless, feel free to play with the full implementation. If
> > you're interested, you can play with the complex cases more. In
> > particular, I'm wondering whether nsolve will actually consider most
> > of them solvable.
> > 
> > As for the results, I think it is the point where we start preparing
> > pull requests with REQUIRED_USE changes to see whether the developers
> > agree with such changes.
> 
> If by that you also include code cleanup and writing tests then yes :)

I'm not sure if we're talking about the same thing. I'm talking about
filing pull requests against ebuilds whose REQUIRED_USE is rejected by
nsolve. I think it'd serve as a reasonable field test for whether
developers agree with the imposed restrictions.

> > [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse
> 
> I really don't like the reordering thing. Even the restricted
> syntax does not fix the issue with '^^ ( a b ) b? ( a )' already
> mentioned here. It'd be much better and simpler for the spec just to
> assign a fixed value and use the solving rules with those.

You're not going to convince me by providing examples that are utterly
broken by design and meaningless ;-).

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Mon, 12 Jun 2017 21:17:16 +0200
Michał Górny  wrote:

> On pon, 2017-06-12 at 11:08 +0200, Alexis Ballier wrote:
> > On Sun, 11 Jun 2017 18:05:18 +0200
> > Alexis Ballier  wrote:
> >   
> > > I think this handles all the cases. I'll try to update the repo
> > > with that algo.  
> > 
> > I've updated my fork. It'd be good to merge it and rebase solve() on
> > top of the output of to_impl.convert_to_implications if you're happy
> > with it.
> > 
> > $ time python3 classify.py requsel 
> > Stats:
> > Parse error: 0
> > Good: 8334
> > Need topo sort: 152
> > Cyclic: 43
> > 
> > real0m1.874s
> > user0m1.869s
> > sys 0m0.005s
> > 
> > 
> > 
> > It works better, no more parse error, and only 43 problematic
> > cases.  
> 
> Thanks for doing it. It's certainly an interesting case study. I've
> merged it and pushed the result.
> 
> However, I personally think it's only going to work against your case.

What do you mean here ?

> You can clearly see now how complex the code has become. Even
> in the pseudo-ocaml you presented it already is complex. Now imagine
> having to retype it in cleartext suitable for the PMS.

The code needs cleanup and probably some refactoring. I think it can be
made much simpler.

> I've actually started typing the initial specification yesterday [1].
> As you can see, banning the extra constraints has made the algorithms
> much simpler. In particular:
> 
> 1. You do not have to define 'falsify' for anything other than pure
> flags -- which makes it easy to inline it.
> 
> 2. ||, ??, ^^ groups are only flat lists of flags -- which makes
> reordering and processing them trivial.
> 
> 3. The algorithm is recursive only on USE-conditional groups. This
> makes it trivial to make it iterative. Optimizations become trivially
> possible.


While you're right in one sense, you're mixing two different things
here. What you wrote *is* recursive. It does not recurse just because
you're assuming a restricted syntax. You're only saving two things:
you don't need to define how to enforce to false (that is 3 lines not 3
pages :=) ) and you're avoiding the nested use conditionals that are
already ill defined per the current spec (foo? bar is equivalent to
&& ( foo bar ) when nested) which I believe is already another problem.

Then, remember how I wanted to be much more drastic than you in the
beginning by killing all ||,&&,^^ etc. and keep only use
conditionals in REQUIRED_USE ?  Well, that's where the complexity comes.
The whole deal then is to define rewriting rules for the AST so that
the algorithm you describe executes the exact same instructions but the
new AST only has use conditionals. This is more like writing a compiler
for the spec, so this does not belong to the spec and there is no
issue here.

[BTW: checking the rewrite rules behave properly is what I meant by
rebasing solve() on top of it and being happy with it]



> Nevertheless, feel free to play with the full implementation. If
> you're interested, you can play with the complex cases more. In
> particular, I'm wondering whether nsolve will actually consider most
> of them solvable.
> 
> As for the results, I think it is the point where we start preparing
> pull requests with REQUIRED_USE changes to see whether the developers
> agree with such changes.

If by that you also include code cleanup and writing tests then yes :)

> [1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse

I really don't like the reordering thing. Even the restricted
syntax does not fix the issue with '^^ ( a b ) b? ( a )' already
mentioned here. It'd be much better and simpler for the spec just to
assign a fixed value and use the solving rules with those.


Alexis.

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

[Michał Górny]

On pon, 2017-06-12 at 11:08 +0200, Alexis Ballier wrote:
> On Sun, 11 Jun 2017 18:05:18 +0200
> Alexis Ballier  wrote:
> 
> > I think this handles all the cases. I'll try to update the repo with
> > that algo.
> 
> I've updated my fork. It'd be good to merge it and rebase solve() on
> top of the output of to_impl.convert_to_implications if you're happy
> with it.
> 
> $ time python3 classify.py requsel 
> Stats:
>   Parse error: 0
>   Good: 8334
>   Need topo sort: 152
>   Cyclic: 43
> 
> real  0m1.874s
> user  0m1.869s
> sys   0m0.005s
> 
> 
> 
> It works better, no more parse error, and only 43 problematic cases.

Thanks for doing it. It's certainly an interesting case study. I've
merged it and pushed the result.

However, I personally think it's only going to work against your case.
You can clearly see now how complex the code has become. Even
in the pseudo-ocaml you presented it already is complex. Now imagine
having to retype it in cleartext suitable for the PMS.

I've actually started typing the initial specification yesterday [1].
As you can see, banning the extra constraints has made the algorithms
much simpler. In particular:

1. You do not have to define 'falsify' for anything other than pure
flags -- which makes it easy to inline it.

2. ||, ??, ^^ groups are only flat lists of flags -- which makes
reordering and processing them trivial.

3. The algorithm is recursive only on USE-conditional groups. This makes
it trivial to make it iterative. Optimizations become trivially
possible.

Nevertheless, feel free to play with the full implementation. If you're
interested, you can play with the complex cases more. In particular, I'm
wondering whether nsolve will actually consider most of them solvable.

As for the results, I think it is the point where we start preparing
pull requests with REQUIRED_USE changes to see whether the developers
agree with such changes.

[1]:https://wiki.gentoo.org/wiki/User:MGorny/GLEP:ReqUse

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Sun, 11 Jun 2017 18:05:18 +0200
Alexis Ballier  wrote:

> I think this handles all the cases. I'll try to update the repo with
> that algo.

I've updated my fork. It'd be good to merge it and rebase solve() on
top of the output of to_impl.convert_to_implications if you're happy
with it.

$ time python3 classify.py requsel 
Stats:
Parse error: 0
Good: 8334
Need topo sort: 152
Cyclic: 43

real0m1.874s
user0m1.869s
sys 0m0.005s



It works better, no more parse error, and only 43 problematic cases.

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

[Alexis Ballier]

On Fri, 09 Jun 2017 18:21:50 +0200
Michał Górny  wrote:

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

The semi-hidden goal here for me is to have purely ast rewriting rules
giving a list of implications. This makes the solver trivial as those
are read as "if condition then constraint" and can be used as input for
the checker. Failing that, this would need to be done on the checker
side anyway and then we might run into problems like the checker not
really checking reality since the solver behaves a little bit
differently.

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

This should be equivalent: masked flags will be toggled as last resort
and fail; eliminated flags will not be toggled at all and fail if
having them as immutable causes a contradiction

> 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 in use.force. This gets reordered to:
> 
>   ?? ( b c a )
> 
> The order between b 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.

Considering that code should ideally be checked, that'd be '?? ( a true
true )' reducing to 'false' and a repoman error.


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


Except feeding the n! possible reorderings to nsolve() and checking them
all I don't see many other possibilities.

We could think about a transformation that would be order agnostic,
like '|| ( a b c )' giving the same output as '|| ( b c a )' but then
this would not express any preference anymore. Remember: The whole
point of the solver is to break the symmetry of SAT formulas so that
there is a natural way to solve them instead of just "figure out some
useflags that make it work". In other words, order does actually
matter a lot, otherwise you fall into the "solve SAT" trap again.


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

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

[Michał Górny]

(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 in use.force. This gets reordered to:

  ?? ( b c a )

The order between b 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 

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

[Alexis Ballier]

On Fri, 09 Jun 2017 14:54:07 +0200
Michał Górny  wrote:

> On pią, 2017-06-09 at 13:41 +0200, Alexis Ballier wrote:
> > On Fri, 09 Jun 2017 11:19:20 +0200
> > Michał Górny  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  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.


Yep, makes sense.

It makes it harder to guess though: "a? ( b ) !b? ( a )" will
enable both a and b if USE=-*. This is not obvious to me from a single
read of the constraint. I need to tell myself "Oh, I've now enabled 'a'
and I need to recheck the first clause.".

I was thinking more from a spec perspective where I would definitely
not want to mandate PM to do fixpoint(solve) or having to detect a
cycle before failing. Also, I believe that forcing a single pass solver
will help in ensuring that the solver solves it the way the developer
writing the constraint meant it.


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


Yeah, that's basically what I inferred from trying to figure out the
meaning out of it later on.

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

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

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

[Michał Górny]

On pią, 2017-06-09 at 14:35 +0200, Jason A. Donenfeld wrote:
> On Mon, May 29, 2017 at 5:33 PM, Michał Górny  wrote:
> > 
> > Secondly, it might be reasonable to provide configurable priorities for
> > solving multi-flag constraints. For example, we could use rightmost-
> > preferred logic for package.use, e.g.:
> > 
> >   */*  PROVIDER_SSL: openssl gnutls
> >   dev-util/foo PROVIDER_SSL: polarssl
> > 
> > which would mean that for all packages, gnutls is preferred over openssl
> > (i.e. if ?? or ^^ applies, openssl will be disabled and gnutls will be
> > used), and polarssl is additionally preferred over everything else for
> > dev-util/foo.
> 
> Please, leftmost instead of rightmost?

How about the following:

  dev-util/xxx foo
  dev-util/xxx bar

should foo or bar be preferred? Leftmost may seem logical at first but
when you have to deal with multiple entries and stacking, it occurs to
you that latter entries usually override the former.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Jason A. Donenfeld]

On Mon, May 29, 2017 at 5:33 PM, Michał Górny  wrote:
>
> Secondly, it might be reasonable to provide configurable priorities for
> solving multi-flag constraints. For example, we could use rightmost-
> preferred logic for package.use, e.g.:
>
>   */*  PROVIDER_SSL: openssl gnutls
>   dev-util/foo PROVIDER_SSL: polarssl
>
> which would mean that for all packages, gnutls is preferred over openssl
> (i.e. if ?? or ^^ applies, openssl will be disabled and gnutls will be
> used), and polarssl is additionally preferred over everything else for
> dev-util/foo.

Please, leftmost instead of rightmost?

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

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

[Michał Górny]

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

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

[Alexis Ballier]

On Wed, 07 Jun 2017 11:27:59 +0200
Michał Górny  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

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

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.

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

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.

> >  else: falsify(input, consequence)  
> > > useflag -> input[useflag] = False  
> 
> Looks mostly sane. You've missed '!flag' but that's trivial to add.

yeah, i realized after sending the email

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

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

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

[Michał Górny]

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,

b. for every X that solve() can solve reliably, nsolve(X) == ok.

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

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

> > Implication(useflag, consequence) ->
> 
>  if not input[useflag]: raise "impossible"

Why impossible? Unless I'm missing something, it's false already.

>  else: falsify(input, consequence)
> > useflag -> input[useflag] = False

Looks mostly sane. You've missed '!flag' but that's trivial to add.

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

> 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.
Preferably it should also be as simple as possible to avoid putting too
much complexity in the spec.


-- 
Best regards,
Michał Górny

signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Tue, 06 Jun 2017 19:39:04 +0200
Michał Górny  wrote:

> > [...]  
> > > > > The question is whether we want to:
> > > > > 
> > > > > a. actually try to solve this nesting insanity,
> > > > > 
> > > > > b. declare it unsupported and throw REQUIRED_USE mismatch on
> > > > > user,
> > > > > 
> > > > > c. ban it altogether.
> > > > 
> > > > 
> > > > I don't think it is *that* insane to support nesting :)
> > > > 
> > > > > ( ^^ ( ?? ( a b ) c ( d e ) ) f )  
> > 
> > If you really need that then you'd need to expand it manually. It
> > seems better to have it expanded internally automatically.
> > Remember you were the one wanting to keep || & co because they're
> > simpler to read and write ;)
> >   
> 
> Well, I was able to implement the logic for all-of blocks outside
> and inside other n-ary constraints, including the necessary logic
> transformations. Fun fact is, I was able to do it without implementing
> a complete set of logic functions and transformations in AST ;-).
> 
> I've just made it fail (correctly this time) with any other kind of
> nesting -- I don't think it's going to have a real use case and even
> if it did, there are more readable ways of solving the same problem.
> 
> The question is -- will you rebase now on top of my changes

yes that should be the goal but there are a lot of things to do prior
to that I think (thanks for doing it btw)

> (and preferably use nice logical changes with good commit messages),

Heh, I really meant 'quickndirty' :) it's actually good there is an
actual semi relevant commit message :p

> or should I try later to merge the rest of your code in? ;-)
> 
> 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.


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])
| AnyOf(l)   -> for i in l: falsify(input, i)
| AtMostOne(l) -> for i in l:
 if eval(input, clause): trueify(input, i)
| Implication(useflag, consequence) ->
 if not input[useflag]: raise "impossible"
 else: falsify(input, consequence)
| useflag -> input[useflag] = False
  


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


Now, what I need is basically a -funroll-all-loops on that algorithm
(We're Gentoo!): This explains why I butchered your code any why all
this is so dependent on the solving method chosen.

After unrolling the loops for a given REQUIRED_USE, this code will look
like:
if useflag1: if useflag2: ... : input[foo] = True; input[bar] = False
if baz: if biz: input[x] = True

In my notation this is:
[
  [useflag1, useflag2, ...]?[foo,!bar]
  [baz, biz]?[x]
]

And that's where 'nsolve' comes into play. Portage will do:

trueify(input, requse)
if not eval(input, requse) then rant

We want to guarantee 'requse' is in a form so that portage never has to
rant. My nsolve is only a sufficient condition for that. I was
expecting more like 10% of problematic cases, but considering the data
obtained is that less than .5% of required use in the tree would
require non trivial change and in all the cases I've seen those
required changes are legit, I believe we can move forward with this.


So, the very first thing to do is to agree that the above solver
(the trueify function) is what we want to 

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

[Michał Górny]

On wto, 2017-06-06 at 19:39 +0200, Michał Górny wrote:
> On wto, 2017-06-06 at 14:08 +0200, Alexis Ballier wrote:
> > On Mon, 05 Jun 2017 20:10:12 +0200
> > Michał Górny  wrote:
> > [...]
> > > > > Stand-alone makes little sense (and little trouble) but as you
> > > > > could have seen it's used nested in other thingies:
> > > > > 
> > > > > 1. || ( ( a b ) ( c d ) e )
> > > > > 
> > > > > 2. ?? ( ( a b ) ( c d ) e )
> > > > > 
> > > > > 3. ^^ ( ( a b ) ( c d ) e )  
> > > > 
> > > > Yeah that's the nesting problem causing a parse error.
> > > > Those should be expanded to implications. What I'm relying onto is
> > > > all clauses to be of the form '[list of conditions]? [list of
> > > > constraints]'  
> > > 
> > > I've noticed that you turned the implications into multi-conditions,
> > > breaking all my scripts ;-). Is the [list of conditions] conjunctive
> > > or disjunctive?
> > 
> > conjunctive as in foo? ( bar? ( baz ) ) -> [foo,bar]?[baz]
> 
> Yeah, I guess that's useful. I didn't do that originally because I
> wanted the AST to be fully compatible with REQUIRED_USE in Gentoo. But I
> guess it doesn't hurt, and makes a lot of the code simpler.
> 
> I've backported this change and adjusted all the remaining modules to
> work with it correctly.
> 
> > 
> > [...]
> > > > > The question is whether we want to:
> > > > > 
> > > > > a. actually try to solve this nesting insanity,
> > > > > 
> > > > > b. declare it unsupported and throw REQUIRED_USE mismatch on user,
> > > > > 
> > > > > c. ban it altogether.  
> > > > 
> > > > 
> > > > I don't think it is *that* insane to support nesting :)
> > > >   
> > > > > ( ^^ ( ?? ( a b ) c ( d e ) ) f )
> > 
> > If you really need that then you'd need to expand it manually. It seems
> > better to have it expanded internally automatically.
> > Remember you were the one wanting to keep || & co because they're
> > simpler to read and write ;)
> > 
> 
> Well, I was able to implement the logic for all-of blocks outside
> and inside other n-ary constraints, including the necessary logic
> transformations. Fun fact is, I was able to do it without implementing
> a complete set of logic functions and transformations in AST ;-).
> 
> I've just made it fail (correctly this time) with any other kind of
> nesting -- I don't think it's going to have a real use case and even if
> it did, there are more readable ways of solving the same problem.
> 
> The question is -- will you rebase now on top of my changes
> (and preferably use nice logical changes with good commit messages),
> or should I try later to merge the rest of your code in? ;-)
> 

I've rebased your changes and pushed them. However, I didn't alter
replace_nary to include '!a...' since it made the results worse for
me... it's possible that I did it wrong.

There's also some issue with all-of expressions that exhibits itself
on ibus. I'll look at that later.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Michał Górny]

On wto, 2017-06-06 at 14:08 +0200, Alexis Ballier wrote:
> On Mon, 05 Jun 2017 20:10:12 +0200
> Michał Górny  wrote:
> [...]
> > > > Stand-alone makes little sense (and little trouble) but as you
> > > > could have seen it's used nested in other thingies:
> > > > 
> > > > 1. || ( ( a b ) ( c d ) e )
> > > > 
> > > > 2. ?? ( ( a b ) ( c d ) e )
> > > > 
> > > > 3. ^^ ( ( a b ) ( c d ) e )  
> > > 
> > > Yeah that's the nesting problem causing a parse error.
> > > Those should be expanded to implications. What I'm relying onto is
> > > all clauses to be of the form '[list of conditions]? [list of
> > > constraints]'  
> > 
> > I've noticed that you turned the implications into multi-conditions,
> > breaking all my scripts ;-). Is the [list of conditions] conjunctive
> > or disjunctive?
> 
> conjunctive as in foo? ( bar? ( baz ) ) -> [foo,bar]?[baz]

Yeah, I guess that's useful. I didn't do that originally because I
wanted the AST to be fully compatible with REQUIRED_USE in Gentoo. But I
guess it doesn't hurt, and makes a lot of the code simpler.

I've backported this change and adjusted all the remaining modules to
work with it correctly.

> 
> [...]
> > > > The question is whether we want to:
> > > > 
> > > > a. actually try to solve this nesting insanity,
> > > > 
> > > > b. declare it unsupported and throw REQUIRED_USE mismatch on user,
> > > > 
> > > > c. ban it altogether.  
> > > 
> > > 
> > > I don't think it is *that* insane to support nesting :)
> > >   
> > > > ( ^^ ( ?? ( a b ) c ( d e ) ) f )
> 
> If you really need that then you'd need to expand it manually. It seems
> better to have it expanded internally automatically.
> Remember you were the one wanting to keep || & co because they're
> simpler to read and write ;)
> 

Well, I was able to implement the logic for all-of blocks outside
and inside other n-ary constraints, including the necessary logic
transformations. Fun fact is, I was able to do it without implementing
a complete set of logic functions and transformations in AST ;-).

I've just made it fail (correctly this time) with any other kind of
nesting -- I don't think it's going to have a real use case and even if
it did, there are more readable ways of solving the same problem.

The question is -- will you rebase now on top of my changes
(and preferably use nice logical changes with good commit messages),
or should I try later to merge the rest of your code in? ;-)

Also, do I presume correctly that for all supported cases (i.e. those
which your nsolve does not reject), solve and nsolve are compatible?

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Mon, 05 Jun 2017 20:10:12 +0200
Michał Górny  wrote:
[...]
> > > Stand-alone makes little sense (and little trouble) but as you
> > > could have seen it's used nested in other thingies:
> > > 
> > > 1. || ( ( a b ) ( c d ) e )
> > > 
> > > 2. ?? ( ( a b ) ( c d ) e )
> > > 
> > > 3. ^^ ( ( a b ) ( c d ) e )  
> > 
> > Yeah that's the nesting problem causing a parse error.
> > Those should be expanded to implications. What I'm relying onto is
> > all clauses to be of the form '[list of conditions]? [list of
> > constraints]'  
> 
> I've noticed that you turned the implications into multi-conditions,
> breaking all my scripts ;-). Is the [list of conditions] conjunctive
> or disjunctive?

conjunctive as in foo? ( bar? ( baz ) ) -> [foo,bar]?[baz]


[...]
> > > The question is whether we want to:
> > > 
> > > a. actually try to solve this nesting insanity,
> > > 
> > > b. declare it unsupported and throw REQUIRED_USE mismatch on user,
> > > 
> > > c. ban it altogether.  
> > 
> > 
> > I don't think it is *that* insane to support nesting :)
> >   
> 
> || ( ^^ ( ?? ( a b ) c ( d e ) ) f )

If you really need that then you'd need to expand it manually. It seems
better to have it expanded internally automatically.
Remember you were the one wanting to keep || & co because they're
simpler to read and write ;)

Alexis.

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

[Ciaran McCreesh]

On Mon, 05 Jun 2017 20:10:12 +0200
Michał Górny  wrote:
> I'm sure Ciaran will love to elaborate ;-).

It's doomed. Even if you get it to work, which you won't, it won't
survive ten seconds contact with the enemy.

-- 
Ciaran McCreesh

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

[Michał Górny]

On pon, 2017-06-05 at 19:24 +0200, Alexis Ballier wrote:
> On Mon, 05 Jun 2017 16:10:25 +0200
> Michał Górny  wrote:
> 
> > On pon, 2017-06-05 at 09:55 +0200, Alexis Ballier wrote:
> > > On Sun, 4 Jun 2017 10:59:38 +0200
> > > Alexis Ballier  wrote:
> > >   
> > > > Here's a quick n dirty code to play with, based on yours: 
> > > > https://github.com/aballier/required-use  
> > > 
> > > I've run that on the whole tree (considering all ebuilds with non
> > > empty REQUIRED_USE), some stats:
> > > 
> > > $ time python3 classify.py requsel 
> > > Stats:
> > >   Parse error: 16  
> > 
> > Hmm, how did you get those numbers? I just tested parsing and found
> > only 7 unique REQUIRED_USE entries that fail. However, my sample file
> > is only around 1000 entries long, so either I failed to get all of
> > them, or you didn't deduplicate your list ;-). More on it below.
> 
> I did not deduplicate anything. I took every single ebuild and
> generated a list of req use out of it. Meaning if you had 10 ebuilds
> for 1 package with the same req use that'd count as 10 above.
> 
> [...]
> > > The cycle is mostly due to:
> > > $ python3 nsolve.py 'llvm? ( gallium ) gallium? ( llvm )'
> > > [...]
> > > toposort.CircularDependencyError: Circular dependencies exist among
> > > these items: {[gallium]? => [llvm]:{[llvm]? => [gallium]}, [llvm]?
> > > => [gallium]:{[gallium]? => [llvm]}}
> > > 
> > > 
> > > This is something I had overseen when replacing 'a q'_j is some p_i
> > > and one of q_1 ... q_m might be false' by only 'a q'_j is some
> > > p_i'; it can be replaced without changing anything in the way PM
> > > would solve it by "a q'_j is some p_i and the set of {q_j} is not a
> > > subset of q' union p'" (that is, {q_i} is not trivially true if the
> > > 2nd clause is applied). Extending that, we get those stats:  
> > 
> > I'm not even trying to understand the things you say with indexes but
> > I trust you know what you're doing.
> 
> With that kind of things it's good to have someone having a second
> look. It's so easy to forget a case or to miss a simplification.

I'm sure Ciaran will love to elaborate ;-).

> > Well, I guess it's time to hit the next level. For a start, we have to
> > handle all-of groups, i.e.:
> > 
> >   ( a b c )
> > 
> > Stand-alone makes little sense (and little trouble) but as you could
> > have seen it's used nested in other thingies:
> > 
> > 1. || ( ( a b ) ( c d ) e )
> > 
> > 2. ?? ( ( a b ) ( c d ) e )
> > 
> > 3. ^^ ( ( a b ) ( c d ) e )
> 
> Yeah that's the nesting problem causing a parse error.
> Those should be expanded to implications. What I'm relying onto is all
> clauses to be of the form '[list of conditions]? [list of constraints]'

I've noticed that you turned the implications into multi-conditions,
breaking all my scripts ;-). Is the [list of conditions] conjunctive or
disjunctive?

> > For verifying constraints, they are not bad. We just follow the
> > generic rule that the branch evaluates to true if all subexpressions
> > are true. 
> > 
> > For solving, it might be a little unclear on how to proceed with
> > partially true branches but for the sake of simplicity I would just
> > ignore them and behave as if they were false. That is, case (1) with
> > USE='c' would result in 'a b' being enabled.
> > 
> > The practical uses I've seen are:
> > 
> > a. || ( deprecated ( gtk3 introspection ) )
> > 
> > I guess this one would be equivalent to:
> > 
> >   !gtk3? ( !introspection? ( deprecated ) )
> 
> Unfortunately no. Favoring leftmost, you need to enable 'deprecated'
> when either gtk3 or introspection is false.
> 
> That'd be:
> !gtk3? ( deprecated )
> !introspection? ( deprecated )

Well, I meant 'by current rules', without considering preferences.

> Fortunately we can distribute \/ and /\:
> > > ( deprecated ( gtk3 introspection ) )
> 
> is equivalent to:
> > > ( deprecated gtk3 )
> > > ( deprecated introspection )
> 
> giving the above implication translation.
> 
> This can be extended to 
> > > ( ( a1 a2 a3 ... ) ( b1 b2 b3 ... ) ... ) to handle all cases.
> 
> 
> 
> > b. ^^ ( ( !32bit 64bit ) ( 32bit !64bit ) ( 32bit 64bit ) )
> > 
> > This looks like a crazy way of saying:
> > 
> >   || ( 32bit 64bit )
> 
> Hmm yes
> 
> 
> > c. ^^ ( ( !ruby !s7 ) ( ruby !s7 ) ( !ruby s7 ) )
> > 
> > This looks like an insane version of:
> > 
> >   ?? ( ruby s7 )
> 
> 
> yes too it seems
> 
> 
> 
> > except that per my solver it just disables both when both are set ;-).
> 
> That's kind of the point. And that's why it is important to have the
> solving rules well defined. Depending on how REQUIRED_USE is written,
> it will be solved differently even for equivalent logical formulas.
> 
> 
> > Not sure if the extra complexity is worth for roughly one valid use
> > case, and a lot of insanity.
> 
> I think this can be done without too much pain. As you noticed, replace
> '^^ ( whatever )' by '|| ( whatever ) ?? ( whatever )' so we're left
> with 

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

[Alexis Ballier]

On Mon, 05 Jun 2017 16:10:25 +0200
Michał Górny  wrote:

> On pon, 2017-06-05 at 09:55 +0200, Alexis Ballier wrote:
> > On Sun, 4 Jun 2017 10:59:38 +0200
> > Alexis Ballier  wrote:
> >   
> > > Here's a quick n dirty code to play with, based on yours: 
> > > https://github.com/aballier/required-use  
> > 
> > I've run that on the whole tree (considering all ebuilds with non
> > empty REQUIRED_USE), some stats:
> > 
> > $ time python3 classify.py requsel 
> > Stats:
> > Parse error: 16  
> 
> Hmm, how did you get those numbers? I just tested parsing and found
> only 7 unique REQUIRED_USE entries that fail. However, my sample file
> is only around 1000 entries long, so either I failed to get all of
> them, or you didn't deduplicate your list ;-). More on it below.

I did not deduplicate anything. I took every single ebuild and
generated a list of req use out of it. Meaning if you had 10 ebuilds
for 1 package with the same req use that'd count as 10 above.

[...]
> > The cycle is mostly due to:
> > $ python3 nsolve.py 'llvm? ( gallium ) gallium? ( llvm )'
> > [...]
> > toposort.CircularDependencyError: Circular dependencies exist among
> > these items: {[gallium]? => [llvm]:{[llvm]? => [gallium]}, [llvm]?
> > => [gallium]:{[gallium]? => [llvm]}}
> > 
> > 
> > This is something I had overseen when replacing 'a q'_j is some p_i
> > and one of q_1 ... q_m might be false' by only 'a q'_j is some
> > p_i'; it can be replaced without changing anything in the way PM
> > would solve it by "a q'_j is some p_i and the set of {q_j} is not a
> > subset of q' union p'" (that is, {q_i} is not trivially true if the
> > 2nd clause is applied). Extending that, we get those stats:  
> 
> I'm not even trying to understand the things you say with indexes but
> I trust you know what you're doing.

With that kind of things it's good to have someone having a second
look. It's so easy to forget a case or to miss a simplification.

> For completeness, we need to
> consider three cross-dependent states:
> 
> a. a? ( b ) b? ( a )


that's exactly the above :p

{q_j} is {b}, {q'} is {a}, {p'} is {b}; {b} is a subset of {a} union
{b}


[...]
> b. !a? ( !b ) !b? ( !a )

that's also the above with s/!b/b/ s/!a/a/ :=)

> c. a? ( b ) !a? ( !b )

that's already handled.

[...]
> > I'll let you play with it, but for me it seems this would work quite
> > nicely.
> >   
> 
> Well, I guess it's time to hit the next level. For a start, we have to
> handle all-of groups, i.e.:
> 
>   ( a b c )
> 
> Stand-alone makes little sense (and little trouble) but as you could
> have seen it's used nested in other thingies:
> 
> 1. || ( ( a b ) ( c d ) e )
> 
> 2. ?? ( ( a b ) ( c d ) e )
> 
> 3. ^^ ( ( a b ) ( c d ) e )

Yeah that's the nesting problem causing a parse error.
Those should be expanded to implications. What I'm relying onto is all
clauses to be of the form '[list of conditions]? [list of constraints]'


> For verifying constraints, they are not bad. We just follow the
> generic rule that the branch evaluates to true if all subexpressions
> are true. 
> 
> For solving, it might be a little unclear on how to proceed with
> partially true branches but for the sake of simplicity I would just
> ignore them and behave as if they were false. That is, case (1) with
> USE='c' would result in 'a b' being enabled.
> 
> The practical uses I've seen are:
> 
> a. || ( deprecated ( gtk3 introspection ) )
> 
> I guess this one would be equivalent to:
> 
>   !gtk3? ( !introspection? ( deprecated ) )

Unfortunately no. Favoring leftmost, you need to enable 'deprecated'
when either gtk3 or introspection is false.

That'd be:
!gtk3? ( deprecated )
!introspection? ( deprecated )


Fortunately we can distribute \/ and /\:
|| ( deprecated ( gtk3 introspection ) )
is equivalent to:
|| ( deprecated gtk3 )
|| ( deprecated introspection )

giving the above implication translation.

This can be extended to 
|| ( ( a1 a2 a3 ... ) ( b1 b2 b3 ... ) ... ) to handle all cases.



> b. ^^ ( ( !32bit 64bit ) ( 32bit !64bit ) ( 32bit 64bit ) )
> 
> This looks like a crazy way of saying:
> 
>   || ( 32bit 64bit )

Hmm yes


> c. ^^ ( ( !ruby !s7 ) ( ruby !s7 ) ( !ruby s7 ) )
> 
> This looks like an insane version of:
> 
>   ?? ( ruby s7 )


yes too it seems



> except that per my solver it just disables both when both are set ;-).

That's kind of the point. And that's why it is important to have the
solving rules well defined. Depending on how REQUIRED_USE is written,
it will be solved differently even for equivalent logical formulas.


> Not sure if the extra complexity is worth for roughly one valid use
> case, and a lot of insanity.

I think this can be done without too much pain. As you noticed, replace
'^^ ( whatever )' by '|| ( whatever ) ?? ( whatever )' so we're left
with only || and ?? (and 'and' denoted by space and grouping in our
notation).

|| ( clause1 clause2 ... ) is replaced by
[!clause1 !clause2 ...]?[clause1]

?? ( 

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

[Michał Górny]

On pon, 2017-06-05 at 09:55 +0200, Alexis Ballier wrote:
> On Sun, 4 Jun 2017 10:59:38 +0200
> Alexis Ballier  wrote:
> 
> > Here's a quick n dirty code to play with, based on yours: 
> > https://github.com/aballier/required-use
> 
> I've run that on the whole tree (considering all ebuilds with non
> empty REQUIRED_USE), some stats:
> 
> $ time python3 classify.py requsel 
> Stats:
>   Parse error: 16

Hmm, how did you get those numbers? I just tested parsing and found only
 7 unique REQUIRED_USE entries that fail. However, my sample file is
only around 1000 entries long, so either I failed to get all of them, or
you didn't deduplicate your list ;-). More on it below.

>   Good: 8316
>   Need topo sort: 140
>   Cyclic: 57
> 
> real  0m2.996s
> user  0m2.950s
> sys   0m0.004s
> 
> 
> Running time is good I think.
> Parse error is some nested construct not supported by your parser that
> I have not fixed either.

Yes, the time is great. It means we can actually think about integrating
it with repoman/pkgcheck.

> The cycle is mostly due to:
> $ python3 nsolve.py 'llvm? ( gallium ) gallium? ( llvm )'
> [...]
> toposort.CircularDependencyError: Circular dependencies exist among
> these items: {[gallium]? => [llvm]:{[llvm]? => [gallium]}, [llvm]? =>
> [gallium]:{[gallium]? => [llvm]}}
> 
> 
> This is something I had overseen when replacing 'a q'_j is some p_i and
> one of q_1 ... q_m might be false' by only 'a q'_j is some p_i'; it can
> be replaced without changing anything in the way PM would solve it by
> "a q'_j is some p_i and the set of {q_j} is not a subset of q' union
> p'" (that is, {q_i} is not trivially true if the 2nd clause is
> applied). Extending that, we get those stats:

I'm not even trying to understand the things you say with indexes but I
trust you know what you're doing. For completeness, we need to consider
three cross-dependent states:

a. a? ( b ) b? ( a )

i.e.:

  y_1 = y_2 = x_1 v x_2

iow, enabling either of the flags causes both of them being enabled. I'm
not sure if we have a valid use case to keep such flags long-term but
short-term they could be useful to handle transition periods when
upstream merges two features (or makes them cross-dependent) and we want
to preserve compatibility with split flags.

b. !a? ( !b ) !b? ( !a )

i.e.:

  y_1 = y_2 = x_1 ^ x_2

iow, you have to enable both flags to keep them enabled. Not sure if we
have any valid use case for this.

c. a? ( b ) !a? ( !b )

i.e.

  y_1 = y_2 = x_1

This mostly a reduced result of:

  a? ( || ( b c d ... ) ) !a? ( !b !c !d ... )

[NB: it would be useful to have a short syntax for that]

I suspect this will be commonly useful to express provider dependencies,
i.e. enforcing a particular constraint for providers only when
the feature flag is enabled, and disabling all provider flags when it is
not.

FWICS, my version solves all three cases correctly, and your does not
explode on them.

> I'll let you play with it, but for me it seems this would work quite
> nicely.
> 

Well, I guess it's time to hit the next level. For a start, we have to
handle all-of groups, i.e.:

  ( a b c )

Stand-alone makes little sense (and little trouble) but as you could
have seen it's used nested in other thingies:

1. || ( ( a b ) ( c d ) e )

2. ?? ( ( a b ) ( c d ) e )

3. ^^ ( ( a b ) ( c d ) e )

For verifying constraints, they are not bad. We just follow the generic
rule that the branch evaluates to true if all subexpressions are true. 

For solving, it might be a little unclear on how to proceed with
partially true branches but for the sake of simplicity I would just
ignore them and behave as if they were false. That is, case (1) with
USE='c' would result in 'a b' being enabled.

The practical uses I've seen are:

a. || ( deprecated ( gtk3 introspection ) )

I guess this one would be equivalent to:

  !gtk3? ( !introspection? ( deprecated ) )

b. ^^ ( ( !32bit 64bit ) ( 32bit !64bit ) ( 32bit 64bit ) )

This looks like a crazy way of saying:

  || ( 32bit 64bit )

c. ^^ ( ( !ruby !s7 ) ( ruby !s7 ) ( !ruby s7 ) )

This looks like an insane version of:

  ?? ( ruby s7 )

except that per my solver it just disables both when both are set ;-).

Not sure if the extra complexity is worth for roughly one valid use
case, and a lot of insanity.

I've pushed a simple update to my parser to account for this. However,
it doesn't support replace_nary atm, so it won't work for you.


Of course past that there's a deeper insanity: all those constructs can
be nested without limits. Verification is possible, solving maybe -- but
I'm not sure if we even want to try to think what the correct solution
would be.

There's only one use of this:

  ?? ( gl3plus ( || ( gles2 gles3 ) ) )

FWICS, it probably works like this;

 g   g
 l   l
 3 g g   3 g g
 p l l   p l l
 l e e   l e e
 u s s   u s s
 s 2 3 | s 2 3
 0 0 0 | 0 0 0 (==)
 0 0 1 | 0 0 1 (==)
 0 1 0 | 0 1 0 (==)
 0 1 1 | 0 1 1 (==)
 1 0 0 | 1 0 0 

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

[Alexis Ballier]

On Mon, 29 May 2017 17:33:13 +0200
Michał Górny  wrote:

> 2.4. Backwards compatibility
> 


Considering the discussions in that thread, a natural way to move
forward now seems to be:

1. Define a way to solve constraints deterministically
2. Get a warning check into repoman to ensure REQUIRED_USE are solved
   that way.
3. Get those repoman warnings fixed.
4. Implement an optional FEATURES in portage for automatic solving
   of REQUIRED_USE.
5. If all goes well, mandate that solving in next EAPI and make the
   repoman warning an error for those EAPIs.

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

[Alexis Ballier]

On Sun, 4 Jun 2017 10:59:38 +0200
Alexis Ballier  wrote:

> Here's a quick n dirty code to play with, based on yours: 
> https://github.com/aballier/required-use

I've run that on the whole tree (considering all ebuilds with non
empty REQUIRED_USE), some stats:

$ time python3 classify.py requsel 
Stats:
Parse error: 16
Good: 8316
Need topo sort: 140
Cyclic: 57

real0m2.996s
user0m2.950s
sys 0m0.004s


Running time is good I think.
Parse error is some nested construct not supported by your parser that
I have not fixed either.


~2.5% simply need to be reordered. ~0.6% require more clever thinking.


Let's have a look at a few of them:

sys-fs/cryptsetup-1.7.5
^^ ( gcrypt kernel nettle openssl ) python? ( ||
( python_targets_python2_7 python_targets_python3_4
python_targets_python3_5 python_targets_python3_6 ) )
static? ( !gcrypt )

USE='-* static' is painful: the first ^^ will enable gcrypt, static?
( !gcrypt ) will disable it. Reordering the ^^ so that kernel appears
first fixes the cycle.


media-libs/mesa-13.0.6
|| ( gcrypt libressl nettle openssl ) d3d9?
( dri3 gallium ) llvm? ( gallium ) opencl? ( gallium llvm ) openmax?
( gallium ) gles1? ( egl ) gles2? ( egl ) vaapi? ( gallium ) vdpau?
( gallium ) vulkan? ( video_cards_i965 ) wayland? ( egl gbm ) xa?
( gallium ) video_cards_freedreno? ( gallium ) video_cards_intel?
( classic ) video_cards_i915? ( || ( classic gallium ) )
video_cards_i965? ( classic ) video_cards_nouveau? ( || ( classic
gallium ) ) video_cards_radeon? ( || ( classic gallium ) gallium?
( x86? ( llvm ) amd64? ( llvm ) ) ) video_cards_r100? ( classic )
video_cards_r200? ( classic ) video_cards_r300? ( gallium x86? ( llvm )
amd64? ( llvm ) ) video_cards_r600? ( gallium ) video_cards_radeonsi?
( gallium llvm ) video_cards_vmware? ( gallium )

The cycle is mostly due to:
$ python3 nsolve.py 'llvm? ( gallium ) gallium? ( llvm )'
[...]
toposort.CircularDependencyError: Circular dependencies exist among
these items: {[gallium]? => [llvm]:{[llvm]? => [gallium]}, [llvm]? =>
[gallium]:{[gallium]? => [llvm]}}


This is something I had overseen when replacing 'a q'_j is some p_i and
one of q_1 ... q_m might be false' by only 'a q'_j is some p_i'; it can
be replaced without changing anything in the way PM would solve it by
"a q'_j is some p_i and the set of {q_j} is not a subset of q' union
p'" (that is, {q_i} is not trivially true if the 2nd clause is
applied). Extending that, we get those stats:

Stats:
Parse error: 16
Good: 8325
Need topo sort: 146
Cyclic: 42

real0m1.575s
user0m1.563s
sys 0m0.012s


Now we seem to get only valid warnings (I have not checked them all
though):

sys-firmware/seabios-1.10.1:
debug? ( !binary ) !amd64? ( !x86? ( binary ) )

USE="debug -amd64 -x86" ?


sci-libs/ceres-solver-1.11.0:
test? ( gflags ) sparse? ( lapack ) abi_x86_32? ( !sparse !lapack )

USE='-* sparse -lapack abi_x86_32' shows a conflict between the last 2
clauses. Better write:

test? ( gflags ) !abi_x86_32? ( sparse? ( lapack ) ) abi_x86_32?
( !sparse !lapack )

which makes the test work



mail-mta/exim-4.89
dane? ( !gnutls ) dmarc? ( spf dkim ) pkcs11? ( gnutls ) spf?
( exiscan-acl ) srs? ( exiscan-acl )

USE="dane pkcs11" ?

sci-libs/hdf5-1.8.18:
threads? ( !cxx !mpi !fortran !hl ) fortran2003? ( fortran )

USE="threads fortran2003" ?





I'll let you play with it, but for me it seems this would work quite
nicely.


Alexis.

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

[Alexis Ballier]

Here's a quick n dirty code to play with, based on yours: 
https://github.com/aballier/required-use

On Sat, 3 Jun 2017 18:58:35 +0200
Alexis Ballier  wrote:

> > 1. ^^ ( pst1 pst2 pst3.. ) pst1? ( pt1 ) pst2? ( pt2 ) pst3? ( pt3
> > )..  

$ python3 ./nsolve.py '^^ ( pst1 pst2 pst3 ) pst1? ( pt1 ) pst2? ( pt2
) pst3? ( pt3 )'

[[!pst1, !pst2, !pst3]? => [pst1], [pst1]? => [!pst2],
[pst1]? => [!pst3], [!pst1, pst2]? => [!pst3], [pst1]? => [pt1],
[pst2]? => [pt2], [pst3]? => [pt3]]


> > 2. ^^ ( pst1 pst2.. ) pst1? ( pt1 ) pst2? ( pt2 ).. ^^ ( pt1 pt2 )



$ python3 ./nsolve.py '^^ ( pst1 pst2 ) pst1? ( pt1 ) pst2? ( pt2 ) ^^
( pt1 pt2 )'

[[!pst1, !pst2]? => [pst1], [pst1]? => [!pst2], [pst1]? => [pt1],
[pst2]? => [pt2], [!pt1, !pt2]? => [pt1], [pt1]? => [!pt2]]

[[pt1]? => [!pt2]] can break [[pst2]? => [pt2]]


> ^^ ( pst1 pst2.. ) pst1? ( pt1 !pt2 ... ) pst2? ( !pt1 pt2 ... )..

$ python3 ./nsolve.py '^^ ( pst1 pst2 ) pst1? ( pt1 !pt2 ) pst2? ( !pt1
pt2 )'

[[!pst1, !pst2]? => [pst1], [pst1]? => [!pst2], [pst1]? => [pt1],
[pst1]? => [!pt2], [pst2]? => [!pt1], [pst2]? => [pt2]]

[[pst2]? => [!pt1]] can break [[pst1]? => [pt1]]
[[pst2]? => [pt2]] can break [[pst1]? => [!pt2]]

> pst1? ( pt1 !pt2 ... )
> pst2? ( !pt1? ( pt2 !pt3 ... ) )
> pst3? ( !pt1? ( !pt2? ( pt3 !pt4 ... ) ) )

$ python3 ./nsolve.py '^^ ( pst1 pst2 ) pst1? ( pt1 !pt2 ) pst2?
( !pst1? ( !pt1 pt2 ) )'

[[!pst1, !pst2]? => [pst1], [pst1]? => [!pst2], [pst1]? => [pt1],
[pst1]? => [!pt2], [pst2, !pst1]? => [!pt1], [pst2, !pst1]? => [pt2]]


All good.


> > 3. doc? ( || ( pt3 pt4 ) ) || ( pt1 pt2 pt3 pt4 )

$ python3 ./nsolve.py 'doc? ( || ( pt3 pt4 ) ) || ( pt1 pt2 pt3 pt4 )'
[[doc, !pt3, !pt4]? => [pt3], [!pt1, !pt2, !pt3, !pt4]? => [pt1]]




Note: the code only reports errors if a clause can break another clause
left to it. It doesn't do topological sorting nor cycle reporting yet.

Alexis.

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

[Alexis Ballier]

On Sat, 03 Jun 2017 17:33:09 +0200
Michał Górny  wrote:

> On sob, 2017-06-03 at 13:00 +0200, Alexis Ballier wrote:
> > This whole thing definitely needs more thought and feedback but for
> > now those extra restrictions seem quite natural to me, allow easy
> > solving on the PM side and allow to have useful feedback from
> > repoman. 
> 
> Well, I'll try to figure out the magic you were telling me later but
> as a quick note, my specific use case for this are Python targets, so
> I'm going throw a few basic concepts that need to work for you to
> play with ;-).
> 
> In the following samples pt1,2,.. stands for PYTHON_TARGETS;
> pst1,2,... for PYTHON_SINGLE_TARGET. Eventually I'd like to kill the
> latter but that depends on how well the autosolving works.
> 
> 1. ^^ ( pst1 pst2 pst3.. ) pst1? ( pt1 ) pst2? ( pt2 ) pst3? ( pt3 )..

the pt{1,2,...} part does not matter here: they all fail point 4 when
compared as 2nd clause to the others (each ptX appears only once in the
whole expression), so this boils down to solving n-ary ^^, and to how
those are translated: you can have several translations but some would
not work properly. Let's try:
(a) pst1? ( !pst2 !pst3 )
(b) pst2? ( !pst3 )
(c) !pst3? ( !pst2? ( pst1 ) )

Between (a) and (c), points 1 to 3 hold (those points are reflexive).
For point 4, "a q'_j is some p_i" will hold in both ways, so we do
actually have a cycle between them. Bad luck.

Let's write (c) as:
(c) !pst3? ( !pst2? ( !pst1? ( pst1 ) ) )

Now, (c) can't break (a) because of point 1: pst1 in (a) vs !pst1 in
(c).


(b) can't break (a) because of point 2: q_i=!pst2 is the negation of
p_j=pst2.

(c) can't break (b) because pst2 vs !pst2 (point 1).


So, this formulation works:
(a) pst1? ( !pst2 !pst3 )
(b) pst2? ( !pst3 )
(c) !pst3? ( !pst2? ( !pst1? ( pst1 ) ) )

USE="pst1 whatever" will enable only pst1. USE="-pst1 pst2 whatever"
will enable only pst2. USE="-pst1 -pst2 pst3" will leave it alone.
USE="-pst{1,2,3}" will enable pst1.



Note that "pst1? ( pt1 ) pst2? ( pt2 ) pst3? ( pt3 ) ^^ ( pst1 pst2
pst3.. )" is a different story: (c) expanded as above can break 'pst1?
( pt1 )' (point 4: a q'_j is some p_i) and you can actually check that
with USE="-pt* -pst*"; you'll need 2 passes to get the proper solution.
Fortunately, this is still a DAG and repoman would be able to propose an
ordering requiring only one pass.


[...]
> 2. ^^ ( pst1 pst2.. ) pst1? ( pt1 ) pst2? ( pt2 ).. ^^ ( pt1 pt2 )
> 
> This is a possible extension of the above for the migration period.
> The idea is that exactly one PST must be selected, and only the
> matching PT must be selected (others are implicitly disabled).

If we expand '^^ ( pt1 pt2 )' as above we get:
(d) pt1? ( !pt2 )
(e) !pt2? ( !pt1? ( pt1 ) )

Here, (d) is annoying: it can break and be broken by 'pst2? ( pt2 )'.
There would be a cycle and this would be rejected/notified.

If you think about it, this would mean I have set USE="-* pt1 pst2";
pst2 forcing to enable pt2 but '^^ ( pt1 pt2 )' with pt1 enabled would
prefer pt1 and disable pt2 again... This hints the solution: You need
to define who wins between pt and pst.

Instead you could write it:
^^ ( pst1 pst2.. ) pst1? ( pt1 !pt2 ... ) pst2? ( !pt1 pt2 ... )..
But then 'pst2? ( !pt1 pt2 ... )' can break each other with 'pst1?
( pt1 !pt2 ... )' in the sense I defined because of point 4 (A q_i is
the negation of a q_'j); you'll get the repoman notification about a
cycle. This is a case of a perfectly valid constraint that is rejected
by the restriction.

It is valid because we know we are guaranteed exactly one pstX will
be enabled. We can hint the solver with that by writing:
^^ ( pst1 pst2.. )
pst1? ( pt1 !pt2 ... )
pst2? ( !pt1? ( pt2 !pt3 ... ) )
pst3? ( !pt1? ( !pt2? ( pt3 !pt4 ... ) ) )


Now we're good: For j>i, solving a pst{j} line does not break a pst{i}
one because of point 2: A q_i (pt{i}) is the negation of a p'_j
(!pt{i}).



It's getting a bit ugly but it's probably bearable with good reporting
from static checkers (repoman).



> 3. doc? ( || ( pt3 pt4 ) ) || ( pt1 pt2 pt3 pt4 )
> 
> This is distutils-r1 with USE=doc requiring python2. Note that it's
> an example where the second || is added via eclass [NB: we've checked
> and PMS says eclass values are appended to ebuild value].


Much simpler here:
(a) doc? ( !pt4? ( pt3 ) )
(b) !pt4? ( !pt3? ( !pt2? ( pt1 ) )

(b) can't break (a) because of point 4: Neither 'a q_i is
  the negation of a q_'j' nor 'a q'_j is some p_i' hold. We're good.


USE="-* doc" will enable pt3 only. USE="-* pt{whatever} doc" will
enable pt3 (if not enabled) unless pt{whatever} contains pt4.

Alexis.

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

[Michał Górny]

On sob, 2017-06-03 at 13:00 +0200, Alexis Ballier wrote:
> This whole thing definitely needs more thought and feedback but for now
> those extra restrictions seem quite natural to me, allow easy solving
> on the PM side and allow to have useful feedback from repoman.
> 

Well, I'll try to figure out the magic you were telling me later but as
a quick note, my specific use case for this are Python targets, so I'm
going throw a few basic concepts that need to work for you to play with
;-).

In the following samples pt1,2,.. stands for PYTHON_TARGETS; pst1,2,...
for PYTHON_SINGLE_TARGET. Eventually I'd like to kill the latter but
that depends on how well the autosolving works.

1. ^^ ( pst1 pst2 pst3.. ) pst1? ( pt1 ) pst2? ( pt2 ) pst3? ( pt3 )..

This is the standard constraint for PYTHON_SINGLE_TARGET -- it needs to
ensure that exactly one PYTHON_SINGLE_TARGET is selected, and that
the matching PYTHON_TARGETS value is (other PYTHON_TARGETS can be
enabled or disabled -- doesn't matter).

2. ^^ ( pst1 pst2.. ) pst1? ( pt1 ) pst2? ( pt2 ).. ^^ ( pt1 pt2 )

This is a possible extension of the above for the migration period.
The idea is that exactly one PST must be selected, and only the matching
PT must be selected (others are implicitly disabled).

3. doc? ( || ( pt3 pt4 ) ) || ( pt1 pt2 pt3 pt4 )

This is distutils-r1 with USE=doc requiring python2. Note that it's
an example where the second || is added via eclass [NB: we've checked
and PMS says eclass values are appended to ebuild value].



-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Fri, 02 Jun 2017 15:55:17 +0200
Michał Górny  wrote:

> On pią, 2017-06-02 at 13:27 +0200, Alexis Ballier wrote:
> > On Thu, 01 Jun 2017 23:31:25 +0200
> > Michał Górny  wrote:
> > [...]  
> > > > There are probably dozens of ways to make that non
> > > > deterministic. Here's one: USE='-*'. Apply '|| ( cli cgi fpm
> > > > apache2 embed phpdbg )' last; this enables 'cli'. Since it's
> > > > the last one, REQUIRED_USE is not satisfied because of 'cli?
> > > > ( ^^ ( readline libedit ) )'. If you process it first, then you
> > > > enable cli and readline and are good.
> > > 
> > > You just take a second iteration, and things fall into place.
> > > That's not a problem.
> > >   
> > > > > > Also, what happens if we applied all the constraints and
> > > > > > obtained some useflags setting that still fails REQUIRED_USE
> > > > > > check ?  
> > > > > 
> > > > > It can't happen. If you can apply all the constraints, then
> > > > > implicitly REQUIRED_USE is satisfied. If you can't apply all
> > > > > the constraints, then it just fails. Of course, we want to
> > > > > ultimately avoid that case.
> > > > 
> > > > See the php example above. How do you ensure this does not
> > > > happen?
> > > > 
> > > > Note that your assertion 'If you can apply all the constraints,
> > > > then implicitly REQUIRED_USE is satisfied.' is false: You're
> > > > changing the values of useflags, thus might violate some
> > > > previously checked constraint.
> > > 
> > > So you reiterate. Either you reach a solution (preferably there's
> > > only a single valid solution you can reach) or you hit a previous
> > > state which indicates a loop and you fail.  
> > 
> > 
> > So, PM, for every ebuild, will need to store the (at most) 2^n
> > states it has already seen while trying to solve REQUIRED_USE and
> > iterate until it cannot proceed anymore or falls into a previous
> > state (so that's 2^n time too). That way we go from a linear time &
> > linear space algorithm to one in exponential time & space. That's
> > probably not a good idea.  
> 
> I don't think that's actually going to happen. You'd have to try
> really hard to get over n-1 iterations. I mean, the only simple way I
> can think of is:
> 
>   b? ( a ) c? ( b ) d? ( c ) e? ( d ) ...
> 
> and this only means n-1 iterations. Can you think of a better way to
> force multiple iterations that can be written without making
> REQUIRED_USE completely unreadable? How likely is that going to happen
> accidentally?

I don't see any reason why it should terminate after n iterations; I
don't see any example of how to do more either. I can try to think more
about it, but maybe it is not even needed, see below.

> > I think it's better to limit the number of iterations to some
> > constant. I'd say 1, then fail if REQUIRED_USE is still not
> > satisfied. Maybe 2 or 3 can be useful but I think it'd be much
> > harder to provide automated checks for that and much harder for
> > ebuild writers to understand what will happen with the REQUIRED_USE
> > they're about to write. 
> 
> Well, I don't mind setting that. All my tests (that weren't
> deliberately abusing the algorithm) were able to finish in a single
> iteration. 2 or 3 should probably be safe for all the reasonable
> uses. However, if we're not going to verify all possible values on
> repoman side, I think it would be better to have a larger limit for
> users, to not have things explode on them unnecessarily.


Look, if we assume left to right solving, only one iteration possible
and all the constraints to be of the form 'p_1? p_2? ... p_n? ( q_1 ...
q_m )' where p_i and q_i are either 'useflag' or '!useflag', then we
only have to check when such a clause can change a previously satisfied
clause to unsatisfied.

For two clauses: 
"p_1? p_2? ... p_n? ( q_1 ... q_m )" and "p'_1? p'_2? ... p'_{n'}?
( q'_1 ... q'_{m'} )", assuming the first is satisfied, when can solving
the 2nd break the 1st?

It must be that:
1.The conditions are compatible: No p_i is the negation of a p'_j.
2.Solving the 1st does not make the 2nd trivially true: No q_i is
  the negation of a p'_j.
3.Solving the 2nd does not make the 1st trivially true afterwards: No
  p_i is the negation of a q'_j.
4.Solving the 2nd does break the 1st assumption: (A q_i is
  the negation of a q_'j) or (a q'_j is some p_i and one of q_1 ... q_m
  might be false).

The only a priori non polynomial part here is "one of q_1 ... q_m
might be false". If we do not check that (only check that some q'_j is
some p_i), we are still guaranteed that the 2nd clause cannot break the
1st but we might end up rejecting otherwise valid constructs.

Doing that, we have a check guaranteeing that the above algorithm will
always provide a valid answer for 'clause_1 clause_2' in
O(|clause_1|*|clause_2|) time.
For a complete REQUIRED_USE='clause_1 ... clause_k', it is sufficient
to check that, for any i>j, clause_i cannot break clause_j in the above

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

[Michał Górny]

On pią, 2017-06-02 at 14:16 +0200, Alexis Ballier wrote:
> On Thu, 01 Jun 2017 23:31:25 +0200
> Michał Górny  wrote:
> > My current code is on github [1]. It's ugly, slow and incomplete. It's
> > merely a proof-of-concept and testing toy but still could give some
> > clues.
> > 
> > [1]:https://github.com/mgorny/required-use
> 
> 
> Nice work by the way. I've not looked much at the code but I've tried
> it on a few examples and it worked well. Then I tried on the php
> example and it didn't finish within 30 mins so I stopped it.
> 
> I think we should really try to find a sub-exponential solution to
> this, I doubt there's anything that can be done if the only solution is
> to enumerate all the possibilities.

Well, as I said, you can split it into multiple independent groups
(that's what I did). Then you solve each of them independently. However,
that was done purely for research needs and I'm not sure how useful it's
going to be in practice.

I can imagine something like:

  || ( foo_* )

for 30-40 flag USE_EXPAND being a problem -- while a trivial constraint
to verify. So the 2^n solution I'd rather consider a nice way to test
the algorithm rather than something potentially useful for verification.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Michał Górny]

On pią, 2017-06-02 at 13:27 +0200, Alexis Ballier wrote:
> On Thu, 01 Jun 2017 23:31:25 +0200
> Michał Górny  wrote:
> [...]
> > > There are probably dozens of ways to make that non deterministic.
> > > Here's one: USE='-*'. Apply '|| ( cli cgi fpm apache2 embed phpdbg
> > > )' last; this enables 'cli'. Since it's the last one, REQUIRED_USE
> > > is not satisfied because of 'cli? ( ^^ ( readline libedit ) )'.
> > > If you process it first, then you enable cli and readline and are
> > > good.  
> > 
> > You just take a second iteration, and things fall into place. That's
> > not a problem.
> > 
> > > > > Also, what happens if we applied all the constraints and
> > > > > obtained some useflags setting that still fails REQUIRED_USE
> > > > > check ?
> > > > 
> > > > It can't happen. If you can apply all the constraints, then
> > > > implicitly REQUIRED_USE is satisfied. If you can't apply all the
> > > > constraints, then it just fails. Of course, we want to ultimately
> > > > avoid that case.  
> > > 
> > > See the php example above. How do you ensure this does not happen?
> > > 
> > > Note that your assertion 'If you can apply all the constraints, then
> > > implicitly REQUIRED_USE is satisfied.' is false: You're changing the
> > > values of useflags, thus might violate some previously checked
> > > constraint.  
> > 
> > So you reiterate. Either you reach a solution (preferably there's only
> > a single valid solution you can reach) or you hit a previous state
> > which indicates a loop and you fail.
> 
> 
> So, PM, for every ebuild, will need to store the (at most) 2^n states it
> has already seen while trying to solve REQUIRED_USE and iterate until
> it cannot proceed anymore or falls into a previous state (so that's 2^n
> time too). That way we go from a linear time & linear space algorithm
> to one in exponential time & space. That's probably not a good idea.

I don't think that's actually going to happen. You'd have to try really
hard to get over n-1 iterations. I mean, the only simple way I can think
of is:

  b? ( a ) c? ( b ) d? ( c ) e? ( d ) ...

and this only means n-1 iterations. Can you think of a better way to
force multiple iterations that can be written without making
REQUIRED_USE completely unreadable? How likely is that going to happen
accidentally?

> I think it's better to limit the number of iterations to some constant.
> I'd say 1, then fail if REQUIRED_USE is still not satisfied. Maybe 2 or
> 3 can be useful but I think it'd be much harder to provide automated
> checks for that and much harder for ebuild writers to understand what
> will happen with the REQUIRED_USE they're about to write.
> 

Well, I don't mind setting that. All my tests (that weren't deliberately
abusing the algorithm) were able to finish in a single iteration. 2 or 3
should probably be safe for all the reasonable uses. However, if we're
not going to verify all possible values on repoman side, I think it
would be better to have a larger limit for users, to not have things
explode on them unnecessarily.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Michał Górny]

On pią, 2017-06-02 at 13:18 +0200, Alexis Ballier wrote:
> On Fri, 02 Jun 2017 08:37:30 +0200
> Michał Górny  wrote:
> 
> > On czw, 2017-06-01 at 23:31 +0200, Michał Górny wrote:
> > > On czw, 2017-06-01 at 10:55 +0200, Alexis Ballier wrote:  
> > > > On Wed, 31 May 2017 21:02:24 +0200
> > > > Michał Górny  wrote:
> > > >   
> > > > > On śro, 2017-05-31 at 19:39 +0200, Alexis Ballier wrote:  
> > > > > > > >  Again, you *need* to process the constraints in order.
> > > > > > > > '!a? ( b ) !b? ( a )' is not deterministic when none of a
> > > > > > > > and b are enabled otherwise.  
> > > > > > > 
> > > > > > > You can't rely on any particular order of constraints,
> > > > > > > especially when eclass stacking comes into play. You could
> > > > > > > try defining some constraint- sorting algorithm but it's
> > > > > > > going to be complex and it's usefulness will be limited
> > > > > > > anyway due to various kinds of grouping.
> > > > > > 
> > > > > > 
> > > > > > Better have some order: If half of the above constraint comes
> > > > > > from ebuild and the other half comes from eclass, then PM
> > > > > > might toggle 'a' or 'b' depending on the phase of the moon
> > > > > > which is specifically what we're trying to avoid.
> > > > > 
> > > > > No, it can't. That's the whole point. The algorithm must be
> > > > > defined so that it is always predictable independently of order
> > > > > (maybe except the ordering inside ^^, ||, ??) and independently
> > > > > of how it's nested (i.e. 'a? ( b? ( c ) )' must give the same
> > > > > result as 'b? ( a? ( c ) )').  
> > > > 
> > > > This is a lot of handwaving without real description of how it
> > > > would work. This starts to look a lot like confluence in
> > > > rewriting systems and you want developers to write only confluent
> > > > rules and repoman to decide that. Good luck with that.  
> > > 
> > > I'm sorry, what I said was quite stupid. I did some thinking and
> > > testing today, and the algorithm can be actually quite trivial. The
> > > real issue is getting a correct input, that is REQUIRED_USE
> > > constraints that have only one solution.
> 
> Don't be sorry, it's not stupid actually. There are various ways to
> determinize how the constraints should be solved. Once that is defined,
> one just needs to apply the rules to the constraints to get a
> temptative solution, making the algorithm trivial, indeed. Depending on
> how you do actually determinize the whole thing can make ensuring
> uniqueness (or even the existence) of a solution quite a pain. That's
> where the trade-offs between ebuild writers wishes and solving the issue
> come into play. I see this long thread as a quite interesting
> discussion where we're trying to converge towards something that leaves
> the problem easily solvable without asking too much to ebuild writers.
> 
> [...]
> > > The biggest issue for me right now is to find a way to determine
> > > whether a particular REQUIRED_USE constraint can have only one
> > > solution, independently of the order of non-n-ary constraints.
> > > However, some of it can be easily eyeball-checked using a graph.
> > >   
> > 
> > Well, I've looked at it more and you were right. While keeping them
> > order-independent is a noble goal, it's not really feasible,
> > especially if we assume that n-ary constraints can be reordered. So I
> > think we can assume left-to-right ordering now (with multiple passes,
> > if necessary).
> 
> 
> There are ways to guarantee order-independence, your gtk+ answer in the
> previous email suggests one: At most one constraint solving rule can be
> applied in any situation; that's what you did by putting the ||
> under !xinerama. This is a quite extreme way to ensure confluence but
> that works. I've not thought too much about it but I think we'd lose
> too much in expressivity though.

For the xinerama rule, you may prefer the opposite rule, i.e.:

  !X? ( !xinerama )

If you did so, I can't think of a way to express it correctly while
preserving full allowance of reshifting ||. So yes, we'd lose too much.

One thing we lose is the ability to clearly check whether the constraint
'makes sense'. Previously, we could (at least theoretically) check
whether it has a single solution and complain otherwise. With left-to-
right, I don't see any way to tell the developer 'something stupid is
going to happen now, you probably meant something else'. But I guess
that's still an improvement over what we have now.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Thu, 01 Jun 2017 23:31:25 +0200
Michał Górny  wrote:
> My current code is on github [1]. It's ugly, slow and incomplete. It's
> merely a proof-of-concept and testing toy but still could give some
> clues.
> 
> [1]:https://github.com/mgorny/required-use


Nice work by the way. I've not looked much at the code but I've tried
it on a few examples and it worked well. Then I tried on the php
example and it didn't finish within 30 mins so I stopped it.

I think we should really try to find a sub-exponential solution to
this, I doubt there's anything that can be done if the only solution is
to enumerate all the possibilities.

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

[Alexis Ballier]

On Thu, 01 Jun 2017 23:31:25 +0200
Michał Górny  wrote:
[...]
> > There are probably dozens of ways to make that non deterministic.
> > Here's one: USE='-*'. Apply '|| ( cli cgi fpm apache2 embed phpdbg
> > )' last; this enables 'cli'. Since it's the last one, REQUIRED_USE
> > is not satisfied because of 'cli? ( ^^ ( readline libedit ) )'.
> > If you process it first, then you enable cli and readline and are
> > good.  
> 
> You just take a second iteration, and things fall into place. That's
> not a problem.
> 
> > > > Also, what happens if we applied all the constraints and
> > > > obtained some useflags setting that still fails REQUIRED_USE
> > > > check ?
> > > 
> > > It can't happen. If you can apply all the constraints, then
> > > implicitly REQUIRED_USE is satisfied. If you can't apply all the
> > > constraints, then it just fails. Of course, we want to ultimately
> > > avoid that case.  
> > 
> > See the php example above. How do you ensure this does not happen?
> > 
> > Note that your assertion 'If you can apply all the constraints, then
> > implicitly REQUIRED_USE is satisfied.' is false: You're changing the
> > values of useflags, thus might violate some previously checked
> > constraint.  
> 
> So you reiterate. Either you reach a solution (preferably there's only
> a single valid solution you can reach) or you hit a previous state
> which indicates a loop and you fail.


So, PM, for every ebuild, will need to store the (at most) 2^n states it
has already seen while trying to solve REQUIRED_USE and iterate until
it cannot proceed anymore or falls into a previous state (so that's 2^n
time too). That way we go from a linear time & linear space algorithm
to one in exponential time & space. That's probably not a good idea.

I think it's better to limit the number of iterations to some constant.
I'd say 1, then fail if REQUIRED_USE is still not satisfied. Maybe 2 or
3 can be useful but I think it'd be much harder to provide automated
checks for that and much harder for ebuild writers to understand what
will happen with the REQUIRED_USE they're about to write.

[...]

Alexis.

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

[Alexis Ballier]

On Fri, 02 Jun 2017 08:37:30 +0200
Michał Górny  wrote:

> On czw, 2017-06-01 at 23:31 +0200, Michał Górny wrote:
> > On czw, 2017-06-01 at 10:55 +0200, Alexis Ballier wrote:  
> > > On Wed, 31 May 2017 21:02:24 +0200
> > > Michał Górny  wrote:
> > >   
> > > > On śro, 2017-05-31 at 19:39 +0200, Alexis Ballier wrote:  
> > > > > > >  Again, you *need* to process the constraints in order.
> > > > > > > '!a? ( b ) !b? ( a )' is not deterministic when none of a
> > > > > > > and b are enabled otherwise.  
> > > > > > 
> > > > > > You can't rely on any particular order of constraints,
> > > > > > especially when eclass stacking comes into play. You could
> > > > > > try defining some constraint- sorting algorithm but it's
> > > > > > going to be complex and it's usefulness will be limited
> > > > > > anyway due to various kinds of grouping.
> > > > > 
> > > > > 
> > > > > Better have some order: If half of the above constraint comes
> > > > > from ebuild and the other half comes from eclass, then PM
> > > > > might toggle 'a' or 'b' depending on the phase of the moon
> > > > > which is specifically what we're trying to avoid.
> > > > 
> > > > No, it can't. That's the whole point. The algorithm must be
> > > > defined so that it is always predictable independently of order
> > > > (maybe except the ordering inside ^^, ||, ??) and independently
> > > > of how it's nested (i.e. 'a? ( b? ( c ) )' must give the same
> > > > result as 'b? ( a? ( c ) )').  
> > > 
> > > This is a lot of handwaving without real description of how it
> > > would work. This starts to look a lot like confluence in
> > > rewriting systems and you want developers to write only confluent
> > > rules and repoman to decide that. Good luck with that.  
> > 
> > I'm sorry, what I said was quite stupid. I did some thinking and
> > testing today, and the algorithm can be actually quite trivial. The
> > real issue is getting a correct input, that is REQUIRED_USE
> > constraints that have only one solution.

Don't be sorry, it's not stupid actually. There are various ways to
determinize how the constraints should be solved. Once that is defined,
one just needs to apply the rules to the constraints to get a
temptative solution, making the algorithm trivial, indeed. Depending on
how you do actually determinize the whole thing can make ensuring
uniqueness (or even the existence) of a solution quite a pain. That's
where the trade-offs between ebuild writers wishes and solving the issue
come into play. I see this long thread as a quite interesting
discussion where we're trying to converge towards something that leaves
the problem easily solvable without asking too much to ebuild writers.

[...]
> > The biggest issue for me right now is to find a way to determine
> > whether a particular REQUIRED_USE constraint can have only one
> > solution, independently of the order of non-n-ary constraints.
> > However, some of it can be easily eyeball-checked using a graph.
> >   
> 
> Well, I've looked at it more and you were right. While keeping them
> order-independent is a noble goal, it's not really feasible,
> especially if we assume that n-ary constraints can be reordered. So I
> think we can assume left-to-right ordering now (with multiple passes,
> if necessary).


There are ways to guarantee order-independence, your gtk+ answer in the
previous email suggests one: At most one constraint solving rule can be
applied in any situation; that's what you did by putting the ||
under !xinerama. This is a quite extreme way to ensure confluence but
that works. I've not thought too much about it but I think we'd lose
too much in expressivity though.

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

[Michał Górny]

On czw, 2017-06-01 at 23:31 +0200, Michał Górny wrote:
> On czw, 2017-06-01 at 10:55 +0200, Alexis Ballier wrote:
> > On Wed, 31 May 2017 21:02:24 +0200
> > Michał Górny  wrote:
> > 
> > > On śro, 2017-05-31 at 19:39 +0200, Alexis Ballier wrote:
> > > > > >  Again, you *need* to process the constraints in order. '!a?
> > > > > > ( b ) !b? ( a )' is not deterministic when none of a and b are
> > > > > > enabled otherwise.
> > > > > 
> > > > > You can't rely on any particular order of constraints, especially
> > > > > when eclass stacking comes into play. You could try defining some
> > > > > constraint- sorting algorithm but it's going to be complex and
> > > > > it's usefulness will be limited anyway due to various kinds of
> > > > > grouping.  
> > > > 
> > > > 
> > > > Better have some order: If half of the above constraint comes from
> > > > ebuild and the other half comes from eclass, then PM might toggle
> > > > 'a' or 'b' depending on the phase of the moon which is specifically
> > > > what we're trying to avoid.  
> > > 
> > > No, it can't. That's the whole point. The algorithm must be defined so
> > > that it is always predictable independently of order (maybe except
> > > the ordering inside ^^, ||, ??) and independently of how it's nested
> > > (i.e. 'a? ( b? ( c ) )' must give the same result as 'b? ( a? ( c )
> > > )').
> > 
> > This is a lot of handwaving without real description of how it would
> > work. This starts to look a lot like confluence in rewriting systems
> > and you want developers to write only confluent rules and repoman to
> > decide that. Good luck with that.
> 
> I'm sorry, what I said was quite stupid. I did some thinking and testing
> today, and the algorithm can be actually quite trivial. The real issue
> is getting a correct input, that is REQUIRED_USE constraints that have
> only one solution.
> 
> That is the whole problem I was signaling, and which I seem to have lost
> sight of: solving is trivial, ensuring that the constraint can have only
> one solution isn't. Hopefully, most of the simple constraints in use
> will 'just work'.
> 
> The biggest issue for me right now is to find a way to determine whether
> a particular REQUIRED_USE constraint can have only one solution,
> independently of the order of non-n-ary constraints. However, some of it
> can be easily eyeball-checked using a graph.
> 

Well, I've looked at it more and you were right. While keeping them
order-independent is a noble goal, it's not really feasible, especially
if we assume that n-ary constraints can be reordered. So I think we can
assume left-to-right ordering now (with multiple passes, if necessary).

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Michał Górny]

On czw, 2017-06-01 at 20:17 -0500, A. Wilcox wrote:
> unpopular, unwanted opinion:
> 
> just have users of a *source based distro* where the emphasis is
> *choice* actually choose what they want?
> 
> What is the big deal with the way REQUIRED_USE works now?  "Users have
> to do something".  You always have to do something when you run
> source-based distros.  If they don't want to do something, don't run a
> distro that is source-based.  Gentoo being about choice necessitates
> knowledge about the choices you make before you make them.  It will
> never be truly "user friendly" for the noob set.  And that's fine, and
> that's where "friendly" forks like Sabayon and CoreOS and Adélie come in

So you don't mind having to manually adjust PYTHON_TARGETS for ~150
packages? Then keep those adjustments in line when upgrading to a newer
version of Python?

I understand that some people just have infinite amounts of time to do
something non-constructive but some of the people would like to just be
able to install/upgrade Gentoo without solving 50 different conflicts
each time.

> For the SSL/provider thing, I suggest just doing a DEPEND=ssl? (
> virtual/ssl ) where that is provided by openssl or libressl.  If a
> package doesn't support both, just DEPEND=ssl? ( whichever one it does
> support ).  [I actually suggested this some time ago, but was ignored
> there, too.]

Those are not drop-in replacements. They are ABI-compatible. If you go
down the virtual path, the switch becomes a complete and irreversible
breakage of everything linking to them, without even lightest clue what
to rebuild. Enjoy.

> But hey, I'm not a Gentoo dev, so I really don't have a voice here. :)
> 

Yet you voice your opinion without trying to understand the problems.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[A. Wilcox]

-BEGIN PGP SIGNED MESSAGE-
Hash: SHA256

On 01/06/17 20:28, Rich Freeman wrote:
> On Thu, Jun 1, 2017 at 9:17 PM, A. Wilcox 
> wrote:
>> 
>> just have users of a *source based distro* where the emphasis is 
>> *choice* actually choose what they want?
>> 
>> What is the big deal with the way REQUIRED_USE works now?  "Users
>> have to do something".
> 
> This is pretty analogous to the current situation with USE flags.
> I have wine installed.  Therefore I am constantly having portage
> add 32-bit ABI flags to my use config, even though I really don't
> do anything other than merge its suggestions.  If I had ever put
> anything in the config file that wasn't there just to make packages
> like wine happy I'd never know as the file is insane now.  Maybe
> some of those use dependencies no longer apply - doesn't matter,
> portage will keep building those packages 32-bit because it thinks
> I actually care about that.

hmm, good point.  I hadn't considered abi_x86_32 since I gave up on
WINE and Skype.

The motivation section that started this thread especially called out
the openssl/libressl thing as the terrible thing and that's why I
thought this would be much easier to just solve with virtuals.
Thinking harder about things like python_targets_python2_7 (trying to
go py3 clean except on packages that won't is a *drag*) and
abi_x86_32, this thread has a point.

Carry on!  Sorry for the noise.

- --arw

- -- 
A. Wilcox (awilfox)
Project Lead, Adélie Linux
http://adelielinux.org
-BEGIN PGP SIGNATURE-
Version: GnuPG v2

iQIcBAEBCAAGBQJZMMBXAAoJEMspy1GSK50UFLsP/3jxN3s/iXOy1DfzUt5eUnUS
rvv5yc46bDW54x6gWf76+nJjbAaoJOgeBmHIapo2tytxEXJM/NlEuyQiLWoypziz
sgm/vwLfBGQlXU9EVNzP7CusTH1CLz5qj4mtuhE5iCRh8Ktj8EnU3byI1unaA2yt
TtkR5z1ojwdzulwg/opxnJcxmZtxE1DjJMuP6xMJVKY5D5jH487JKKzKWttLJ70f
0Kds4Pxa8Lfek/ItynKsoVAEbnjPl26bDQ4gA3gVM0MsKIuJnsrIpzPUKQFIUz2a
jg81pJRk7d1NTlzCF+BDWpCDnsIgSdN2xWh9/fBkiQH1htxoBT5wy9sg+LZe/Z5u
er77ScIYGoOu1lH3kVWLOivTYxFyEJ5NXVHfDN8DQaHdM2wGl6C3gRqg3u/qAj+m
jGY8Tdj/pYFaHL6+l1gR6ViF562K3HKhAd+zjLPk3vWxO7j6SMRCelukmKy0G8yg
+k1S5MTjOW3rPZXAcoGoVj3mMqoRzIzs2OXcuAWAZNZu7lSGQ+TIkEOXqzQ41ZUz
z+yjiq2HjuIy+xVhXmcnYTurJi41F6DAQyz172btNstlk2gtget4iqEP85DDv3kF
GxoriSEmtTvfLyYS2PpzpaaPhUISysrjtOryhN13CpZ6sCcBbfRGVZGu8X2/TRNg
EHuak23KYEtGWdnyXe+D
=wbnO
-END PGP SIGNATURE-

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

[Rich Freeman]

On Thu, Jun 1, 2017 at 9:17 PM, A. Wilcox  wrote:
>
> just have users of a *source based distro* where the emphasis is
> *choice* actually choose what they want?
>
> What is the big deal with the way REQUIRED_USE works now?  "Users have
> to do something".

The issue is that there isn't any value being added by what the user
is doing if there is basically just one way to satisfy a constraint,
or often even if there are multiple ways.

Imagine if portage simply refused to install any package unless it was
in @world.  When you type emerge vim it would spit out a long list of
missing dependencies.  Then you'd add those to your @world and try
again.  Your @world would have 800 packages in it.  When you no longer
need a package you would uninstall it, but all the dependencies would
remain.

This is pretty analogous to the current situation with USE flags.  I
have wine installed.  Therefore I am constantly having portage add
32-bit ABI flags to my use config, even though I really don't do
anything other than merge its suggestions.  If I had ever put anything
in the config file that wasn't there just to make packages like wine
happy I'd never know as the file is insane now.  Maybe some of those
use dependencies no longer apply - doesn't matter, portage will keep
building those packages 32-bit because it thinks I actually care about
that.

This isn't about overriding user choice.  If you don't want X11
support you can set USE=-X and that is fine.  However, if you don't
care one way or another, why badger the user to make choices?  We
already have package USE defaults for just this reason.

Source based distros aren't about making users micromanage their
configuration for the sake of doing so.  You might as well do Linux
>From Scratch if you want that.  Our goal is to enable you to make the
choices you actually care about, but then take care of the rest for
you.


-- 
Rich

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

[A. Wilcox]

-BEGIN PGP SIGNED MESSAGE-
Hash: SHA256

unpopular, unwanted opinion:

just have users of a *source based distro* where the emphasis is
*choice* actually choose what they want?

What is the big deal with the way REQUIRED_USE works now?  "Users have
to do something".  You always have to do something when you run
source-based distros.  If they don't want to do something, don't run a
distro that is source-based.  Gentoo being about choice necessitates
knowledge about the choices you make before you make them.  It will
never be truly "user friendly" for the noob set.  And that's fine, and
that's where "friendly" forks like Sabayon and CoreOS and Adélie come in
.

I don't really want to see Portage's code base bloated with even
another solver that is poorly defined (and worse, this one would make
it in to PMS) just because users want to be lazy and Gentoo devs want
to enable laziness.

For the SSL/provider thing, I suggest just doing a DEPEND=ssl? (
virtual/ssl ) where that is provided by openssl or libressl.  If a
package doesn't support both, just DEPEND=ssl? ( whichever one it does
support ).  [I actually suggested this some time ago, but was ignored
there, too.]

But hey, I'm not a Gentoo dev, so I really don't have a voice here. :)

- --arw

- -- 
A. Wilcox (awilfox)
Project Lead, Adélie Linux
http://adelielinux.org
-BEGIN PGP SIGNATURE-
Version: GnuPG v2

iQIcBAEBCAAGBQJZMLy/AAoJEMspy1GSK50Uxd4QAIgieHNztCMC0R4z4++QGDO5
8j6uITVKoCP7wKpVZ2Dm8r0g2EbVBH+zy+Kz3Mbum8agaosoG6oW1mj66S2TjpX8
C8OokXVjhQuuddiDiZo2jXN5SABs/LLvkrElDVNdiGSluyfz/0V2I+OcXz40CrQv
KjZA4LWIavOK8FhX8PzPydwtDbS9YPBuDKE2vdK9A5+raleKZvjlhLw3PF1yDqlc
k1slBy20Wg5WtA0L1lo+ugZbLSrR5wmzBqji24Vh7pTariSV8nMhbAKiEVOY3PZ8
bEJdCahSO45Z9HJHfW6rxfVHPDWwCXw2JRjL4H9ixY3m96Za6KRNc1K/2KOOgI9D
0zyI2O+vtBrHmQJ9QiXsQ8c11MwYqz//2APCTuIwV8qjvKQTQBvQQRibYlZCRGJ7
8pBMrryd8TmtVcbN+aLzZcn1Z0K1lmM42zZxg1070C72VidJJOi4WqfO7/vWoMzQ
m5TlUqd/vFLB5UidCND5KD9GDhiVQBl8DSJlENwaPGLgIqxGbzx6A/gxh80+TC4Q
+SiKiQ/et87WVbZxNwx7/j5RATAlfZwMLvMVibjcwc+RKbx4JrOI2eaj/IOEMM8T
suYiHN2Q63HWjZXj59o9Jo/5uzhE2Ygd6VlyCQPvAgbfe8gWOTsXtMat03FSkkb0
2Z1+N5nnCdWSMLLSvNBN
=Rxfe
-END PGP SIGNATURE-

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

[Michał Górny]

On czw, 2017-06-01 at 10:55 +0200, Alexis Ballier wrote:
> On Wed, 31 May 2017 21:02:24 +0200
> Michał Górny  wrote:
> 
> > On śro, 2017-05-31 at 19:39 +0200, Alexis Ballier wrote:
> > > > >  Again, you *need* to process the constraints in order. '!a?
> > > > > ( b ) !b? ( a )' is not deterministic when none of a and b are
> > > > > enabled otherwise.
> > > > 
> > > > You can't rely on any particular order of constraints, especially
> > > > when eclass stacking comes into play. You could try defining some
> > > > constraint- sorting algorithm but it's going to be complex and
> > > > it's usefulness will be limited anyway due to various kinds of
> > > > grouping.  
> > > 
> > > 
> > > Better have some order: If half of the above constraint comes from
> > > ebuild and the other half comes from eclass, then PM might toggle
> > > 'a' or 'b' depending on the phase of the moon which is specifically
> > > what we're trying to avoid.  
> > 
> > No, it can't. That's the whole point. The algorithm must be defined so
> > that it is always predictable independently of order (maybe except
> > the ordering inside ^^, ||, ??) and independently of how it's nested
> > (i.e. 'a? ( b? ( c ) )' must give the same result as 'b? ( a? ( c )
> > )').
> 
> This is a lot of handwaving without real description of how it would
> work. This starts to look a lot like confluence in rewriting systems
> and you want developers to write only confluent rules and repoman to
> decide that. Good luck with that.

I'm sorry, what I said was quite stupid. I did some thinking and testing
today, and the algorithm can be actually quite trivial. The real issue
is getting a correct input, that is REQUIRED_USE constraints that have
only one solution.

That is the whole problem I was signaling, and which I seem to have lost
sight of: solving is trivial, ensuring that the constraint can have only
one solution isn't. Hopefully, most of the simple constraints in use
will 'just work'.

The biggest issue for me right now is to find a way to determine whether
a particular REQUIRED_USE constraint can have only one solution,
independently of the order of non-n-ary constraints. However, some of it
can be easily eyeball-checked using a graph.

> Let's look at real world examples:
> gtk+:
> 
> REQUIRED_USE="
> || ( aqua wayland X )
> xinerama? ( X )
> "

$ ./solve.py '|| ( aqua wayland X ) xinerama? ( X )'
[!wayland? => [!X? => [aqua]], xinerama? => [X]]

   x x
 w i   w i
 a n   a n
 y e   y e
   a l r a l r
   q a a q a a
   u n m u n m
 X a d a | X a d a
 0 0 0 0 | 0 1 0 0
 0 0 0 1 | 1 1 0 1
 0 0 1 0 | 0 0 1 0 (==)
 0 0 1 1 | 1 0 1 1
 0 1 0 0 | 0 1 0 0 (==)
 0 1 0 1 | 1 1 0 1
 0 1 1 0 | 0 1 1 0 (==)
 0 1 1 1 | 1 1 1 1
 1 0 0 0 | 1 0 0 0 (==)
 1 0 0 1 | 1 0 0 1 (==)
 1 0 1 0 | 1 0 1 0 (==)
 1 0 1 1 | 1 0 1 1 (==)
 1 1 0 0 | 1 1 0 0 (==)
 1 1 0 1 | 1 1 0 1 (==)
 1 1 1 0 | 1 1 1 0 (==)
 1 1 1 1 | 1 1 1 1 (==)

> 
> Let's assume aqua is masked, which reduces to:
> REQUIRED_USE="
> || ( wayland X )
> xinerama? ( X )
> "

$ ./solve.py '|| ( aqua wayland X ) xinerama? ( X )' '!aqua'
[!X? => [!aqua? => [wayland]], xinerama? => [X]]

   x x
 w i   w i
 a n   a n
 y e   y e
   a l r a l r
   q a a q a a
   u n m u n m
 X a d a | X a d a
 0 0 0 0 | 0 0 1 0
 0 0 0 1 | 1 0 1 1
 0 0 1 0 | 0 0 1 0 (==)
 0 0 1 1 | 1 0 1 1
 1 0 0 0 | 1 0 0 0 (==)
 1 0 0 1 | 1 0 0 1 (==)
 1 0 1 0 | 1 0 1 0 (==)
 1 0 1 1 | 1 0 1 1 (==)

(to avoid having to explicitly play with empty clauses and such, it
doesn't remove masked flags, just shifts them to the end)

> 
> With USE='-* xinerama' this one is invalid: applying the first
> constraint first enables wayland, then the 2nd enables X, giving a
> result of USE="xinerama wayland X". Applying the 2nd first enables X,
> then the 1st does nothing, giving a result of USE="xinerama X".

Indeed. To regain order-indepedence, you could do:

  xinerama? ( X ) !xinerama? ( || ( aqua wayland X ) )

While it's non-obvious, it's the only reasonable way to ensure that
things don't start falling apart randomly.

> Now the funny one:
> $ portageq metadata / ebuild dev-lang/php-7.0.18 REQUIRED_USE
> cli? ( ^^ ( readline libedit ) ) truetype? ( gd ) webp? ( gd ) cjk?
> ( gd ) exif? ( gd ) xpm? ( gd ) gd? ( zlib ) simplexml? ( xml ) soap?
> ( xml ) wddx? ( xml ) xmlrpc? ( || ( xml iconv ) ) xmlreader? ( xml )
> xslt? ( xml ) ldap-sasl? ( ldap ) mhash? ( hash ) phar? ( hash ) qdbm?
> ( !gdbm ) readline? ( !libedit ) recode? ( !imap !mysqli ) sharedmem?
> ( !threads ) mysql? ( || ( mysqli pdo ) ) || ( cli cgi fpm apache2
> embed phpdbg )

It isn't as scary as it looks. If you graph it, then you can notice it's
just got a few separate sub-graphs:

1. [!cgi, !fpm, !phpdbg, !apache2, !embed] -> cli -> (readline <=> !libedit)

(the last bit having duplicate 'readline? ( !libedit )' which is wrong)

2. [truetype, webp, cjk, exif, xpm] -> 

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

[Alexis Ballier]

On Wed, 31 May 2017 21:02:24 +0200
Michał Górny  wrote:

> On śro, 2017-05-31 at 19:39 +0200, Alexis Ballier wrote:
> > > >  Again, you *need* to process the constraints in order. '!a?
> > > > ( b ) !b? ( a )' is not deterministic when none of a and b are
> > > > enabled otherwise.
> > > 
> > > You can't rely on any particular order of constraints, especially
> > > when eclass stacking comes into play. You could try defining some
> > > constraint- sorting algorithm but it's going to be complex and
> > > it's usefulness will be limited anyway due to various kinds of
> > > grouping.  
> > 
> > 
> > Better have some order: If half of the above constraint comes from
> > ebuild and the other half comes from eclass, then PM might toggle
> > 'a' or 'b' depending on the phase of the moon which is specifically
> > what we're trying to avoid.  
> 
> No, it can't. That's the whole point. The algorithm must be defined so
> that it is always predictable independently of order (maybe except
> the ordering inside ^^, ||, ??) and independently of how it's nested
> (i.e. 'a? ( b? ( c ) )' must give the same result as 'b? ( a? ( c )
> )').

This is a lot of handwaving without real description of how it would
work. This starts to look a lot like confluence in rewriting systems
and you want developers to write only confluent rules and repoman to
decide that. Good luck with that.

Let's look at real world examples:
gtk+:

REQUIRED_USE="
|| ( aqua wayland X )
xinerama? ( X )
"

Let's assume aqua is masked, which reduces to:
REQUIRED_USE="
|| ( wayland X )
xinerama? ( X )
"

With USE='-* xinerama' this one is invalid: applying the first
constraint first enables wayland, then the 2nd enables X, giving a
result of USE="xinerama wayland X". Applying the 2nd first enables X,
then the 1st does nothing, giving a result of USE="xinerama X".


Now the funny one:
$ portageq metadata / ebuild dev-lang/php-7.0.18 REQUIRED_USE
cli? ( ^^ ( readline libedit ) ) truetype? ( gd ) webp? ( gd ) cjk?
( gd ) exif? ( gd ) xpm? ( gd ) gd? ( zlib ) simplexml? ( xml ) soap?
( xml ) wddx? ( xml ) xmlrpc? ( || ( xml iconv ) ) xmlreader? ( xml )
xslt? ( xml ) ldap-sasl? ( ldap ) mhash? ( hash ) phar? ( hash ) qdbm?
( !gdbm ) readline? ( !libedit ) recode? ( !imap !mysqli ) sharedmem?
( !threads ) mysql? ( || ( mysqli pdo ) ) || ( cli cgi fpm apache2
embed phpdbg )



There are probably dozens of ways to make that non deterministic.
Here's one: USE='-*'. Apply '|| ( cli cgi fpm apache2 embed phpdbg )'
last; this enables 'cli'. Since it's the last one, REQUIRED_USE is not
satisfied because of 'cli? ( ^^ ( readline libedit ) )'.
If you process it first, then you enable cli and readline and are good.

> If you start relying on stuff like ordering, you're one step from
> making stuff suddenly fail or change meaning due to minor changes,
> like sorting stuff.

What we want to ensure is that for 2 identical inputs the results are
identical. If ordering is specified, then re-ordering REQUIRED_USE in
an ebuild is not minor anymore. That's a trade off.


> > eclass stacking is not a problem: specify if it's append or prepend
> > and be done.  
> 
> What about multiple inherits with guards? Next thing I know, we end up
> putting REQUIRED_USE outside guards (like we have to do with
> EXPORT_FUNCTIONS now) because you need a specific order, and guards
> make it unpredictable.

guards wont make much of a difference: They'll simply de-duplicate
constraints by keeping only the rightmost one in the prepend case and
the leftmost one in the append case I think.

> > Note that if you want to remove the need for an order, you'll need
> > to ensure that all orderings of the constraints give the same
> > result. It's not sufficient to "only" check all possible inputs.  
> 
> That's the matter of the algorithm.

For what I know, this algorithm does not even exist.

> > Also, what happens if we applied all the constraints and obtained
> > some useflags setting that still fails REQUIRED_USE check ?  
> 
> It can't happen. If you can apply all the constraints, then implicitly
> REQUIRED_USE is satisfied. If you can't apply all the constraints,
> then it just fails. Of course, we want to ultimately avoid that case.

See the php example above. How do you ensure this does not happen?

Note that your assertion 'If you can apply all the constraints, then
implicitly REQUIRED_USE is satisfied.' is false: You're changing the
values of useflags, thus might violate some previously checked
constraint.


> > > The point would be: by definition, the solver should be able to
> > > touch *any* USE flag. If it can't, it mostly implies that you
> > > can't use the automatic solver, and so the case is irrelevant for
> > > checking. Attempting to go beyond that is going to give a lot of
> > > complexity and most likely kill the whole idea.
> > > 
> > > One thing we need to worry about are masks. We need to think about
> > > them.  
> > 
> > It makes zero 

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

[Ciaran McCreesh]

On Wed, 31 May 2017 21:02:24 +0200
Michał Górny  wrote:
> No, it can't. That's the whole point. The algorithm must be defined so
> that it is always predictable independently of order

So what's this mysterious algorithm then?

-- 
Ciaran McCreesh

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

[Michał Górny]

On śro, 2017-05-31 at 19:39 +0200, Alexis Ballier wrote:
> > >  Again, you *need* to process the constraints in order. '!a?
> > > ( b ) !b? ( a )' is not deterministic when none of a and b are
> > > enabled otherwise.  
> > 
> > You can't rely on any particular order of constraints, especially when
> > eclass stacking comes into play. You could try defining some
> > constraint- sorting algorithm but it's going to be complex and it's
> > usefulness will be limited anyway due to various kinds of grouping.
> 
> 
> Better have some order: If half of the above constraint comes from
> ebuild and the other half comes from eclass, then PM might toggle 'a' or
> 'b' depending on the phase of the moon which is specifically what we're
> trying to avoid.

No, it can't. That's the whole point. The algorithm must be defined so
that it is always predictable independently of order (maybe except
the ordering inside ^^, ||, ??) and independently of how it's nested
(i.e. 'a? ( b? ( c ) )' must give the same result as 'b? ( a? ( c ) )').

If you start relying on stuff like ordering, you're one step from making
stuff suddenly fail or change meaning due to minor changes, like sorting
stuff.

> eclass stacking is not a problem: specify if it's append or prepend and
> be done.

What about multiple inherits with guards? Next thing I know, we end up
putting REQUIRED_USE outside guards (like we have to do with
EXPORT_FUNCTIONS now) because you need a specific order, and guards make
it unpredictable.

> Note that if you want to remove the need for an order, you'll need to
> ensure that all orderings of the constraints give the same result. It's
> not sufficient to "only" check all possible inputs.

That's the matter of the algorithm.

> Also, what happens if we applied all the constraints and obtained some
> useflags setting that still fails REQUIRED_USE check ?

It can't happen. If you can apply all the constraints, then implicitly
REQUIRED_USE is satisfied. If you can't apply all the constraints, then
it just fails. Of course, we want to ultimately avoid that case.

> > The point would be: by definition, the solver should be able to touch
> > *any* USE flag. If it can't, it mostly implies that you can't use
> > the automatic solver, and so the case is irrelevant for checking.
> > Attempting to go beyond that is going to give a lot of complexity
> > and most likely kill the whole idea.
> > 
> > One thing we need to worry about are masks. We need to think about
> > them.
> 
> It makes zero difference for any solver if you replace variables
> (useflags) by 'true' or 'false' constants (masked/forced/user-forced
> useflags). It's even simpler actually. Whether the formula is not
> constantly 'true' (ie REQUIRED_USE is useless) or constantly
> 'false' (ie there's no way to solve it) is equivalent to solving SAT.
> We likely don't want that for repoman running on php.
> 

Well, probably yes. We just need to make sure to apply them correctly
in different contexts, to avoid accidentally skipping some constraints.
I think it would be reasonably to assume that:

a. flags masked/forced on LHS of implications (foo?) are evaluated
in place, i.e. either always require RHS or remove it completely:

  foo? ( bar )-> with foo forced, bar is always required
  => we should also force bar

b. flags masked/forced inside ^^, ??, || alter the contents/meaning --
in particular they might replace the whole construct with a single flag
or make it unsolvable:

  ^^ ( foo bar baz ) -> with foo forced, [bar baz] are never allowed
 => we should mask them

  || ( foo bar baz ) -> with foo forced, the constraint can be skipped

c. flags masked/forced otherwise can't be altered:

  foo? ( bar )-> with bar forced, we can skip the constraint.
  -> with bar masked, foo should be masked as well

Does that cover all the contexts?

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Wed, 31 May 2017 15:04:52 +0200
Michał Górny  wrote:

> On śro, 2017-05-31 at 10:38 +0200, Alexis Ballier wrote:
> > > > What if I specifically set USE=-bar in make.conf ? Do we really
> > > > want PM to override that without telling me ?
> > > 
> > > Yes. Unless you specifically and explicitly disable that
> > > (globally or for USE=bar), in which case the PM would just reject
> > > to proceed.  
> > 
> > 
> > Then could you please explain how to get the list of useflags the
> > solver is allowed to toggle ? Preferably in a PMS-friendly way (aka
> > no USE=foo emerge). It's not clear to me what this would be and is
> > mandatory for determinism.
> > 
> > Note that most definitions are acceptable, but there must be one.  
> 
> If we *really* want to set this for the users, it would simply be
> a variable defined in make.profile, e.g.:
> 
>   REQUIRED_USE_STRICT="foo bar"
> 
> which would mean the solver is globally forbidden from touching those
> flags, i.e. if the solution would involve touching them, PM must fail
> and request user to manually resolve it.
> 
> However, as far as I'm concerned we'd be good at keeping this purely
> as user configuration, alike FEATURES=i-do-not-want-automatic-solving.

Ok, why not.

> > > > I believe that, from the ebuild POV, the ternary useflag model
> > > > is more appropriate: You have a whole bunch of ways to specify
> > > > useflags with portage (make.conf, package.use, profiles, command
> > > > line, ...). From the ebuild those are collapsed into 'user
> > > > input'. You only have IUSE (with its defaults) and that's what
> > > > the auto-solver should play with: those are the flags that can
> > > > be toggled.
> > > 
> > > I see your point. However, it's merely a preference problem and we
> > > really don't want the constraints to become ternary and/or PM try
> > > to force the reverse solutions. That's an easy way to lose
> > > predictability.  
> > 
> > They're not ternary anymore after processing ebuild: IUSE="foo +bar"
> > means instantiate foo as -foo if not specified, and bar as +bar.
> > The way I see it, ternary model is useful in the sense that the 3rd
> > undefined state is what the solver can toggle, the others are fixed
> > (either by user input or e.g. use.mask).
> > 
> > Basically, I see automatic solving of REQUIRED_USE as dynamic IUSE
> > defaults. But see above, this might not be the best way.  
> 
> I'm lost on what you're trying to achieve here. Maybe give a full run-
> out based on Portage behavior -- i.e. involving all the places USE
> flags can be altered in Portage, and how they're going to affect the
> result. Don't forget about USE_ORDER.

What I'm suggesting is: Flags that can be toggled are the same that
would be affected by IUSE defaults. Others are fixed and the
REQUIRED_USE formula is instantiated & reduced with those values. If
there is a contradiction already, fail hard. If not, apply the
algorithm to determine a set of IUSE defaults that would make it
work. Process the ebuild as if it had those IUSE default.

You seem to be going in another direction which is unclear to me.

[...]
> > > > > Now, this also means that every constraint that can't be
> > > > > solved in this easy fashion is invalid. We want to detect
> > > > > that, and warn the developer. Some of those could be tricky.
> > > > > Simple example:
> > > > > 
> > > > >   foo? ( baz ) bar? ( !baz )
> > > > > 
> > > > > This one is invalid because USE='foo bar' requires both 'baz'
> > > > > and '!baz' as a solution. Remember that we don't want to do
> > > > > any changes besides what's explicitly written there, no
> > > > > guessing.
> > > > 
> > > > Besides that, what makes it invalid ?
> > > 
> > > What makes it invalid is that you can't solve it in a predictable
> > > way.  
> > 
> > You can fail in a predictable way and ebuild writer can adjust it to
> > avoid that.  
> 
> If the point is to process constraints *automatically*, then failing
> is not the desired result. Yes, we can consider that a minor
> issue/warning level but it is still an issue. I named it 'invalid'
> because it prevents the automatic solving from working which is the
> purpose of this whole effort.

Ok. I was assuming we do not want to change anything user-specified.
When I set USE=foo, I want foo, not maybe foo. But why not: As you
noted this can be a PM feature and there's not much to be checked in
that case.

As for how to check that, it is still completely unclear to me if
there'd be anything better than enumerating all the possible inputs.


> >  Again, you *need* to process the constraints in order. '!a?
> > ( b ) !b? ( a )' is not deterministic when none of a and b are
> > enabled otherwise.  
> 
> You can't rely on any particular order of constraints, especially when
> eclass stacking comes into play. You could try defining some
> constraint- sorting algorithm but it's going to be complex and it's
> usefulness will be limited anyway due to various kinds 

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

[Michał Górny]

On śro, 2017-05-31 at 10:38 +0200, Alexis Ballier wrote:
> > > What if I specifically set USE=-bar in make.conf ? Do we really
> > > want PM to override that without telling me ?  
> > 
> > Yes. Unless you specifically and explicitly disable that (globally or
> > for USE=bar), in which case the PM would just reject to proceed.
> 
> 
> Then could you please explain how to get the list of useflags the
> solver is allowed to toggle ? Preferably in a PMS-friendly way (aka no
> USE=foo emerge). It's not clear to me what this would be and is
> mandatory for determinism.
> 
> Note that most definitions are acceptable, but there must be one.

If we *really* want to set this for the users, it would simply be
a variable defined in make.profile, e.g.:

  REQUIRED_USE_STRICT="foo bar"

which would mean the solver is globally forbidden from touching those
flags, i.e. if the solution would involve touching them, PM must fail
and request user to manually resolve it.

However, as far as I'm concerned we'd be good at keeping this purely as
user configuration, alike FEATURES=i-do-not-want-automatic-solving.

> > > I believe that, from the ebuild POV, the ternary useflag model is
> > > more appropriate: You have a whole bunch of ways to specify
> > > useflags with portage (make.conf, package.use, profiles, command
> > > line, ...). From the ebuild those are collapsed into 'user input'.
> > > You only have IUSE (with its defaults) and that's what the
> > > auto-solver should play with: those are the flags that can be
> > > toggled.  
> > 
> > I see your point. However, it's merely a preference problem and we
> > really don't want the constraints to become ternary and/or PM try to
> > force the reverse solutions. That's an easy way to lose
> > predictability.
> 
> They're not ternary anymore after processing ebuild: IUSE="foo +bar"
> means instantiate foo as -foo if not specified, and bar as +bar.
> The way I see it, ternary model is useful in the sense that the 3rd
> undefined state is what the solver can toggle, the others are fixed
> (either by user input or e.g. use.mask).
> 
> Basically, I see automatic solving of REQUIRED_USE as dynamic IUSE
> defaults. But see above, this might not be the best way.

I'm lost on what you're trying to achieve here. Maybe give a full run-
out based on Portage behavior -- i.e. involving all the places USE flags
can be altered in Portage, and how they're going to affect the result.
Don't forget about USE_ORDER.

> > Besides, I should point out that USE_EXPAND in make.profile
> > and make.conf are strictly binary.
> 
> Last I checked IUSE="+use_expand_foo use_expand_bar" worked just as
> useflags.

I'm talking about FOO="bar baz" form which implies -* for all remaining
values (and does not accept '-flag', unless I'm mistaken).

> 
> > > > Now, this also means that every constraint that can't be solved in
> > > > this easy fashion is invalid. We want to detect that, and warn the
> > > > developer. Some of those could be tricky. Simple example:
> > > > 
> > > >   foo? ( baz ) bar? ( !baz )
> > > > 
> > > > This one is invalid because USE='foo bar' requires both 'baz' and
> > > > '!baz' as a solution. Remember that we don't want to do any
> > > > changes besides what's explicitly written there, no guessing.  
> > > 
> > > Besides that, what makes it invalid ?  
> > 
> > What makes it invalid is that you can't solve it in a predictable way.
> 
> You can fail in a predictable way and ebuild writer can adjust it to
> avoid that.

If the point is to process constraints *automatically*, then failing is
not the desired result. Yes, we can consider that a minor issue/warning
level but it is still an issue. I named it 'invalid' because it prevents
the automatic solving from working which is the purpose of this whole
effort.

>  Again, you *need* to process the constraints in order. '!a?
> ( b ) !b? ( a )' is not deterministic when none of a and b are
> enabled otherwise.

You can't rely on any particular order of constraints, especially when
eclass stacking comes into play. You could try defining some constraint-
sorting algorithm but it's going to be complex and it's usefulness will
be limited anyway due to various kinds of grouping.

> You'll get a message like:
> "
>  The constraint bar? ( !baz )' is violated.
> bar is enabled because $reason (say, make.conf)
> baz is enabled because of the constraint 'foo? ( baz )'
> foo is enabled because $reason
> "

You = user or ebuild author? Because per my proposal, this construct
should result in QA error/warning, telling the ebuild writer to use
predictable constraints.

Of course, we could still accept the ebuild and just fail hard on user
side (alike REQUIRED_USE). But that's really getting out of scope.

> 
> > >  How is it more invalid than '?? ( foo bar )' ?  
> > 
> > This would go into:
> > 
> >   foo? ( !bar )
> 
> Just to be clear: Are you suggesting banning '??' from the syntax or
> simply an internal rewrite 

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

[Alexis Ballier]

On Wed, 31 May 2017 10:03:12 +0200
Michał Górny  wrote:

> On śro, 2017-05-31 at 09:32 +0200, Alexis Ballier wrote:
> > On Wed, 31 May 2017 08:55:17 +0200
> > Michał Górny  wrote:
> >   
> > > On wto, 2017-05-30 at 20:46 +0200, Alexis Ballier wrote:  
> > > > On Tue, 30 May 2017 20:11:38 +0200
> > > > Michał Górny  wrote:
> > > > [...]
> > > > > > > Of course, we could just validate all the possible cases
> > > > > > > via repoman, and reject the ebuild if there's at least one
> > > > > > > conflict between them. Not sure how to express that
> > > > > > > properly in the spec though. Not sure how it would work
> > > > > > > practically.  
> > > > > > 
> > > > > > Adding a 2^n check to repoman isn't gonna work well.
> > > > > >   
> > > > > 
> > > > > I'm not saying it's the most optimal algorithm of verifying
> > > > > the correctness of the constraints. It's just the one that's
> > > > > quite obvious -- relatively simple and reliable. If someone
> > > > > can come up with something better that covers at least the
> > > > > most common cases, I'm all for it.
> > > > > 
> > > > > That said, this wouldn't be that much of a problem if we can
> > > > > keep the n low. For a start, we can rule out all flags that
> > > > > don't appear in REQUIRED_USE at all. Furthermore, I think we
> > > > > could also ignore the constraints for flags that don't appear
> > > > > there at least 'twice', and so on.
> > > > 
> > > > :)
> > > > 
> > > > You're applying classical techniques to lower the size of a SAT
> > > > instance so that your exponential algorithm does not explode,
> > > > but it's still hard.
> > > > 
> > > > I'm not sure what you want: If you want to detect that there is
> > > > an impossible constraint, well, ebuild writer will notice soon
> > > > enough when testing it. If you want to detect that there is a
> > > > way to have a conflict between useflags, then there will be
> > > > valid cases where this will happen.
> > > > 
> > > > That said, assuming we have REQUIRED_USE in CNF form, its
> > > > negation is in DNF form. Solving SAT on DNF formulas is easy
> > > > (linear I think), and this would give you an assignment of
> > > > useflags triggering an impossible constraint. e.g. 'foo? ( bar
> > > > )' with USE='foo -bar' in make.conf. This could be used to
> > > > trigger a repoman warning but basically every single ebuild
> > > > would trigger those.
> > > 
> > > Not sure if we understand each other.
> > > 
> > > I'd like the constraints to be plain straightforward, to the
> > > point of having only one acceptable solution. No special
> > > Portage-style algorithms that attempt to provide a reasonable
> > > solution to unreasonable input, resulting in horrible solutions
> > > that need 20 more hacks every few months.  
> > 
> > Yes, we definitely agree here. For that, you need to kill the SAT
> > solver and define (spec) what is the straightforward solution, aka a
> > deterministic and straightforward (*) algorithm. Otherwise, you fall
> > into the problems Ciaran explained in an earlier email.
> > 
> > 
> > (*) It's better for the algorithm to be simple enough so that
> > REQUIRED_USE can be written easily for achieving a given behavior.
> > 
> >   
> > > For example:
> > > 
> > >   foo? ( bar )
> > > 
> > > would mean 'if you have USE=foo, then USE=bar is enabled as
> > > well'. Not 'find some random solution which satisfies this'. In
> > > other words, here changing USE=foo into USE=-foo is not an
> > > acceptable solution.  
> > 
> > 
> > What if I specifically set USE=-bar in make.conf ? Do we really
> > want PM to override that without telling me ?  
> 
> Yes. Unless you specifically and explicitly disable that (globally or
> for USE=bar), in which case the PM would just reject to proceed.


Then could you please explain how to get the list of useflags the
solver is allowed to toggle ? Preferably in a PMS-friendly way (aka no
USE=foo emerge). It's not clear to me what this would be and is
mandatory for determinism.

Note that most definitions are acceptable, but there must be one.

> > I believe that, from the ebuild POV, the ternary useflag model is
> > more appropriate: You have a whole bunch of ways to specify
> > useflags with portage (make.conf, package.use, profiles, command
> > line, ...). From the ebuild those are collapsed into 'user input'.
> > You only have IUSE (with its defaults) and that's what the
> > auto-solver should play with: those are the flags that can be
> > toggled.  
> 
> I see your point. However, it's merely a preference problem and we
> really don't want the constraints to become ternary and/or PM try to
> force the reverse solutions. That's an easy way to lose
> predictability.

They're not ternary anymore after processing ebuild: IUSE="foo +bar"
means instantiate foo as -foo if not specified, and bar as +bar.
The way I see it, ternary model is useful in the sense that the 3rd
undefined state 

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

[Michał Górny]

On śro, 2017-05-31 at 09:32 +0200, Alexis Ballier wrote:
> On Wed, 31 May 2017 08:55:17 +0200
> Michał Górny  wrote:
> 
> > On wto, 2017-05-30 at 20:46 +0200, Alexis Ballier wrote:
> > > On Tue, 30 May 2017 20:11:38 +0200
> > > Michał Górny  wrote:
> > > [...]  
> > > > > > Of course, we could just validate all the possible cases via
> > > > > > repoman, and reject the ebuild if there's at least one
> > > > > > conflict between them. Not sure how to express that properly
> > > > > > in the spec though. Not sure how it would work
> > > > > > practically.
> > > > > 
> > > > > Adding a 2^n check to repoman isn't gonna work well.
> > > > > 
> > > > 
> > > > I'm not saying it's the most optimal algorithm of verifying
> > > > the correctness of the constraints. It's just the one that's quite
> > > > obvious -- relatively simple and reliable. If someone can come up
> > > > with something better that covers at least the most common cases,
> > > > I'm all for it.
> > > > 
> > > > That said, this wouldn't be that much of a problem if we can keep
> > > > the n low. For a start, we can rule out all flags that don't
> > > > appear in REQUIRED_USE at all. Furthermore, I think we could also
> > > > ignore the constraints for flags that don't appear there at least
> > > > 'twice', and so on.  
> > > 
> > > :)
> > > 
> > > You're applying classical techniques to lower the size of a SAT
> > > instance so that your exponential algorithm does not explode, but
> > > it's still hard.
> > > 
> > > I'm not sure what you want: If you want to detect that there is an
> > > impossible constraint, well, ebuild writer will notice soon enough
> > > when testing it. If you want to detect that there is a way to have a
> > > conflict between useflags, then there will be valid cases where this
> > > will happen.
> > > 
> > > That said, assuming we have REQUIRED_USE in CNF form, its negation
> > > is in DNF form. Solving SAT on DNF formulas is easy (linear I
> > > think), and this would give you an assignment of useflags
> > > triggering an impossible constraint. e.g. 'foo? ( bar )' with
> > > USE='foo -bar' in make.conf. This could be used to trigger a
> > > repoman warning but basically every single ebuild would trigger
> > > those.  
> > 
> > Not sure if we understand each other.
> > 
> > I'd like the constraints to be plain straightforward, to the point of
> > having only one acceptable solution. No special Portage-style
> > algorithms that attempt to provide a reasonable solution to
> > unreasonable input, resulting in horrible solutions that need 20 more
> > hacks every few months.
> 
> Yes, we definitely agree here. For that, you need to kill the SAT
> solver and define (spec) what is the straightforward solution, aka a
> deterministic and straightforward (*) algorithm. Otherwise, you fall
> into the problems Ciaran explained in an earlier email.
> 
> 
> (*) It's better for the algorithm to be simple enough so that
> REQUIRED_USE can be written easily for achieving a given behavior.
> 
> 
> > For example:
> > 
> >   foo? ( bar )
> > 
> > would mean 'if you have USE=foo, then USE=bar is enabled as well'. Not
> > 'find some random solution which satisfies this'. In other words, here
> > changing USE=foo into USE=-foo is not an acceptable solution.
> 
> 
> What if I specifically set USE=-bar in make.conf ? Do we really want PM
> to override that without telling me ?

Yes. Unless you specifically and explicitly disable that (globally or
for USE=bar), in which case the PM would just reject to proceed.

> I believe that, from the ebuild POV, the ternary useflag model is more
> appropriate: You have a whole bunch of ways to specify useflags with
> portage (make.conf, package.use, profiles, command line, ...). From the
> ebuild those are collapsed into 'user input'. You only have IUSE (with
> its defaults) and that's what the auto-solver should play with: those
> are the flags that can be toggled.

I see your point. However, it's merely a preference problem and we
really don't want the constraints to become ternary and/or PM try to
force the reverse solutions. That's an easy way to lose predictability.

Besides, I should point out that USE_EXPAND in make.profile
and make.conf are strictly binary. Furthermore, the ternary idea starts
becoming blurry when you have to deal with profiles that you explicitly
want to disable in user configuration.

> > Now, this also means that every constraint that can't be solved in
> > this easy fashion is invalid. We want to detect that, and warn the
> > developer. Some of those could be tricky. Simple example:
> > 
> >   foo? ( baz ) bar? ( !baz )
> > 
> > This one is invalid because USE='foo bar' requires both 'baz' and
> > '!baz' as a solution. Remember that we don't want to do any changes
> > besides what's explicitly written there, no guessing.
> 
> Besides that, what makes it invalid ?

What makes it invalid is that you can't solve it in a predictable way.

> 

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

[Alexis Ballier]

On Wed, 31 May 2017 09:54:56 +0200
Alexis Ballier  wrote:

> On Wed, 31 May 2017 08:51:33 +0100
> Ciaran McCreesh  wrote:
> 
> > On Wed, 31 May 2017 09:35:04 +0200
> > Michał Górny  wrote:  
> > > On śro, 2017-05-31 at 08:24 +0100, Ciaran McCreesh wrote:
> > > > On Wed, 31 May 2017 08:55:17 +0200
> > > > Michał Górny  wrote:  
> > > > > For example:
> > > > > 
> > > > >   foo? ( bar )
> > > > > 
> > > > > would mean 'if you have USE=foo, then USE=bar is enabled as
> > > > > well'.  
> > > > 
> > > > What about "if bar cannot be enabled, then turn foo off"?
> > > 
> > > Not expressible. The best you can do is 'if bar is
> > > disabled, ...'
> > 
> > This is the kind of thing that gets very messy when a user wants ssl
> > enabled, and has to enable either openssl or libressl, and they're
> > on a profile where openssl is masked but the ebuild writer prefers
> > that option...
> >   
> 
> ssl? ( ^^ ( openssl libressl ) ) with openssl masked will be reduced
> to 'ssl? ( libressl )' so all good here.
> 

Note: that's also an argument for applying user input before trying to
solve anything. At the very least masks.

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

[Alexis Ballier]

On Wed, 31 May 2017 08:51:33 +0100
Ciaran McCreesh  wrote:

> On Wed, 31 May 2017 09:35:04 +0200
> Michał Górny  wrote:
> > On śro, 2017-05-31 at 08:24 +0100, Ciaran McCreesh wrote:  
> > > On Wed, 31 May 2017 08:55:17 +0200
> > > Michał Górny  wrote:
> > > > For example:
> > > > 
> > > >   foo? ( bar )
> > > > 
> > > > would mean 'if you have USE=foo, then USE=bar is enabled as
> > > > well'.
> > > 
> > > What about "if bar cannot be enabled, then turn foo off"?  
> > 
> > Not expressible. The best you can do is 'if bar is disabled, ...'  
> 
> This is the kind of thing that gets very messy when a user wants ssl
> enabled, and has to enable either openssl or libressl, and they're on
> a profile where openssl is masked but the ebuild writer prefers that
> option...
> 

ssl? ( ^^ ( openssl libressl ) ) with openssl masked will be reduced to
'ssl? ( libressl )' so all good here.

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

[Ciaran McCreesh]

On Wed, 31 May 2017 09:35:04 +0200
Michał Górny  wrote:
> On śro, 2017-05-31 at 08:24 +0100, Ciaran McCreesh wrote:
> > On Wed, 31 May 2017 08:55:17 +0200
> > Michał Górny  wrote:  
> > > For example:
> > > 
> > >   foo? ( bar )
> > > 
> > > would mean 'if you have USE=foo, then USE=bar is enabled as
> > > well'.  
> > 
> > What about "if bar cannot be enabled, then turn foo off"?
> 
> Not expressible. The best you can do is 'if bar is disabled, ...'

This is the kind of thing that gets very messy when a user wants ssl
enabled, and has to enable either openssl or libressl, and they're on a
profile where openssl is masked but the ebuild writer prefers that
option...

-- 
Ciaran McCreesh

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

[Michał Górny]

On śro, 2017-05-31 at 08:24 +0100, Ciaran McCreesh wrote:
> On Wed, 31 May 2017 08:55:17 +0200
> Michał Górny  wrote:
> > For example:
> > 
> >   foo? ( bar )
> > 
> > would mean 'if you have USE=foo, then USE=bar is enabled as well'.
> 
> What about "if bar cannot be enabled, then turn foo off"?
> 

Not expressible. The best you can do is 'if bar is disabled, ...'


-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Wed, 31 May 2017 08:24:20 +0100
Ciaran McCreesh  wrote:

> On Wed, 31 May 2017 08:55:17 +0200
> Michał Górny  wrote:
> > For example:
> > 
> >   foo? ( bar )
> > 
> > would mean 'if you have USE=foo, then USE=bar is enabled as well'.  
> 
> What about "if bar cannot be enabled, then turn foo off"?
> 

You ask a constructivist who'll yell at you saying that 'foo -> bar' is
not equivalent to '!bar -> !foo'. You'll have to write the latter as
well if you want that.

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

[Alexis Ballier]

On Wed, 31 May 2017 08:55:17 +0200
Michał Górny  wrote:

> On wto, 2017-05-30 at 20:46 +0200, Alexis Ballier wrote:
> > On Tue, 30 May 2017 20:11:38 +0200
> > Michał Górny  wrote:
> > [...]  
> > > > > Of course, we could just validate all the possible cases via
> > > > > repoman, and reject the ebuild if there's at least one
> > > > > conflict between them. Not sure how to express that properly
> > > > > in the spec though. Not sure how it would work
> > > > > practically.
> > > > 
> > > > Adding a 2^n check to repoman isn't gonna work well.
> > > > 
> > > 
> > > I'm not saying it's the most optimal algorithm of verifying
> > > the correctness of the constraints. It's just the one that's quite
> > > obvious -- relatively simple and reliable. If someone can come up
> > > with something better that covers at least the most common cases,
> > > I'm all for it.
> > > 
> > > That said, this wouldn't be that much of a problem if we can keep
> > > the n low. For a start, we can rule out all flags that don't
> > > appear in REQUIRED_USE at all. Furthermore, I think we could also
> > > ignore the constraints for flags that don't appear there at least
> > > 'twice', and so on.  
> > 
> > :)
> > 
> > You're applying classical techniques to lower the size of a SAT
> > instance so that your exponential algorithm does not explode, but
> > it's still hard.
> > 
> > I'm not sure what you want: If you want to detect that there is an
> > impossible constraint, well, ebuild writer will notice soon enough
> > when testing it. If you want to detect that there is a way to have a
> > conflict between useflags, then there will be valid cases where this
> > will happen.
> > 
> > That said, assuming we have REQUIRED_USE in CNF form, its negation
> > is in DNF form. Solving SAT on DNF formulas is easy (linear I
> > think), and this would give you an assignment of useflags
> > triggering an impossible constraint. e.g. 'foo? ( bar )' with
> > USE='foo -bar' in make.conf. This could be used to trigger a
> > repoman warning but basically every single ebuild would trigger
> > those.  
> 
> Not sure if we understand each other.
> 
> I'd like the constraints to be plain straightforward, to the point of
> having only one acceptable solution. No special Portage-style
> algorithms that attempt to provide a reasonable solution to
> unreasonable input, resulting in horrible solutions that need 20 more
> hacks every few months.

Yes, we definitely agree here. For that, you need to kill the SAT
solver and define (spec) what is the straightforward solution, aka a
deterministic and straightforward (*) algorithm. Otherwise, you fall
into the problems Ciaran explained in an earlier email.


(*) It's better for the algorithm to be simple enough so that
REQUIRED_USE can be written easily for achieving a given behavior.


> For example:
> 
>   foo? ( bar )
> 
> would mean 'if you have USE=foo, then USE=bar is enabled as well'. Not
> 'find some random solution which satisfies this'. In other words, here
> changing USE=foo into USE=-foo is not an acceptable solution.


What if I specifically set USE=-bar in make.conf ? Do we really want PM
to override that without telling me ?

I believe that, from the ebuild POV, the ternary useflag model is more
appropriate: You have a whole bunch of ways to specify useflags with
portage (make.conf, package.use, profiles, command line, ...). From the
ebuild those are collapsed into 'user input'. You only have IUSE (with
its defaults) and that's what the auto-solver should play with: those
are the flags that can be toggled.


> Now, this also means that every constraint that can't be solved in
> this easy fashion is invalid. We want to detect that, and warn the
> developer. Some of those could be tricky. Simple example:
> 
>   foo? ( baz ) bar? ( !baz )
> 
> This one is invalid because USE='foo bar' requires both 'baz' and
> '!baz' as a solution. Remember that we don't want to do any changes
> besides what's explicitly written there, no guessing.

Besides that, what makes it invalid ? How is it more invalid than '??
( foo bar )' ?

> However, the
> following should be valid:
> 
>   foo? ( baz ) bar? ( !foo !baz )
> 
> Because now we clearly indicate that USE=bar disables USE=foo,
> and therefore makes the first constraint inapplicable. It clearly
> indicates course of action for all combinations:

Ok, I now think you're aiming for giving full power to the solver,
overriding user inputs if necessary. Before going further, I think we
should first agree on what are the useflags such a solver can toggle.
I'm not sure 'USE=foo emerge blah' should disable foo instead of
failing for example.


Alexis.

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

[Ciaran McCreesh]

On Wed, 31 May 2017 08:55:17 +0200
Michał Górny  wrote:
> For example:
> 
>   foo? ( bar )
> 
> would mean 'if you have USE=foo, then USE=bar is enabled as well'.

What about "if bar cannot be enabled, then turn foo off"?

-- 
Ciaran McCreesh

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

[Michał Górny]

On wto, 2017-05-30 at 20:46 +0200, Alexis Ballier wrote:
> On Tue, 30 May 2017 20:11:38 +0200
> Michał Górny  wrote:
> [...]
> > > > Of course, we could just validate all the possible cases via
> > > > repoman, and reject the ebuild if there's at least one conflict
> > > > between them. Not sure how to express that properly in the spec
> > > > though. Not sure how it would work practically.  
> > > 
> > > Adding a 2^n check to repoman isn't gonna work well.
> > >   
> > 
> > I'm not saying it's the most optimal algorithm of verifying
> > the correctness of the constraints. It's just the one that's quite
> > obvious -- relatively simple and reliable. If someone can come up with
> > something better that covers at least the most common cases, I'm all
> > for it.
> > 
> > That said, this wouldn't be that much of a problem if we can keep the
> > n low. For a start, we can rule out all flags that don't appear
> > in REQUIRED_USE at all. Furthermore, I think we could also ignore
> > the constraints for flags that don't appear there at least 'twice',
> > and so on.
> 
> :)
> 
> You're applying classical techniques to lower the size of a SAT
> instance so that your exponential algorithm does not explode, but it's
> still hard.
> 
> I'm not sure what you want: If you want to detect that there is an
> impossible constraint, well, ebuild writer will notice soon enough when
> testing it. If you want to detect that there is a way to have a
> conflict between useflags, then there will be valid cases where this
> will happen.
> 
> That said, assuming we have REQUIRED_USE in CNF form, its negation is
> in DNF form. Solving SAT on DNF formulas is easy (linear I think), and
> this would give you an assignment of useflags triggering an impossible
> constraint. e.g. 'foo? ( bar )' with USE='foo -bar' in make.conf.
> This could be used to trigger a repoman warning but basically every
> single ebuild would trigger those.

Not sure if we understand each other.

I'd like the constraints to be plain straightforward, to the point of
having only one acceptable solution. No special Portage-style algorithms
that attempt to provide a reasonable solution to unreasonable input,
resulting in horrible solutions that need 20 more hacks every few
months.

For example:

  foo? ( bar )

would mean 'if you have USE=foo, then USE=bar is enabled as well'. Not
'find some random solution which satisfies this'. In other words, here
changing USE=foo into USE=-foo is not an acceptable solution.

Now, this also means that every constraint that can't be solved in this
easy fashion is invalid. We want to detect that, and warn the developer.
Some of those could be tricky. Simple example:

  foo? ( baz ) bar? ( !baz )

This one is invalid because USE='foo bar' requires both 'baz' and '!baz'
as a solution. Remember that we don't want to do any changes besides
what's explicitly written there, no guessing. However, the following
should be valid:

  foo? ( baz ) bar? ( !foo !baz )

Because now we clearly indicate that USE=bar disables USE=foo,
and therefore makes the first constraint inapplicable. It clearly
indicates course of action for all combinations:

  foo bar baz -> foo bar baz
   F   F   F  -> [valid]
   F   F   T  -> [valid]
   F   T   F  -> [valid]
   F   T   T  ->  F   T   F
   T   F   F  ->  T   F   T
   T   F   T  -> [valid]
   T   T   F  ->  F   T   F
   T   T   T  ->  F   T   F

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Kent Fredric]

On Tue, 30 May 2017 09:56:07 +0100
Ciaran McCreesh  wrote:

> First problem: encoding "don't change this from its current setting
> unless you have a reason to do so" is an utter pain in SAT.

I get the impression that this is harder to solve in Gentoo than it has
to be, because my impression of portage config is that all sources of
configuration are equal.

Configuration
in /etc/portage/* , /etc/portage/profile/*, /usr/portage/profile/* are
taken like equals, and as far as I can tell, portage has no way of
knowing if a use flag is disabled by user choice, or if the flag being
disabled is simply the default.

I think having a clear way to disambiguate between the two would give
the resolver more freedom to adjust the settings that the user didn't
specify as preferences, and try harder to conform to the users
preferences 

Instead of the current approach, where you can either "Change nothing"
or "change anything". 

"Change nothing at first" -> "Change anything within this subset
second" -> "Recommend changes in config if you can't solve within that
constraint" 


pgpRFpnur1A6e.pgp
Description: OpenPGP digital signature

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

[Alexis Ballier]

On Tue, 30 May 2017 20:11:38 +0200
Michał Górny  wrote:
[...]
> > > Of course, we could just validate all the possible cases via
> > > repoman, and reject the ebuild if there's at least one conflict
> > > between them. Not sure how to express that properly in the spec
> > > though. Not sure how it would work practically.  
> > 
> > Adding a 2^n check to repoman isn't gonna work well.
> >   
> 
> I'm not saying it's the most optimal algorithm of verifying
> the correctness of the constraints. It's just the one that's quite
> obvious -- relatively simple and reliable. If someone can come up with
> something better that covers at least the most common cases, I'm all
> for it.
> 
> That said, this wouldn't be that much of a problem if we can keep the
> n low. For a start, we can rule out all flags that don't appear
> in REQUIRED_USE at all. Furthermore, I think we could also ignore
> the constraints for flags that don't appear there at least 'twice',
> and so on.

:)

You're applying classical techniques to lower the size of a SAT
instance so that your exponential algorithm does not explode, but it's
still hard.

I'm not sure what you want: If you want to detect that there is an
impossible constraint, well, ebuild writer will notice soon enough when
testing it. If you want to detect that there is a way to have a
conflict between useflags, then there will be valid cases where this
will happen.

That said, assuming we have REQUIRED_USE in CNF form, its negation is
in DNF form. Solving SAT on DNF formulas is easy (linear I think), and
this would give you an assignment of useflags triggering an impossible
constraint. e.g. 'foo? ( bar )' with USE='foo -bar' in make.conf.
This could be used to trigger a repoman warning but basically every
single ebuild would trigger those.

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

[Michał Górny]

On wto, 2017-05-30 at 17:33 +0200, Alexis Ballier wrote:
> On Tue, 30 May 2017 16:33:32 +0200
> Michał Górny  wrote:
> 
> [...]
> > The problem is: how far is that going to work? That's what I would
> > like to try determining in the first place.
> > 
> > I'm most worried about complex constructs like:
> > 
> >   foo? ( bar ) ^^ ( baz bar )
> 
> The order in which it is written will matter:
> Assuming user has enabled 'foo', first process 'foo? ( bar )', which
> gives you "USE='foo bar'". Then process '^^ ( baz bar )'; all good,
> we're done.
> 
> If user has enabled 'foo baz' then there is a problem and it is
> normal to rant.
> 
> > But I do not have any obvious ideas how to express them safely while
> > preserving readability and relative simplicity of the constructs, i.e.
> > not having to write a big mapping table.
> > 
> > Especially if we are to allow having a preference on baz, the mapping
> > for ^^ alone would be:
> > 
> >   !bar !baz -> !bar  baz
> >bar !baz ->  bar !baz  [valid]
> >   !bar  baz -> !bar  baz  [valid]
> >bar  baz -> !bar  baz
> > 
> > With the additional foo constraint, it becomes harder but not
> > impossible. However, with more constraints we may reach a dead end.
> 
> You already made a convincing argument that || & co are good things to
> have, that's not to write the combinatorics of the whole thing as
> implications!
> 
> Moreover, you can use implications and the processing order as hints: If
> you believe 'if foo and bar are enabled then baz should most likely be
> enabled even if the latter '|| ( bay baz )' would select 'bay' and not
> 'baz'' you prepend required_use by 'foo? bar? baz' and are done with it.
> 
> 
> > Of course, we could just validate all the possible cases via repoman,
> > and reject the ebuild if there's at least one conflict between them.
> > Not sure how to express that properly in the spec though. Not sure
> > how it would work practically.
> 
> Adding a 2^n check to repoman isn't gonna work well.
> 

I'm not saying it's the most optimal algorithm of verifying
the correctness of the constraints. It's just the one that's quite
obvious -- relatively simple and reliable. If someone can come up with
something better that covers at least the most common cases, I'm all for
it.

That said, this wouldn't be that much of a problem if we can keep the n
low. For a start, we can rule out all flags that don't appear
in REQUIRED_USE at all. Furthermore, I think we could also ignore
the constraints for flags that don't appear there at least 'twice',
and so on.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Alexis Ballier]

On Tue, 30 May 2017 16:33:32 +0200
Michał Górny  wrote:

[...]
> The problem is: how far is that going to work? That's what I would
> like to try determining in the first place.
> 
> I'm most worried about complex constructs like:
> 
>   foo? ( bar ) ^^ ( baz bar )

The order in which it is written will matter:
Assuming user has enabled 'foo', first process 'foo? ( bar )', which
gives you "USE='foo bar'". Then process '^^ ( baz bar )'; all good,
we're done.

If user has enabled 'foo baz' then there is a problem and it is
normal to rant.

> But I do not have any obvious ideas how to express them safely while
> preserving readability and relative simplicity of the constructs, i.e.
> not having to write a big mapping table.
> 
> Especially if we are to allow having a preference on baz, the mapping
> for ^^ alone would be:
> 
>   !bar !baz -> !bar  baz
>bar !baz ->  bar !baz  [valid]
>   !bar  baz -> !bar  baz  [valid]
>bar  baz -> !bar  baz
> 
> With the additional foo constraint, it becomes harder but not
> impossible. However, with more constraints we may reach a dead end.

You already made a convincing argument that || & co are good things to
have, that's not to write the combinatorics of the whole thing as
implications!

Moreover, you can use implications and the processing order as hints: If
you believe 'if foo and bar are enabled then baz should most likely be
enabled even if the latter '|| ( bay baz )' would select 'bay' and not
'baz'' you prepend required_use by 'foo? bar? baz' and are done with it.


> Of course, we could just validate all the possible cases via repoman,
> and reject the ebuild if there's at least one conflict between them.
> Not sure how to express that properly in the spec though. Not sure
> how it would work practically.

Adding a 2^n check to repoman isn't gonna work well.


[...]

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

[Michał Górny]

On wto, 2017-05-30 at 14:00 +0200, Ulrich Mueller wrote:
> > > > > > On Tue, 30 May 2017, Alexis Ballier wrote:
> > The way I see it, this boils down to spec'ing something that
> > guarantees there's a unique solution given an input. The solution
> > does not have to be good or bad (we don't have a good metric on that
> > anyway), it just has to be deterministic so that developers can
> > arrange their REQUIRED_USE constraints to have PM chose the proper
> > solution.
> 
> Right. As I see it, the problem we must solve is that for k USE flags
> there are 2**k possible combinations, but there may be only n
> combinations that are valid, with n < 2**k. For example, for
> IUSE="foo bar baz" there are 2**3 = 8 possible combinations, but with
> REQUIRED_USE="|| ( foo bar baz )" or "^^ ( foo bar baz )" only 7 or 3
> of them are valid, respectively.
> 
> Now we can either just specify which of the combinations are valid;
> this is what REQUIRED_USE currently does. Or we can specify a complete
> mapping from every invalid input combination of flags to a valid
> output combination. I think we should do the latter.
> 

Well, you have a point. My proposal was to do the latter, reusing
the syntax from the former.

Strictly speaking, the following REQUIRED_USE are equivalent:

  foo? ( bar )  (1)

  !bar? ( !foo )(2)

However, the developers already select between the two to suggest
a specific solution to the user. (1) is used to suggest that enabling
the 'bar' flag is the more obvious solution; (2) is used to suggest that
disabling 'foo' would be most likely preferred.

If we stick to that, I think we can easily achieve the latter goal
without sacrificing much of readability and/or making things much harder
for developers. That is, treating the '?' as implication:

  foo? ( bar )-> foo implies bar

  !bar? ( !foo )  -> !bar implies !foo

The problem is: how far is that going to work? That's what I would like
to try determining in the first place.

I'm most worried about complex constructs like:

  foo? ( bar ) ^^ ( baz bar )

But I do not have any obvious ideas how to express them safely while
preserving readability and relative simplicity of the constructs, i.e.
not having to write a big mapping table.

Especially if we are to allow having a preference on baz, the mapping
for ^^ alone would be:

  !bar !baz -> !bar  baz
   bar !baz ->  bar !baz  [valid]
  !bar  baz -> !bar  baz  [valid]
   bar  baz -> !bar  baz

With the additional foo constraint, it becomes harder but not
impossible. However, with more constraints we may reach a dead end.

Of course, we could just validate all the possible cases via repoman,
and reject the ebuild if there's at least one conflict between them. Not
sure how to express that properly in the spec though. Not sure how it
would work practically.

As I said, it's an early RFC to figure out any tips before starting to
investigate the technical mysteries. Probably worth to look into
existing REQUIRED_USE uses and put them into some trivial constraint
solver.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Michał Górny]

On wto, 2017-05-30 at 11:34 +0200, Alexis Ballier wrote:
> Sidenote: I just realized '|| ( a b c )' with left-most preference
> > > might be better since we are not dealing with binary variables but
> > > ternary ones (user disabled, user enabled, unspecified). 'USE="" ||
> > > ( a b c )' should evaluate to 'a', 'USE="-a" || ( a b c )' should
> > > evaluate to 'b'. I don't see how to rewrite that with pure
> > > implications.  
> > 
> > The ternary concept is not exactly in line with how we handle USE
> > flags now. It's more like multi-layer binary. My proposal solved the
> > problem you were trying to solve via establishing priorities -- I
> > find it simpler to reorder the flags and use binary logic than to
> > invent a more complex logic to solve the same problem.
> 
> I've re-read your proposal entirely and I don't see where you describe
> how to establish priorities. You describe how users can specify those,
> but nowhere do I see any default priority being mandated. If you
> describe and mandate it, then all is good I think. As I said, there
> are plenty of ways to solve the problem but it has to be mandated
> otherwise you're just postponing issues, not solving them.
> 

Hmm, I'm sorry then, I must've missed specifying it. Of course
the intent was that the default preference was deterministic. I would go
for 'left-most first' idea, as that seems the most obvious.


-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Ulrich Mueller]

> On Tue, 30 May 2017, Alexis Ballier wrote:

> The way I see it, this boils down to spec'ing something that
> guarantees there's a unique solution given an input. The solution
> does not have to be good or bad (we don't have a good metric on that
> anyway), it just has to be deterministic so that developers can
> arrange their REQUIRED_USE constraints to have PM chose the proper
> solution.

Right. As I see it, the problem we must solve is that for k USE flags
there are 2**k possible combinations, but there may be only n
combinations that are valid, with n < 2**k. For example, for
IUSE="foo bar baz" there are 2**3 = 8 possible combinations, but with
REQUIRED_USE="|| ( foo bar baz )" or "^^ ( foo bar baz )" only 7 or 3
of them are valid, respectively.

Now we can either just specify which of the combinations are valid;
this is what REQUIRED_USE currently does. Or we can specify a complete
mapping from every invalid input combination of flags to a valid
output combination. I think we should do the latter.

Ulrich


pgptD7wtEavWk.pgp
Description: PGP signature

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

[Alexis Ballier]

On Tue, 30 May 2017 10:29:48 +0200
Michał Górny  wrote:
> That's why I'm sending this to the mailing list as a RFC, not a
> proposal to vote on. It solves a defined set of problems, and gives
> other chance to improve it and turn it into a complete solution. It's
> not like it's going anywhere before it's implemented as a PoC and
> tested.

Nobody's blaming you for that, rather the contrary :)

> > > Yes, they do. They improve readability, compared to cascades of
> > > plain constraints. I'm pretty sure users will be happier to see
> > > 'you need to select one of foo, bar, baz' than 'if foo is
> > > disabled, then ...'  
> > 
> > If the point is to automatically propose a solution, then who cares
> > about readability? Users won't even see that message.  
> 
> But users should be able to reasonably figure out what happened,
> exactly. There's a difference in quality between the two messages:
> 
> a. 'foo is enabled; bar, got disabled',
> 
> b. 'one of foo, bar, baz had to be enabled => you chose foo'.
> 
> Not saying you can't figure it out. Saying in a more complex case,
> grouping constraints like this is helpful.


Why not then. You're right it makes more sense.


> > Note that there are plenty of ways to add determinism in your
> > proposal, but it *has* to be specified otherwise PM can't rely on
> > it. For instance, you can say that in an unsatisfied || block then
> > the left-most useflag is automatically enabled. || then becomes some
> > syntactic sugar around unary operators: || ( a ... ) becomes
> > equivalent to '!...? ( a )'. You can do the same for other
> > operators.
> > 
> > 
> > Sidenote: I just realized '|| ( a b c )' with left-most preference
> > might be better since we are not dealing with binary variables but
> > ternary ones (user disabled, user enabled, unspecified). 'USE="" ||
> > ( a b c )' should evaluate to 'a', 'USE="-a" || ( a b c )' should
> > evaluate to 'b'. I don't see how to rewrite that with pure
> > implications.  
> 
> The ternary concept is not exactly in line with how we handle USE
> flags now. It's more like multi-layer binary. My proposal solved the
> problem you were trying to solve via establishing priorities -- I
> find it simpler to reorder the flags and use binary logic than to
> invent a more complex logic to solve the same problem.

I've re-read your proposal entirely and I don't see where you describe
how to establish priorities. You describe how users can specify those,
but nowhere do I see any default priority being mandated. If you
describe and mandate it, then all is good I think. As I said, there
are plenty of ways to solve the problem but it has to be mandated
otherwise you're just postponing issues, not solving them.


Alexis.

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

[Alexis Ballier]

On Tue, 30 May 2017 09:56:07 +0100
Ciaran McCreesh  wrote:

> On Tue, 30 May 2017 10:46:54 +0200
> Alexis Ballier  wrote:
> > On Tue, 30 May 2017 09:22:45 +0100
> > Ciaran McCreesh  wrote:  
> > > On Tue, 30 May 2017 09:42:45 +0200
> > > Alexis Ballier  wrote:
> > > > Oh crap, this requires to solve SAT.  
> > > 
> > > The main problem would not be solving SAT, in this case. The
> > > problem is providing the right answer when not enough information
> > > is given. Spitting out a resolution which satisfies every
> > > dependency isn't typically that difficult. Spitting out a
> > > resolution which doesn't just turn off all your use flags and
> > > uninstall most of your programs is the hard part.
> > 
> > I don't really understand here: Assuming the formula is reduced
> > where user-set useflags and profile-masked/forced ones are already
> > assigned their true/false values, this leaves a formula with
> > variables where changing any of those won't turn off (or on)
> > anything you didn't want. If you can solve SAT on this reduced
> > instance then you're safe, aren't you ?  
> 
> First problem: encoding "don't change this from its current setting
> unless you have a reason to do so" is an utter pain in SAT. There are
> other models like ASP that can just about get around this, but
> expressing it properly is best done by just writing your own solver.
> Remember that you have to allow the solver to toggle some flags, so
> you can't just lock everything, but at the same time, you don't want
> the solver to randomly toggle a flag that isn't specified by the user
> or the profile, unless it absolutely has a good reason to do so.
> 
> Second problem: a solver will spit out an arbitrary solution. If the
> user then runs it again, there's no guarantee that it will spit out
> the same arbitrary solution. That can be addressed by the right
> choice of restart policies and tiebreaking etc if you're prepared to
> muck around with the solver enough. But even if you do, suppose the
> user thinks "yes, that's almost fine, but let me change one other
> thing" (or if the install fails half-way through and the user tries
> to carry on after fixing it). The solver will then spit out a totally
> different arbitrary solution that looks nothing like the first one.


The way I see it, this boils down to spec'ing something that guarantees
there's a unique solution given an input. The solution does not have to
be good or bad (we don't have a good metric on that anyway), it just
has to be deterministic so that developers can arrange their
REQUIRED_USE constraints to have PM chose the proper solution.


Note: To me, the problems you describe are really the root of SAT
solving problems (or any NP problem FWIW): An algorithm has to make
choices that might have consequences arbitrary far and it might realize
after running for a while that its initial assumption was invalid.

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

[Ciaran McCreesh]

On Tue, 30 May 2017 10:46:54 +0200
Alexis Ballier  wrote:
> On Tue, 30 May 2017 09:22:45 +0100
> Ciaran McCreesh  wrote:
> > On Tue, 30 May 2017 09:42:45 +0200
> > Alexis Ballier  wrote:  
> > > Oh crap, this requires to solve SAT.
> > 
> > The main problem would not be solving SAT, in this case. The problem
> > is providing the right answer when not enough information is given.
> > Spitting out a resolution which satisfies every dependency isn't
> > typically that difficult. Spitting out a resolution which doesn't
> > just turn off all your use flags and uninstall most of your programs
> > is the hard part.  
> 
> I don't really understand here: Assuming the formula is reduced where
> user-set useflags and profile-masked/forced ones are already assigned
> their true/false values, this leaves a formula with variables where
> changing any of those won't turn off (or on) anything you didn't want.
> If you can solve SAT on this reduced instance then you're safe, aren't
> you ?

First problem: encoding "don't change this from its current setting
unless you have a reason to do so" is an utter pain in SAT. There are
other models like ASP that can just about get around this, but
expressing it properly is best done by just writing your own solver.
Remember that you have to allow the solver to toggle some flags, so you
can't just lock everything, but at the same time, you don't want the
solver to randomly toggle a flag that isn't specified by the user or
the profile, unless it absolutely has a good reason to do so.

Second problem: a solver will spit out an arbitrary solution. If the
user then runs it again, there's no guarantee that it will spit out the
same arbitrary solution. That can be addressed by the right choice of
restart policies and tiebreaking etc if you're prepared to muck around
with the solver enough. But even if you do, suppose the user thinks
"yes, that's almost fine, but let me change one other thing" (or if
the install fails half-way through and the user tries to carry on after
fixing it). The solver will then spit out a totally different arbitrary
solution that looks nothing like the first one.

-- 
Ciaran McCreesh

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

[Alexis Ballier]

On Tue, 30 May 2017 09:22:45 +0100
Ciaran McCreesh  wrote:

> On Tue, 30 May 2017 09:42:45 +0200
> Alexis Ballier  wrote:
> > Oh crap, this requires to solve SAT.  
> 
> The main problem would not be solving SAT, in this case. The problem
> is providing the right answer when not enough information is given.
> Spitting out a resolution which satisfies every dependency isn't
> typically that difficult. Spitting out a resolution which doesn't
> just turn off all your use flags and uninstall most of your programs
> is the hard part.

I don't really understand here: Assuming the formula is reduced where
user-set useflags and profile-masked/forced ones are already assigned
their true/false values, this leaves a formula with variables where
changing any of those won't turn off (or on) anything you didn't want.
If you can solve SAT on this reduced instance then you're safe, aren't
you ?

> > Not hard as in you need a Ph.D. in algorithms to solve it but the
> > kind of hardness almost every cryptographic algorithm used today,
> > and in the foreseeable future, relies on.  
> 
> Hrm, you're a bit off, there. SAT solving in practice isn't usually
> that bad unless either your inputs are huge or they're deliberately
> crafted to be ultra-nasty. Being NP-complete just means that instances
> that will hit exponential behaviour exist, not that those instances
> will occur in the application area you care about.

Yes, SAT is somewhat one of the easiest NP complete problems. Still,
do we accept everyone having php installed to have its 'emerge -uDN
world' consume 1 cpu-minute? 10 cpu-minutes? 60 cpu-minutes? What's the
limit? How do we define 'ultra-nasty' constructs? How do we avoid them?
Do we want to spec the solver's heuristic used so that developers can
rely on it performing well on some constructs and poorly on some others?
Do we want to spec some syntax so that PM developers can use an
heuristic performing well on the instances provided?

I really believe that's too many questions for something that can be
solved efficiently in a simpler manner.

Bests,

Alexis.

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

[Michał Górny]

On wto, 2017-05-30 at 09:42 +0200, Alexis Ballier wrote:
> On Mon, 29 May 2017 23:23:55 +0200
> Michał Górny  wrote:
> 
> > On pon, 2017-05-29 at 20:00 +0200, Alexis Ballier wrote:
> > > On Mon, 29 May 2017 17:33:13 +0200
> > > Michał Górny  wrote:
> 
> [...]
> > > > It can also be used with multi-flag ??, ^^ and || constraints,
> > > > i.e.:
> > > > 
> > > > - ?? means that at most one of the flags can be enabled. If user
> > > > configuration causes more than one of the flags to be enabled,
> > > > additional flags are implicitly disabled (masked) to satisfy
> > > > the constraint.
> > > > 
> > > > - || means that at least one of the flags must be enabled. If user
> > > > configuration causes none of the flags to be enabled, one of them
> > > > is enabled implicitly (forced).
> > > > 
> > > > - ^^ means that exactly one of the flags must be enabled. The
> > > > behavior is a combination of both above constraints.
> > > > 
> > > > The automated solving of USE constraints would require the
> > > > developers to consider the implicit effect of the constraints
> > > > they are writing.  
> > > 
> > > 
> > > Can you provide an efficient algorithm for the above syntax?
> > > That is, given a set of +/- useflags forced by user, output the set
> > > of effective useflags (or a rant if it is inconsistent).  
> > 
> > I'd rather leave that to people who are good with algorithms. I find
> > the whole thing scary but I don't really see a sane alternative here.
> 
> Well, Ciaran is a bit extreme with his implementation thing, but
> he's right in the sense that here you're really repeating the same
> mistakes that you're trying to fix. REQUIRED_USE was invented the same
> way: Let's add some nice syntax to express dependency between useflags.
> Ship it. Oh crap, this requires to solve SAT. Well, nothing good can be
> done here, let's spit out to the user to chose for herself.
> With your proposal, it seems to me you're simply postponing the problem
> but not fixing it: Instead of spiting that one has to enable some
> useflags, you'd spit that one has to specify how to solve the
> constraint by expressing some preference. In the end, this'll add
> another layer of complexity in both PM and the user configuration but
> would not solve the root of the problem which is that no-one knows how
> to automatically find a solution to those constraints and PM can't take
> any action without user input.
> 
> You can't get away with "There is a solution but I'll leave that to
> people who are good with algorithms": That is roughly the definition of
> NP. If the person writing a proposal for a new feature (which is thus
> supposedly the one person that has thoroughly thought the problem) can't
> at least roughly draft how to implement it, that doesn't give much faith
> in that it can be done properly. It certainly does not mean said person
> is not good with algorithms but rather that the problem is very likely
> to be a hard one. Not hard as in you need a Ph.D. in algorithms to
> solve it but the kind of hardness almost every cryptographic algorithm
> used today, and in the foreseeable future, relies on.

That's why I'm sending this to the mailing list as a RFC, not a proposal
to vote on. It solves a defined set of problems, and gives other chance
to improve it and turn it into a complete solution. It's not like it's
going anywhere before it's implemented as a PoC and tested.

> > Yes, they do. They improve readability, compared to cascades of plain
> > constraints. I'm pretty sure users will be happier to see 'you need to
> > select one of foo, bar, baz' than 'if foo is disabled, then ...'
> 
> If the point is to automatically propose a solution, then who cares
> about readability? Users won't even see that message.

But users should be able to reasonably figure out what happened,
exactly. There's a difference in quality between the two messages:

a. 'foo is enabled; bar, got disabled',

b. 'one of foo, bar, baz had to be enabled => you chose foo'.

Not saying you can't figure it out. Saying in a more complex case,
grouping constraints like this is helpful.

> 
> Note that there are plenty of ways to add determinism in your proposal,
> but it *has* to be specified otherwise PM can't rely on it. For
> instance, you can say that in an unsatisfied || block then the
> left-most useflag is automatically enabled. || then becomes some
> syntactic sugar around unary operators: || ( a ... ) becomes equivalent
> to '!...? ( a )'. You can do the same for other operators.
> 
> 
> Sidenote: I just realized '|| ( a b c )' with left-most preference might
> be better since we are not dealing with binary variables but ternary
> ones (user disabled, user enabled, unspecified). 'USE="" || ( a b c )'
> should evaluate to 'a', 'USE="-a" || ( a b c )' should evaluate to 'b'.
> I don't see how to rewrite that with pure implications.

The ternary concept is not exactly in line with how we handle USE flags
now. It's 

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

[Ciaran McCreesh]

On Tue, 30 May 2017 09:42:45 +0200
Alexis Ballier  wrote:
> Oh crap, this requires to solve SAT.

The main problem would not be solving SAT, in this case. The problem is
providing the right answer when not enough information is given.
Spitting out a resolution which satisfies every dependency isn't
typically that difficult. Spitting out a resolution which doesn't
just turn off all your use flags and uninstall most of your programs is
the hard part.

> Not hard as in you need a Ph.D. in algorithms to solve it but the
> kind of hardness almost every cryptographic algorithm used today, and
> in the foreseeable future, relies on.

Hrm, you're a bit off, there. SAT solving in practice isn't usually
that bad unless either your inputs are huge or they're deliberately
crafted to be ultra-nasty. Being NP-complete just means that instances
that will hit exponential behaviour exist, not that those instances
will occur in the application area you care about.

-- 
Ciaran McCreesh

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

[Alexis Ballier]

On Tue, 30 May 2017 10:05:41 +0200
Ulrich Mueller  wrote:

> > On Tue, 30 May 2017, Alexis Ballier wrote:  
> 
> > On Tue, 30 May 2017 00:01:16 +0200
> > Ulrich Mueller  wrote:  
> 
> >> Also, can we find a better name? Sorry for the bikeshedding at this
> >> early stage, but I believe that ENFORCED_USE can be easily confused
> >> with use.force in profiles. MAPPED_USE? USE_MAP?  
> 
> > Why do we even need a new name ?  
> 
> This was under the assumption that we would somewhat restrict the
> syntax.
> 
> Sure, if someone comes up with an algorithm that will give a unique
> and predictable solution with current REQUIRED_USE syntax then we can
> keep the old name.

Even if restricting the syntax I'm not sure it is desirable either: If
we keep current REQUIRED_USE we'll still have cases where it'll fail
horribly, hence not fixing the issue.


If all you care about is the syntax, then sure it is doable, but the
semantics have to change, and I don't see much difference in
restricting the syntax vs. changing its meaning.

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

[Ulrich Mueller]

> On Tue, 30 May 2017, Alexis Ballier wrote:

> On Tue, 30 May 2017 00:01:16 +0200
> Ulrich Mueller  wrote:

>> Also, can we find a better name? Sorry for the bikeshedding at this
>> early stage, but I believe that ENFORCED_USE can be easily confused
>> with use.force in profiles. MAPPED_USE? USE_MAP?

> Why do we even need a new name ?

This was under the assumption that we would somewhat restrict the
syntax.

Sure, if someone comes up with an algorithm that will give a unique
and predictable solution with current REQUIRED_USE syntax then we can
keep the old name.

Ulrich


pgpkcDvb1xl6v.pgp
Description: PGP signature

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

[Alexis Ballier]

On Tue, 30 May 2017 00:01:16 +0200
Ulrich Mueller  wrote:

> > On Mon, 29 May 2017, Michał Górny wrote:  

> Also, can we find a better name? Sorry for the bikeshedding at this
> early stage, but I believe that ENFORCED_USE can be easily confused
> with use.force in profiles. MAPPED_USE? USE_MAP?

Why do we even need a new name ?

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

[Alexis Ballier]

On Mon, 29 May 2017 23:23:55 +0200
Michał Górny  wrote:

> On pon, 2017-05-29 at 20:00 +0200, Alexis Ballier wrote:
> > On Mon, 29 May 2017 17:33:13 +0200
> > Michał Górny  wrote:
[...]
> > > It can also be used with multi-flag ??, ^^ and || constraints,
> > > i.e.:
> > > 
> > > - ?? means that at most one of the flags can be enabled. If user
> > > configuration causes more than one of the flags to be enabled,
> > > additional flags are implicitly disabled (masked) to satisfy
> > > the constraint.
> > > 
> > > - || means that at least one of the flags must be enabled. If user
> > > configuration causes none of the flags to be enabled, one of them
> > > is enabled implicitly (forced).
> > > 
> > > - ^^ means that exactly one of the flags must be enabled. The
> > > behavior is a combination of both above constraints.
> > > 
> > > The automated solving of USE constraints would require the
> > > developers to consider the implicit effect of the constraints
> > > they are writing.  
> > 
> > 
> > Can you provide an efficient algorithm for the above syntax?
> > That is, given a set of +/- useflags forced by user, output the set
> > of effective useflags (or a rant if it is inconsistent).  
> 
> I'd rather leave that to people who are good with algorithms. I find
> the whole thing scary but I don't really see a sane alternative here.

Well, Ciaran is a bit extreme with his implementation thing, but
he's right in the sense that here you're really repeating the same
mistakes that you're trying to fix. REQUIRED_USE was invented the same
way: Let's add some nice syntax to express dependency between useflags.
Ship it. Oh crap, this requires to solve SAT. Well, nothing good can be
done here, let's spit out to the user to chose for herself.
With your proposal, it seems to me you're simply postponing the problem
but not fixing it: Instead of spiting that one has to enable some
useflags, you'd spit that one has to specify how to solve the
constraint by expressing some preference. In the end, this'll add
another layer of complexity in both PM and the user configuration but
would not solve the root of the problem which is that no-one knows how
to automatically find a solution to those constraints and PM can't take
any action without user input.

You can't get away with "There is a solution but I'll leave that to
people who are good with algorithms": That is roughly the definition of
NP. If the person writing a proposal for a new feature (which is thus
supposedly the one person that has thoroughly thought the problem) can't
at least roughly draft how to implement it, that doesn't give much faith
in that it can be done properly. It certainly does not mean said person
is not good with algorithms but rather that the problem is very likely
to be a hard one. Not hard as in you need a Ph.D. in algorithms to
solve it but the kind of hardness almost every cryptographic algorithm
used today, and in the foreseeable future, relies on.

> Worst case, we have to figure out some arbitrary limitations to keep
> things sane.

The main point of my reply was (and still is) to find such limitations.
It is not as arbitrary as you may think and requires to be properly
understood so that we have to sacrifice the least expressivity power. A
good way to understand what a proper limitation would be is to try to
solve the problem.

> > Maybe I'm mistaken, but I doubt it is possible with n-ary
> > constraints.
> > 
> > Now the extra question: Do those n-ary operators have any
> > advantage ?  
> 
> Yes, they do. They improve readability, compared to cascades of plain
> constraints. I'm pretty sure users will be happier to see 'you need to
> select one of foo, bar, baz' than 'if foo is disabled, then ...'

If the point is to automatically propose a solution, then who cares
about readability? Users won't even see that message.

Note that there are plenty of ways to add determinism in your proposal,
but it *has* to be specified otherwise PM can't rely on it. For
instance, you can say that in an unsatisfied || block then the
left-most useflag is automatically enabled. || then becomes some
syntactic sugar around unary operators: || ( a ... ) becomes equivalent
to '!...? ( a )'. You can do the same for other operators.


Sidenote: I just realized '|| ( a b c )' with left-most preference might
be better since we are not dealing with binary variables but ternary
ones (user disabled, user enabled, unspecified). 'USE="" || ( a b c )'
should evaluate to 'a', 'USE="-a" || ( a b c )' should evaluate to 'b'.
I don't see how to rewrite that with pure implications.

> > The point is to express some preference, below you suggest to leave
> > that to the user, but what about leaving that to the ebuild
> > developer?  
> 
> Well, I don't find that a killer feature but I don't see a reason to
> take it away either. Either way we have some risks, especially when
> USE dependencies and blockers are involved. In both scenarios, I find

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

[Ciaran McCreesh]

On Tue, 30 May 2017 00:01:16 +0200
Ulrich Mueller  wrote:
> > On Mon, 29 May 2017, Michał Górny wrote:  
> > On pon, 2017-05-29 at 20:00 +0200, Alexis Ballier wrote:  
> >> Can you provide an efficient algorithm for the above syntax? That
> >> is, given a set of +/- useflags forced by user, output the set of
> >> effective useflags (or a rant if it is inconsistent).  
> 
> > I'd rather leave that to people who are good with algorithms. I find
> > the whole thing scary but I don't really see a sane alternative
> > here. Worst case, we have to figure out some arbitrary limitations
> > to keep things sane.  
> 
> IMHO the sanest alternative would be to restrict the syntax to USE
> conditional forms which have an obvious solution. One of the many
> problems of REQUIRED_USE is that it sometimes requires solving a
> Zebra Puzzle.

Solving zebra puzzles isn't really that bad in practice most of the
time. The tricky bit is finding the *right* solution, given poor input
data that doesn't really let you evaluate what right is. As a simple
example, in the olden days, the most obvious and shortest answer to
fixing Gnome resolution errors was to set USE=mips because that
disabled a whole load of browser dependencies...

-- 
Ciaran McCreesh

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

[Ulrich Mueller]

> On Mon, 29 May 2017, Michał Górny wrote:

> On pon, 2017-05-29 at 20:00 +0200, Alexis Ballier wrote:
>> Can you provide an efficient algorithm for the above syntax? That
>> is, given a set of +/- useflags forced by user, output the set of
>> effective useflags (or a rant if it is inconsistent).

> I'd rather leave that to people who are good with algorithms. I find
> the whole thing scary but I don't really see a sane alternative here.
> Worst case, we have to figure out some arbitrary limitations to keep
> things sane.

IMHO the sanest alternative would be to restrict the syntax to USE
conditional forms which have an obvious solution. One of the many
problems of REQUIRED_USE is that it sometimes requires solving a
Zebra Puzzle.

Also, can we find a better name? Sorry for the bikeshedding at this
early stage, but I believe that ENFORCED_USE can be easily confused
with use.force in profiles. MAPPED_USE? USE_MAP?

Ulrich


pgpoQc77HrAEH.pgp
Description: PGP signature

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

[Ciaran McCreesh]

On Mon, 29 May 2017 23:23:55 +0200
Michał Górny  wrote:
> > Can you provide an efficient algorithm for the above syntax?
> > That is, given a set of +/- useflags forced by user, output the set
> > of effective useflags (or a rant if it is inconsistent).  
> 
> I'd rather leave that to people who are good with algorithms. I find
> the whole thing scary but I don't really see a sane alternative here.
> Worst case, we have to figure out some arbitrary limitations to keep
> things sane.

That bit is NP-complete by an easy reduction from SAT. That isn't
necessarily a problem, because resolution isn't even in NP yet we're
still managing to spit out decent answers most of the time. Rather, the
difficulty lies in spitting out a *good* solution to the problem from
a user's perspective, and that's something that can't be done without
extremely high quality inputs.

-- 
Ciaran McCreesh

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

[Michał Górny]

On pon, 2017-05-29 at 20:00 +0200, Alexis Ballier wrote:
> On Mon, 29 May 2017 17:33:13 +0200
> Michał Górny  wrote:
> 
> > In the basic form, it can be used to conditionally force a specific
> > flag to be enabled or disabled. For example:
> > 
> >   foo? ( bar )
> > 
> > would mean that the bar flag is implicitly enabled (forced) if foo is
> > enabled as well. Appropriately:
> > 
> >   foo? ( !bar )
> > 
> > would mean that the bar flag is implicitly disabled (masked) in that
> > case.
> 
> All good here.
> 
> 
> > It can also be used with multi-flag ??, ^^ and || constraints, i.e.:
> > 
> > - ?? means that at most one of the flags can be enabled. If user
> > configuration causes more than one of the flags to be enabled,
> > additional flags are implicitly disabled (masked) to satisfy
> > the constraint.
> > 
> > - || means that at least one of the flags must be enabled. If user
> > configuration causes none of the flags to be enabled, one of them is
> > enabled implicitly (forced).
> > 
> > - ^^ means that exactly one of the flags must be enabled. The behavior
> > is a combination of both above constraints.
> > 
> > The automated solving of USE constraints would require the developers
> > to consider the implicit effect of the constraints they are writing.
> 
> 
> Can you provide an efficient algorithm for the above syntax?
> That is, given a set of +/- useflags forced by user, output the set of
> effective useflags (or a rant if it is inconsistent).

I'd rather leave that to people who are good with algorithms. I find
the whole thing scary but I don't really see a sane alternative here.
Worst case, we have to figure out some arbitrary limitations to keep
things sane.

> Maybe I'm mistaken, but I doubt it is possible with n-ary constraints.
> 
> Now the extra question: Do those n-ary operators have any advantage ?

Yes, they do. They improve readability, compared to cascades of plain
constraints. I'm pretty sure users will be happier to see 'you need to
select one of foo, bar, baz' than 'if foo is disabled, then ...'

> The point is to express some preference, below you suggest to leave
> that to the user, but what about leaving that to the ebuild developer?

Well, I don't find that a killer feature but I don't see a reason to
take it away either. Either way we have some risks, especially when USE
dependencies and blockers are involved. In both scenarios, I find it
less risky to let user control the order than to rely on all developers
respecting the same preference order. Not saying the latter wouldn't
hurt anyway but the users would at least have an easy way out.

> That way, e.g., || can be rewritten as implications: '|| ( a b c )'
> becomes '!b? !c? a' meaning if none is enabled then a is automatically
> enabled.

Unless you are planning to cache the rewritten forms, I don't see
a problem, really. You just reorder the flags according to the apparent
preference before rewriting.

> 
> Note that with only unary constraints, computing the set of effective
> useflags becomes trivial (linear in the # of useflags + constraints):
> take the constraints as a list, solve the first one, add its
> consequences (if any) to the set of forced useflags, continue with next
> constraint or rant if the set of forced flags is inconsistent.

Sounds fine. But I'm not an expert to really judge that ;-).

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Michał Górny]

On pon, 2017-05-29 at 20:24 +0100, Ciaran McCreesh wrote:
> On Mon, 29 May 2017 17:33:13 +0200
> Michał Górny  wrote:
> > For a long time we seem to be missing appropriate tools to handle USE
> > flag constraints efficiently. EAPI 4 brought REQUIRED_USE but all
> > things considered, it has proven to be far from an optimal solution.
> > I would therefore like to discuss adding a better tool to amend or
> > replace it, to allow for automated handling of USE flag constraints.
> 
> REQUIRED_USE's problems all come from it being thrown in at the last
> minute without any testing of either the user experience or the
> feasibility of its implementation. Have you implemented a prototype to
> show that you can actually fix those problems?
> 

I tend to RFC before starting the implementation. Saves effort.

-- 
Best regards,
Michał Górny


signature.asc
Description: This is a digitally signed message part

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

[Ciaran McCreesh]

On Mon, 29 May 2017 21:42:33 +0200
Michał Górny  wrote:
> On pon, 2017-05-29 at 20:24 +0100, Ciaran McCreesh wrote:
> > On Mon, 29 May 2017 17:33:13 +0200
> > Michał Górny  wrote:  
> > > For a long time we seem to be missing appropriate tools to handle
> > > USE flag constraints efficiently. EAPI 4 brought REQUIRED_USE but
> > > all things considered, it has proven to be far from an optimal
> > > solution. I would therefore like to discuss adding a better tool
> > > to amend or replace it, to allow for automated handling of USE
> > > flag constraints.  
> > 
> > REQUIRED_USE's problems all come from it being thrown in at the last
> > minute without any testing of either the user experience or the
> > feasibility of its implementation. Have you implemented a prototype
> > to show that you can actually fix those problems?
> 
> I tend to RFC before starting the implementation. Saves effort.

Not the implementation. A prototype implementation. As we saw from
REQUIRED_USE, it really doesn't save effort to spend time specifying
something that can't even remotely work...

-- 
Ciaran McCreesh