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 A380B139694 for ; Wed, 31 May 2017 08:03:42 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 4E6FFE0E9B; Wed, 31 May 2017 08:03:34 +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 E9951E0E93 for ; Wed, 31 May 2017 08:03:33 +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 2980B341709; Wed, 31 May 2017 08:03:31 +0000 (UTC) Message-ID: <1496217792.1164.5.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: Wed, 31 May 2017 10:03:12 +0200 In-Reply-To: <20170531093257.23b66f88@gentoo.org> References: <1496071993.31087.1.camel@gentoo.org> <20170529200037.2559f80a@gentoo.org> <1496093035.12795.3.camel@gentoo.org> <20170530094245.40e1cf64@gentoo.org> <20170530092245.681d4aeb@snowblower> <20170530104654.31b89e10@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> Organization: Gentoo Content-Type: multipart/signed; micalg="pgp-sha512"; protocol="application/pgp-signature"; boundary="=-lW0l8dsYOshNx5Ju/16O" 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: 5c6a9ebf-e9c8-4e25-a634-35955aa0b749 X-Archives-Hash: e89d18046777188b59c54926c357b898 --=-lW0l8dsYOshNx5Ju/16O Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On =C5=9Bro, 2017-05-31 at 09:32 +0200, Alexis Ballier wrote: > On Wed, 31 May 2017 08:55:17 +0200 > Micha=C5=82 G=C3=B3rny wrote: >=20 > > On wto, 2017-05-30 at 20:46 +0200, Alexis Ballier wrote: > > > On Tue, 30 May 2017 20:11:38 +0200 > > > Micha=C5=82 G=C3=B3rny wrote: > > > [...] =20 > > > > > > Of course, we could just validate all the possible cases via > > > > > > repoman, and reject the ebuild if there's at least one > > > > > > conflict between them. Not sure how to express that properly > > > > > > in the spec though. Not sure how it would work > > > > > > practically. =20 > > > > >=20 > > > > > Adding a 2^n check to repoman isn't gonna work well. > > > > > =20 > > > >=20 > > > > I'm not saying it's the most optimal algorithm of verifying > > > > the correctness of the constraints. It's just the one that's quite > > > > obvious -- relatively simple and reliable. If someone can come up > > > > with something better that covers at least the most common cases, > > > > I'm all for it. > > > >=20 > > > > That said, this wouldn't be that much of a problem if we can keep > > > > the n low. For a start, we can rule out all flags that don't > > > > appear in REQUIRED_USE at all. Furthermore, I think we could also > > > > ignore the constraints for flags that don't appear there at least > > > > 'twice', and so on. =20 > > >=20 > > > :) > > >=20 > > > You're applying classical techniques to lower the size of a SAT > > > instance so that your exponential algorithm does not explode, but > > > it's still hard. > > >=20 > > > I'm not sure what you want: If you want to detect that there is an > > > impossible constraint, well, ebuild writer will notice soon enough > > > when testing it. If you want to detect that there is a way to have a > > > conflict between useflags, then there will be valid cases where this > > > will happen. > > >=20 > > > That said, assuming we have REQUIRED_USE in CNF form, its negation > > > is in DNF form. Solving SAT on DNF formulas is easy (linear I > > > think), and this would give you an assignment of useflags > > > triggering an impossible constraint. e.g. 'foo? ( bar )' with > > > USE=3D'foo -bar' in make.conf. This could be used to trigger a > > > repoman warning but basically every single ebuild would trigger > > > those. =20 > >=20 > > Not sure if we understand each other. > >=20 > > I'd like the constraints to be plain straightforward, to the point of > > having only one acceptable solution. No special Portage-style > > algorithms that attempt to provide a reasonable solution to > > unreasonable input, resulting in horrible solutions that need 20 more > > hacks every few months. >=20 > Yes, we definitely agree here. For that, you need to kill the SAT > solver and define (spec) what is the straightforward solution, aka a > deterministic and straightforward (*) algorithm. Otherwise, you fall > into the problems Ciaran explained in an earlier email. >=20 >=20 > (*) It's better for the algorithm to be simple enough so that > REQUIRED_USE can be written easily for achieving a given behavior. >=20 >=20 > > For example: > >=20 > > foo? ( bar ) > >=20 > > would mean 'if you have USE=3Dfoo, then USE=3Dbar is enabled as well'. = Not > > 'find some random solution which satisfies this'. In other words, here > > changing USE=3Dfoo into USE=3D-foo is not an acceptable solution. >=20 >=20 > What if I specifically set USE=3D-bar in make.conf ? Do we really want PM > to override that without telling me ? Yes. Unless you specifically and explicitly disable that (globally or for USE=3Dbar), in which case the PM would just reject to proceed. > I believe that, from the ebuild POV, the ternary useflag model is more > appropriate: You have a whole bunch of ways to specify useflags with > portage (make.conf, package.use, profiles, command line, ...). From the > ebuild those are collapsed into 'user input'. You only have IUSE (with > its defaults) and that's what the auto-solver should play with: those > are the flags that can be toggled. I see your point. However, it's merely a preference problem and we really don't want the constraints to become ternary and/or PM try to force the reverse solutions. That's an easy way to lose predictability. Besides, I should point out that USE_EXPAND in make.profile and make.conf are strictly binary. Furthermore, the ternary idea starts becoming blurry when you have to deal with profiles that you explicitly want to disable in user configuration. > > Now, this also means that every constraint that can't be solved in > > this easy fashion is invalid. We want to detect that, and warn the > > developer. Some of those could be tricky. Simple example: > >=20 > > foo? ( baz ) bar? ( !baz ) > >=20 > > This one is invalid because USE=3D'foo bar' requires both 'baz' and > > '!baz' as a solution. Remember that we don't want to do any changes > > besides what's explicitly written there, no guessing. >=20 > Besides that, what makes it invalid ? What makes it invalid is that you can't solve it in a predictable way. > How is it more invalid than '?? ( foo bar )' ? This would go into: foo? ( !bar ) which gives a single predictable solution: foo bar -> foo bar F F -> [valid] F T -> [valid] T F -> [valid -- matches constraint] T T -> T F Note that to preserve predictability you need to always leave out the last bit, i.e. ?? ( a b c ) would go into: a? ( !b !c ) b? ( !c ) a b c -> a b c F F F -> [valid] F F T -> [valid] F T F -> [valid -- matches constraint] F T T -> F T F T F F -> [valid -- matches constraint] T F T -> T F F T T F -> T F F T T T -> T F F And so on. >=20 > > However, the > > following should be valid: > >=20 > > foo? ( baz ) bar? ( !foo !baz ) > >=20 > > Because now we clearly indicate that USE=3Dbar disables USE=3Dfoo, > > and therefore makes the first constraint inapplicable. It clearly > > indicates course of action for all combinations: >=20 > Ok, I now think you're aiming for giving full power to the solver, > overriding user inputs if necessary. Before going further, I think we > should first agree on what are the useflags such a solver can toggle. > I'm not sure 'USE=3Dfoo emerge blah' should disable foo instead of > failing for example. >=20 As I said, it's a matter of configuration to decide which flags should be touched, and which not. Of course if we find that necessary, we may go into defining a specific set in the profiles or metadata. However, I would rather focus on getting a PoC solver and checker first, and play with existing constraints to see how it all works. --=20 Best regards, Micha=C5=82 G=C3=B3rny --=-lW0l8dsYOshNx5Ju/16O 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+0Rk4FAlkueMJfFIAAAAAALgAo aXNzdWVyLWZwckBub3RhdGlvbnMub3BlbnBncC5maWZ0aGhvcnNlbWFuLm5ldDZE QkIwN0NDNEYwREFEMDZFQTBBRkU0MUIwN0ExQUVBRUZCNDQ2NEUSHG1nb3JueUBn ZW50b28ub3JnAAoJELB6GurvtEZOMN8P/1G9FfpM9wT6cDzK6mRRh733/n017iUs 1OaaXIP5NkJNoq4jAn8LnQ0jGPLeQDtK9lI25EfOK43vjg+A5+1gc/VCE4ry059t sJF6BdNoAYIcPyjIyKTg7jt9sSPZ5xq92iQ5MFHJKSLgLKGEoA44aBDj7cu8elvF sfAxv4DtZaxNB6zlJbVlzwYELtf+uKjEMBEfQX24HWXQ5eLYSnC/FmezsOoCfzfJ qOFsSuEYc65uZiL1naaY3Vjap+bk/1v70PwKWdOHvbo/vEqRMchpCgFAO2I30m52 Y3TZSCvIpKwYr3Obm3sPo3+XRLeNl9hfUk8r4TYvjeMOQ4puMiA+GT/zfejsqtR6 7iFs5p/1cPeNMvbJbd8dGwpEUF8pTLui6m7zDMRM4q5Ybofxz6iaY6lpN7Wtmrhw +zgIHvrORcSY0dHYLt+Q9Ch0XhBA4zT1vtXs/hTac7aGEb2B7I8sZHWu3FUA09m4 obFpLuLp4a97u/qLLpyKv7uADRitPgsM/CiX2atPA2jWfe5cWgL46NDW7Ss70bMI kbSefPdte7Qv1ebxByUef6lbhGe17c+2BQR0sJCTgZtMDpf4B+knXVvOMD3rYPH3 gxhGqHg5tKiOUjOHjO+sFEjIkOIZtgc7JTtMJoxwrugC+9DQj2DhZ/UoyTMUIoc5 Ge55efzaH54t =UBjy -----END PGP SIGNATURE----- --=-lW0l8dsYOshNx5Ju/16O--