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 ACBB9139694 for ; Mon, 5 Jun 2017 17:24:49 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id BF251E0DC8; Mon, 5 Jun 2017 17:24:41 +0000 (UTC) Received: from smtp.gentoo.org (mail.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 67B9BE0DAC for ; Mon, 5 Jun 2017 17:24:41 +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 9A367341961 for ; Mon, 5 Jun 2017 17:24:39 +0000 (UTC) Date: Mon, 5 Jun 2017 19:24:33 +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: <20170605192433.6238797b@gentoo.org> In-Reply-To: <1496671825.1230.3.camel@gentoo.org> References: <1496071993.31087.1.camel@gentoo.org> <20170530095607.1adbc0b8@snowblower> <20170530112518.65b4f9e9@gentoo.org> <22829.24276.295.969060@a1i15.kph.uni-mainz.de> <1496154812.1238.5.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> 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: f237598f-bb72-4659-a117-787d08c96bde X-Archives-Hash: e2482b1c08fd6a843343e02a1ec40dc4 On Mon, 05 Jun 2017 16:10:25 +0200 Micha=C5=82 G=C3=B3rny wrote: > On pon, 2017-06-05 at 09:55 +0200, Alexis Ballier wrote: > > On Sun, 4 Jun 2017 10:59:38 +0200 > > Alexis Ballier wrote: > > =20 > > > Here's a quick n dirty code to play with, based on yours:=20 > > > https://github.com/aballier/required-use =20 > >=20 > > I've run that on the whole tree (considering all ebuilds with non > > empty REQUIRED_USE), some stats: > >=20 > > $ time python3 classify.py requsel=20 > > Stats: > > Parse error: 16 =20 >=20 > Hmm, how did you get those numbers? I just tested parsing and found > only 7 unique REQUIRED_USE entries that fail. However, my sample file > is only around 1000 entries long, so either I failed to get all of > them, or you didn't deduplicate your list ;-). More on it below. I did not deduplicate anything. I took every single ebuild and generated a list of req use out of it. Meaning if you had 10 ebuilds for 1 package with the same req use that'd count as 10 above. [...] > > The cycle is mostly due to: > > $ python3 nsolve.py 'llvm? ( gallium ) gallium? ( llvm )' > > [...] > > toposort.CircularDependencyError: Circular dependencies exist among > > these items: {[gallium]? =3D> [llvm]:{[llvm]? =3D> [gallium]}, [llvm]? > > =3D> [gallium]:{[gallium]? =3D> [llvm]}} > >=20 > >=20 > > This is something I had overseen when replacing 'a q'_j is some p_i > > and one of q_1 ... q_m might be false' by only 'a q'_j is some > > p_i'; it can be replaced without changing anything in the way PM > > would solve it by "a q'_j is some p_i and the set of {q_j} is not a > > subset of q' union p'" (that is, {q_i} is not trivially true if the > > 2nd clause is applied). Extending that, we get those stats: =20 >=20 > I'm not even trying to understand the things you say with indexes but > I trust you know what you're doing. With that kind of things it's good to have someone having a second look. It's so easy to forget a case or to miss a simplification. > For completeness, we need to > consider three cross-dependent states: >=20 > a. a? ( b ) b? ( a ) that's exactly the above :p {q_j} is {b}, {q'} is {a}, {p'} is {b}; {b} is a subset of {a} union {b} [...] > b. !a? ( !b ) !b? ( !a ) that's also the above with s/!b/b/ s/!a/a/ :=3D) > c. a? ( b ) !a? ( !b ) that's already handled. [...] > > I'll let you play with it, but for me it seems this would work quite > > nicely. > > =20 >=20 > Well, I guess it's time to hit the next level. For a start, we have to > handle all-of groups, i.e.: >=20 > ( a b c ) >=20 > Stand-alone makes little sense (and little trouble) but as you could > have seen it's used nested in other thingies: >=20 > 1. || ( ( a b ) ( c d ) e ) >=20 > 2. ?? ( ( a b ) ( c d ) e ) >=20 > 3. ^^ ( ( a b ) ( c d ) e ) Yeah that's the nesting problem causing a parse error. Those should be expanded to implications. What I'm relying onto is all clauses to be of the form '[list of conditions]? [list of constraints]' > For verifying constraints, they are not bad. We just follow the > generic rule that the branch evaluates to true if all subexpressions > are true.=C2=A0 >=20 > For solving, it might be a little unclear on how to proceed with > partially true branches but for the sake of simplicity I would just > ignore them and behave as if they were false. That is, case (1) with > USE=3D'c' would result in 'a b' being enabled. >=20 > The practical uses I've seen are: >=20 > a.=C2=A0|| ( deprecated ( gtk3 introspection ) ) >=20 > I guess this one would be equivalent to: >=20 > !gtk3? ( !introspection? ( deprecated ) ) Unfortunately no. Favoring leftmost, you need to enable 'deprecated' when either gtk3 or introspection is false. That'd be: !gtk3? ( deprecated ) !introspection? ( deprecated ) Fortunately we can distribute \/ and /\: || ( deprecated ( gtk3 introspection ) ) is equivalent to: || ( deprecated gtk3 ) || ( deprecated introspection ) giving the above implication translation. This can be extended to=20 || ( ( a1 a2 a3 ... ) ( b1 b2 b3 ... ) ... ) to handle all cases. > b. ^^ ( ( !32bit 64bit ) ( 32bit !64bit ) ( 32bit 64bit ) ) >=20 > This looks like a crazy way of saying: >=20 > || ( 32bit 64bit ) Hmm yes > c. ^^ ( ( !ruby !s7 ) ( ruby !s7 ) ( !ruby s7 ) ) >=20 > This looks like an insane version of: >=20 > ?? ( ruby s7 ) yes too it seems > except that per my solver it just disables both when both are set ;-). That's kind of the point. And that's why it is important to have the solving rules well defined. Depending on how REQUIRED_USE is written, it will be solved differently even for equivalent logical formulas. > Not sure if the extra complexity is worth for roughly one valid use > case, and a lot of insanity. I think this can be done without too much pain. As you noticed, replace '^^ ( whatever )' by '|| ( whatever ) ?? ( whatever )' so we're left with only || and ?? (and 'and' denoted by space and grouping in our notation). || ( clause1 clause2 ... ) is replaced by [!clause1 !clause2 ...]?[clause1] ?? ( clause1 clause2 ... ) is replaced by: [clause1]?[!clause2 !clause3 ...] [!clause1]?[ ?? ( clause2 clause3 ... ) ] ! (|| ( clause1 clause2 ... ) ) is '!clause1 !clause2 ...' (de morgan) ! ( clause1 clause2 ... ) is '|| ( !clause1 !clause2 ... )' (de morgan too) ! (?? ( clause1 clause2 ... ) ) could be written as 'clause1? ( || ( clause2 ... ) ) !clause1? ( ! ?? ( clause2 ... ) )' and I think that's it to allow expanding everything to implications. [ begin || ( clause1 clause2 ... ) end ]?[constraint] is: [ begin clause1 end]?[constraint] [ begin clause2 end]?[constraint] etc. [ begin ([icond]?[iconstraint]) end]?[constraint] is: [ begin icond]?[iconstraint] [ begin end]?[constraint] I think and [ begin ( clause1 clause2 ... ) end]?[constraint] is [ begin clause1 clause2 ... end]?[constraint] [...] > Of course past that there's a deeper insanity: all those constructs > can be nested without limits. Verification is possible, solving maybe > -- but I'm not sure if we even want to try to think what the correct > solution would be. We're good as long as they're rewritten as implications internally. > There's only one use of this: >=20 > ?? ( gl3plus ( || ( gles2 gles3 ) ) ) That'd be: gl3plus? ( ! || ( gles2 gles3 ) ) per the above reduced to: gl3plus? ( !gles2 !gles3 ) >=20 > FWICS, it probably works like this; >=20 > =C2=A0g=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0g=C2=A0=C2=A0=C2=A0=C2=A0 > =C2=A0l=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0l=C2=A0=C2=A0=C2=A0=C2=A0 > =C2=A03 g g=C2=A0=C2=A0=C2=A03 g g > =C2=A0p l l=C2=A0=C2=A0=C2=A0p l l > =C2=A0l e e=C2=A0=C2=A0=C2=A0l e e > =C2=A0u s s=C2=A0=C2=A0=C2=A0u s s > =C2=A0s 2 3 | s 2 3 > =C2=A00 0 0 | 0 0 0 (=3D=3D) > =C2=A00 0 1 | 0 0 1 (=3D=3D) > =C2=A00 1 0 | 0 1 0 (=3D=3D) > =C2=A00 1 1 | 0 1 1 (=3D=3D) > =C2=A01 0 0 | 1 0 0 (=3D=3D) > =C2=A01 0 1 | 1 0 1 [unsolvable due to loop] > =C2=A01 1 0 | 1 1 0 [unsolvable due to loop] > =C2=A01 1 1 | 1 1 1 [unsolvable due to loop] >=20 > i.e. it would be equivalent to: >=20 > gl3plus? ( !gles2 !gles3 ) >=20 > unless the author meant something else and failed. Exactly. I don't know why you see a loop. > 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. I don't think it is *that* insane to support nesting :) Alexis.