On śro, 2017-06-14 at 15:16 +0200, Alexis Ballier wrote: > On Wed, 14 Jun 2017 14:24:48 +0200 > Michał Górny <mgo...@gentoo.org> 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 <mgo...@gentoo.org> 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 <mgo...@gentoo.org> 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 additional > > transformations. > > Then I already explained how to make it work. > > Transformations are out of scope of the spec and more for improving > code sharing: Those are required for checking that the solver will > provide a proper solution; if there is some flaw or undefined behavior > in the spec, then solve() might change, if both the solver and the > checker work on the same input data then at least there won't be some > desynchronization between them. solve.py now verifies that the result with transformations is the same as without transformations. That should help us keep the code in sync. > [...] > > > > > > [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. If you want to play with it more, then please by all means do so. 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. This also means writing the spec to account for all the corner cases you need accounting for, and convincing people for every arbitrary restriction you need to enforce to make things work. Like expecting most of the ebuilds to use the same flag order in ^^ or otherwise USE dependencies will just explode in their faces. -- Best regards, Michał Górny
signature.asc
Description: This is a digitally signed message part
