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 <mgorny@g.o> 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 <mgorny@g.o> 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 <mgorny@g.o> 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 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.

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

> Furthermore, the ternary idea
> starts becoming blurry when you have to deal with profiles that you
> explicitly want to disable in user configuration.

I'm not following you here.

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

> >  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 for the solver ?

> which gives a single predictable solution:

Then ebuild writer should not write 'foo? ( baz ) bar? ( !baz )' but
rather: 'foo? ( !bar baz ) bar? ( !baz )', which should cover more
cases. With USE="foo bar", the message would then be:
"
  The constraint 'foo? ( !bar )' is violated.
      foo is enabled because $reason
      bar is enabled because $reason
"
which is similar to the above except there's one less step for
explaining the reasons. It's not dramatic but it is, indeed, desirable
to have simple & clear reasons. I'd say that's more to the argument for
specifying completely how to solve that and leave those small
improvements to ebuild writers and/or QA.

[...]
> > > 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.
> >
>
> As I said, it's a matter of configuration to decide which flags should
> be touched, and which not. Of course if we find that necessary, we may
> go into defining a specific set in the profiles or metadata.
>
> However, I would rather focus on getting a PoC solver and checker
> first, and play with existing constraints to see how it all works.

The solver seems on good tracks, at least from the algorithmic POV. The
checker, however, is not clear at all to me. The main reason is that to
determine if the solver will be able to solve it, it needs to know what
the solver can toggle and what not.

Alexis.