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 E0387139694 for ; Fri, 9 Jun 2017 09:19:46 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 7EB2DE0E56; Fri, 9 Jun 2017 09:19:38 +0000 (UTC) Received: from smtp.gentoo.org (smtp.gentoo.org [140.211.166.183]) (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 212BCE0C64 for ; Fri, 9 Jun 2017 09:19:38 +0000 (UTC) Received: from pomiot (d202-252.icpnet.pl [109.173.202.252]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) (Authenticated sender: mgorny) by smtp.gentoo.org (Postfix) with ESMTPSA id ABC873418A2; Fri, 9 Jun 2017 09:19:36 +0000 (UTC) Message-ID: <1496999960.29391.1.camel@gentoo.org> Subject: Re: [gentoo-dev] [RFC] Forced/automatic USE flag constraints (codename: ENFORCED_USE) From: =?UTF-8?Q?Micha=C5=82_G=C3=B3rny?= To: gentoo-dev@lists.gentoo.org Date: Fri, 09 Jun 2017 11:19:20 +0200 In-Reply-To: <20170607115654.2a5da5e2@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> <20170607115654.2a5da5e2@gentoo.org> Organization: Gentoo Content-Type: multipart/signed; micalg="pgp-sha512"; protocol="application/pgp-signature"; boundary="=-CRlY1az78hEVsn7u4SVz" X-Mailer: Evolution 3.22.6 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 X-Archives-Salt: a23901b8-f79a-4399-8222-14dd5e3ac8c4 X-Archives-Hash: ecd3495408606ea5a7c1e0fe5b70c628 --=-CRlY1az78hEVsn7u4SVz Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On =C5=9Bro, 2017-06-07 at 11:56 +0200, Alexis Ballier wrote: > On Wed, 07 Jun 2017 11:27:59 +0200 > Micha=C5=82 G=C3=B3rny wrote: >=20 > > 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, >=20 > yes >=20 > > b. for every X that solve() can solve reliably, nsolve(X) =3D=3D ok. >=20 > 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? b. for all 'need toposort' results, the solve() should be able to find a solution with n>=3D1 iterations? c. all of 'circular' results have at least one USE flag combination that can not be solved by solve()? > > > 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. >=20 > Best way to debate this is probably to write the implication > translation and feed that to nsolve from a few test cases. Exactly my thought. Since both algorithms should be kept in sync, it probably makes sense to figure out the translation first and use whatever makes it consistent without hacking on the translation hard. I'll try to figure it out on paper today. > 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. In either case, it's purely a matter of contract. You can't predict which one will be more correct, and I think it's hard to even predict which one developers will consider less surprising. Besides, the all cases we had for this were pretty much meaningless, and choosing A over B would only result in preferring clause X over Y ;-). >=20 > > > > 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? >=20 > or the leftmost first false if one is already true in there, yes >=20 > > > > Implication(useflag, consequence) -> =20 > > >=20 > > > if not input[useflag]: raise "impossible" =20 > >=20 > > Why impossible? Unless I'm missing something, it's false already. >=20 > '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'. > 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. Strictly speaking, there's no rule prohibiting that. And I think we actually have or had used 'foo?' inside '||' at least in dependencies. The basic idea is that if the flag is disabled, the contents disappear from the containing '||' block. Now, this makes a lot of things harder. For plain solve(), it's not a major problem -- worst case, we put an extra reordering on each iteration based on enabled USE flags. For nsolve(), it's harder since it makes the iteration graph PITA. I'll have to think if we can even translate it reasonably. > > >=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. >=20 > 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. > > > 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. >=20 > Yep, that's the point of nsolve/classify :) >=20 > > Preferably it should also be as simple as possible to avoid putting > > too much complexity in the spec. >=20 > Yes; not sure if anything simpler than the above can be achieved though. >=20 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=3Dsolve-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. --=20 Best regards, Micha=C5=82 G=C3=B3rny --=-CRlY1az78hEVsn7u4SVz Content-Type: application/pgp-signature; name="signature.asc" Content-Description: This is a digitally signed message part Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iQKmBAABCgCQFiEEbbsHzE8NrQbqCv5BsHoa6u+0Rk4FAlk6aBhfFIAAAAAALgAo aXNzdWVyLWZwckBub3RhdGlvbnMub3BlbnBncC5maWZ0aGhvcnNlbWFuLm5ldDZE QkIwN0NDNEYwREFEMDZFQTBBRkU0MUIwN0ExQUVBRUZCNDQ2NEUSHG1nb3JueUBn ZW50b28ub3JnAAoJELB6GurvtEZO1bIQAMX2tOi/q/el0qrzdktxXykMVFn3GdVO AuRkLj/XbKQn9fyXgDd5RHFmpjPnWkIhpfvUMI0YGdvCyo7qjxJgAQLeVMOqm5w7 hh7eqF7iudfDGraIDONxFDYml6+IpjF6FyL8bgM751EX19Sjk6VEX5WZ2/dhQlzu /KCjx6cveNXKet9a/xQB0PvRLlVHiE9tOe2Qh7f4iu+P04XyzRL/K4N7/VfPm/nH ESrBnibVgd/FVZlKRx+tmRaN20Bj3xDtUaK0fkvqMszeXPJ6kTWwjw9EN/SuaMGK bP/r02MAyHWlyWUTz0FIRR4EAo7EkMUbq7GEaJeHPeBKo2Z8Px3vwvY0MMniEAQ3 VpwvuAH1oR9N1TLAwWkvD2VfB4IKosgjsGtih76Y43XrsgU91Gv+1HDALQUbhUDR xLGouX/74ys2RlHHVUeYjlKMxeL8IAgw70+JVJcjlP4pp98v1RSOKuTQ82/NrSyK ufakcOWAyCyeioYNf5poP8287BJVvhB95OSOLN/LKZi6SeR//jYUUSjoUciJvgWh Nhwyc2hjWZc5nsRSzM2hhYTy4TWJybXyYxV1ikI6OLXSysVn9sqvpf0SAl+1LtoZ H9nJM0OMx3L33Y8EWNIsuJNVorhfQXMtRrH7aL8E2wI9jcCB/dBNXtHqQpjP565g VJap5+qMTVik =zmRJ -----END PGP SIGNATURE----- --=-CRlY1az78hEVsn7u4SVz--