From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id 61218139694 for ; Wed, 7 Jun 2017 08:18:16 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 81AC8E0FAE; Wed, 7 Jun 2017 08:18:07 +0000 (UTC) Received: from smtp.gentoo.org (dev.gentoo.org [IPv6:2001:470:ea4a:1:5054:ff:fec7:86e4]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 26735E0FAA for ; Wed, 7 Jun 2017 08:18:07 +0000 (UTC) Received: from localhost (unknown [IPv6:2a01:e34:eeaa:6bd0:4ecc:6aff:fe03:1cfc]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) (Authenticated sender: aballier) by smtp.gentoo.org (Postfix) with ESMTPSA id 381FD341A26 for ; Wed, 7 Jun 2017 08:18:05 +0000 (UTC) Date: Wed, 7 Jun 2017 10:17:59 +0200 From: Alexis Ballier To: gentoo-dev@lists.gentoo.org Subject: Re: [gentoo-dev] [RFC] Forced/automatic USE flag constraints (codename: ENFORCED_USE) Message-ID: <20170607101759.7e21f0f6@gentoo.org> In-Reply-To: <1496770744.1157.1.camel@gentoo.org> References: <1496071993.31087.1.camel@gentoo.org> <20170530173340.0b575526@gentoo.org> <1496167898.1335.1.camel@gentoo.org> <20170530204614.61e8e42c@gentoo.org> <1496213717.1164.1.camel@gentoo.org> <20170531093257.23b66f88@gentoo.org> <1496217792.1164.5.camel@gentoo.org> <20170531103819.417c2420@gentoo.org> <1496235892.25038.1.camel@gentoo.org> <20170531193922.477245bb@gentoo.org> <1496257344.25758.1.camel@gentoo.org> <20170601105523.08a9234e@gentoo.org> <1496352685.30502.4.camel@gentoo.org> <20170602132758.50a5f734@gentoo.org> <1496411717.29233.5.camel@gentoo.org> <20170603130000.4f88fb14@gentoo.org> <1496503989.15351.1.camel@gentoo.org> <20170603185835.57741ff0@gentoo.org> <20170604105938.2b40157f@gentoo.org> <20170605095516.0b463432@gentoo.org> <1496671825.1230.3.camel@gentoo.org> <20170605192433.6238797b@gentoo.org> <1496686212.1222.4.camel@gentoo.org> <20170606140803.051f8048@gentoo.org> <1496770744.1157.1.camel@gentoo.org> Organization: Gentoo X-Mailer: Claws Mail 3.15.0-dirty (GTK+ 2.24.31; x86_64-pc-linux-gnu) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-dev@lists.gentoo.org Reply-to: gentoo-dev@lists.gentoo.org MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Archives-Salt: d84d2ecc-569c-4445-a400-cef448c79788 X-Archives-Hash: dada16dd748e842189aaa6d3905f2a85 On Tue, 06 Jun 2017 19:39:04 +0200 Micha=C5=82 G=C3=B3rny wrote: > > [...] =20 > > > > > The question is whether we want to: > > > > >=20 > > > > > a. actually try to solve this nesting insanity, > > > > >=20 > > > > > b. declare it unsupported and throw REQUIRED_USE mismatch on > > > > > user, > > > > >=20 > > > > > c. ban it altogether. =20 > > > >=20 > > > >=20 > > > > I don't think it is *that* insane to support nesting :) > > > > =20 > > > > > ( ^^ ( ?? ( a b ) c ( d e ) ) f ) =20 > >=20 > > 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 ;) > > =20 >=20 > 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 ;-). >=20 > 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. >=20 > 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? ;-) >=20 > Also, do I presume correctly that for all supported cases (i.e. those > which your nsolve does not reject), solve and nsolve are compatible? >=20 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 =3D 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) =3D 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 =3D (lambda x,y: pass) for i in l: f(input, i) if eval(input, i): f =3D falsify | Implication(useflag, consequence) -> if input[useflag]: trueify(input, consequence) | useflag -> input[useflag] =3D True Now you see that for the AtMostOne case we need its dual, the 'falsify(input, clause)' function: falsify(input, clause) =3D 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] =3D False =20 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=3D"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] =3D True; input[bar] =3D False if baz: if biz: input[x] =3D 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 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). Bests, Alexis.