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

[Ciaran McCreesh <ciaran.mccreesh@googlemail.com>]

On Tue, 30 May 2017 10:46:54 +0200
Alexis Ballier <aballier@gentoo.org> wrote:
> On Tue, 30 May 2017 09:22:45 +0100
> Ciaran McCreesh <ciaran.mccreesh@googlemail.com> wrote:
> > On Tue, 30 May 2017 09:42:45 +0200
> > Alexis Ballier <aballier@gentoo.org> 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