On Fri, 09 Jun 2017 14:54:07 +0200
Michał Górny <mgo...@gentoo.org> 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 <mgo...@gentoo.org> 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 <mgo...@gentoo.org> 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 specific problem
> > > via applying some kind of 'if forced/masked' logic into the AST.
> >
> > I think we're having communication interferences here :) That's
> > exactly what I'm talking about.
> >
> > More specifically:
> >
> > For each profile:
> > formula=replace_masks_and_force_by_constants(required_use)
> > simplify(formula)
> > nsolve(formula)
> >
> > In your example above, we'd call 'nsolve("|| ( X )")' and
> > 'nsolve("|| ( Y )")' (or even simpler, depending on how simplify()
> > is defined). If both X and Y are masked on a profile, then that'd
> > reduce to 'nsolve("False")' which would rant.
>
> So you're talking about reducing prior to transforming? Yes, that'd
> work. As I mentioned in one of the first mails wrt my reference
> implementation, I've used reordering (stable sort) instead of reducing
> since it was simpler.
>
> If you reduce (simplify), you need to account for special cases like
> getting '|| ()' etc. If you reorder only, things just fail the normal
> way.
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.
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().
> > I think that for solve(), reordering is basically equivalent since
> > we always favour leftmost. However, we have to somehow guarantee
> > that solve() will never try to enable a masked flag. This is
> > guaranteed by the above checks on profiles if enforced by repoman.
> > If we apply the same logic for solve that'd basically be built-in
> > (masked/forced flags wont appear in solve()'s input anymore), which
> > I believe is better. Keep in mind that users can mask and force
> > some useflags, so the repoman check won't catch that.
> >
> >
> > > > > > So, the very first thing to do is to agree that the above
> > > > > > solver (the trueify function) is what we want to implement
> > > > > > and set this in stone. There's no point in implementing a
> > > > > > proper requse checker if the algorithm is meant to change.
> > > > > > Having a formal definition will also be necessary to
> > > > > > mandate that in future EAPIs.
> > > > > >
> > > > > > Then, and only then, we'd need to have the above solver
> > > > > > implemented into portage (hidden under a FEATURES) and
> > > > > > import my nsolve into repoman (after due cleanup).
> > > > > >
> > > > >
> > > > > Yes, that's my goal. However, before we can set the algorithm
> > > > > in stone we need to verify that it will work in all of the
> > > > > supported cases.
> > > >
> > > > Yep, that's the point of nsolve/classify :)
> > > >
> > > > > Preferably it should also be as simple as possible to avoid
> > > > > putting too much complexity in the spec.
> > > >
> > > > Yes; not sure if anything simpler than the above can be achieved
> > > > though.
> > >
> > > Actually, I think we should roughly proceed in the following way:
> > >
> > > 1. Design the solve() algorithm.
> > >
> > > 1a. Test solve() on isolated test cases.
> > >
> > > 1b. Integrate solve() into Portage (as optional feature) and
> > > encourage wider testing.
> > >
> > > 2. Design the nsolve() verification based on solve().
> > >
> > > 2a. Test nsolve() separately.
> > >
> > > 2b. Start fixing simple cases that do not bring any controversy
> > > (like most of the reorderings).
> > >
> > > 2c. Integrate nsolve() into repoman.
> > >
> > > 3. Spec the whole thing and decide how to go next.
> > >
> > >
> > > Assuming that 1* and 2* is to be done simultaneously, and each
> > > subpoint implies that if we hit any walls, we can go back to a
> > > previous point and fix the design.
> > >
> > > I think we're mostly past 1a and 2a now. We should try to think a
> > > bit more about the corner cases right now, and when we're done
> > > with that, the next step would be to:
> > >
> > > A. start fixing some cases ('need topo sort' at least?) to improve
> > > testing area for the implementation,
> > >
> > > B. integrate solve() into Portage,
> > >
> > > C. maybe optionally integrate nsolve() into repoman.
> > >
> > > However, I don't want to set the spec into stone until we have
> > > some live testing via Portage with FEATURES=solve-required-use or
> > > alike. For repoman, we can add the verification optionally (i.e.
> > > with the above feature or via a separate command-line option) but
> > > I don't think we should enable it by default until we verify it.
> > >
> >
> > Yes, I agree. Since solve() and nsolve() are very related we should
> > carefully think how to organize the code then in order to avoid
> > duplication or them getting out of sync.
> >
> > As for enabling it into repoman, I'm not sure which is best. Safest
> > way is obviously as you suggest, but a warning is not a blocker, so
> > enabling it by default can have a nice effect of receiving hate
> > mails from angry developers if something is wrong.
> >
>
> There's wisdom in this as well. I'm just a little bit worried that
> we're first make developers change their REQUIRED_USE, and then have
> to change the algorithm anyway ;-).
Yeah, I wouldn't enable it without some good testing on the whole tree
and starting to deal with the annoying cases. But then I'd assume it'd
be good.
Alexis.
