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 4C657139694 for ; Wed, 7 Jun 2017 09:57:12 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 21AA721C1BE; Wed, 7 Jun 2017 09:57:03 +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 BE10221C07F for ; Wed, 7 Jun 2017 09:57:02 +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 7AF15341A60 for ; Wed, 7 Jun 2017 09:57:01 +0000 (UTC) Date: Wed, 7 Jun 2017 11:56:54 +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: <20170607115654.2a5da5e2@gentoo.org> In-Reply-To: <1496827679.2129.3.camel@gentoo.org> References: <1496071993.31087.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> <20170607101759.7e21f0f6@gentoo.org> <1496827679.2129.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: 4dc19da7-6a76-4a04-88a1-112d2ecbf958 X-Archives-Hash: 74011071c008d1ad2ad8ba1070a84b50 On Wed, 07 Jun 2017 11:27:59 +0200 Micha=C5=82 G=C3=B3rny wrote: > On =C5=9Bro, 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?=20 > >=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. =20 >=20 > What I mean is whether you can guarantee that: >=20 > a. for every X that nsolve(X) =3D=3D ok, solve() will be able to find > a valid solution, yes > b. for every X that solve() can solve reliably, nsolve(X) =3D=3D ok. no and that's not really possible > > 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). > >=20 > > The way I see it, REQUIRED_USE ast looks like: > > (assuming ^^ is already expanded to || + ??) > >=20 > > clause =3D > > AllOf(list of clauses) > > | AnyOf(list of clauses) > > | AtMostOne(list of clauses) > > | Implication(useflag, clause) > > | useflag > >=20 > > 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: > >=20 > > trueify(input, clause) =3D match clause with > > AllOf(l) -> for i in l: trueify(input, i) =20 > > > AnyOf(l) -> if not eval(input, clause): trueify(input, l[0]) > > > AtMostOne(l) -> f =3D (lambda x,y: pass) =20 > >=20 > > for i in l: > > f(input, i) > > if eval(input, i): f =3D falsify =20 > > > Implication(useflag, consequence) -> =20 > >=20 > > if input[useflag]: trueify(input, consequence) =20 > > > useflag -> input[useflag] =3D True =20 > >=20 > >=20 > > Now you see that for the AtMostOne case we need its dual, the > > 'falsify(input, clause)' function: > >=20 > > falsify(input, clause) =3D match clause with > > AllOf(l) -> falsify(input, l[0]) =20 >=20 > That's a debatable case. My solve() actually 'falsifies' all > the subexpressions which might be more reliable. Best way to debate this is probably to write the implication translation and feed that to nsolve from a few test cases. Intuition is that falsifying all of them adds more pressure on the solver and you might end up failing to solve it for no good reason, so falsifying only one of them seems safer. > > > AnyOf(l) -> for i in l: falsify(input, i) > > > AtMostOne(l) -> for i in l: =20 > >=20 > > if eval(input, clause): trueify(input, i) =20 >=20 > Do I read this correctly that it pretty much implies enabling the > first two subexpressions? or the leftmost first false if one is already true in there, yes > > > Implication(useflag, consequence) -> =20 > >=20 > > if not input[useflag]: raise "impossible" =20 >=20 > 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 it's really a corner case as I think we don't allow nested implications inside ||, ^^, () or ??, which is the only way to reach that. > > else: falsify(input, consequence) =20 > > > useflag -> input[useflag] =3D False =20 >=20 > Looks mostly sane. You've missed '!flag' but that's trivial to add. yeah, i realized after sending the email > >=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)" ). =20 >=20 > 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. > > 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. > >=20 > > 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). > > =20 >=20 > 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. Alexis.