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 50EF2139694 for ; Wed, 7 Jun 2017 09:28:31 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 8986B21C1BE; Wed, 7 Jun 2017 09:28:14 +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 3800721C07F for ; Wed, 7 Jun 2017 09:28:14 +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 7C577341A20; Wed, 7 Jun 2017 09:28:12 +0000 (UTC) Message-ID: <1496827679.2129.3.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, 07 Jun 2017 11:27:59 +0200 In-Reply-To: <20170607101759.7e21f0f6@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> <20170607101759.7e21f0f6@gentoo.org> Organization: Gentoo Content-Type: multipart/signed; micalg="pgp-sha512"; protocol="application/pgp-signature"; boundary="=-/L6eTstQh7sLjXEyL8TE" 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: d59c1909-ce1f-4584-9042-f7360f259acd X-Archives-Hash: ef2e3176f2d0bde59b5f3347e0bed501 --=-/L6eTstQh7sLjXEyL8TE Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. What I mean is whether you can guarantee that: a. for every X that nsolve(X) =3D=3D ok, solve() will be able to find a valid solution, b. for every X that solve() can solve reliably, nsolve(X) =3D=3D ok. > 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) > > AnyOf(l) -> if not eval(input, clause): trueify(input, l[0]) > > AtMostOne(l) -> f =3D (lambda x,y: pass) >=20 > for i in l: > f(input, i) > if eval(input, i): f =3D falsify > > Implication(useflag, consequence) -> >=20 > if input[useflag]: trueify(input, consequence) > > useflag -> input[useflag] =3D True >=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]) That's a debatable case. My solve() actually 'falsifies' all the subexpressions which might be more reliable. > > AnyOf(l) -> for i in l: falsify(input, i) > > AtMostOne(l) -> for i in l: >=20 > if eval(input, clause): trueify(input, i) Do I read this correctly that it pretty much implies enabling the first two subexpressions? > > Implication(useflag, consequence) -> >=20 > if not input[useflag]: raise "impossible" Why impossible? Unless I'm missing something, it's false already. > else: falsify(input, consequence) > > useflag -> input[useflag] =3D False Looks mostly sane. You've missed '!flag' but that's trivial to add. >=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)" ). You need to be able to reorder the clauses to handle use.force and use.mask. > 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 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. Preferably it should also be as simple as possible to avoid putting too much complexity in the spec. --=20 Best regards, Micha=C5=82 G=C3=B3rny --=-/L6eTstQh7sLjXEyL8TE 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+0Rk4FAlk3xx9fFIAAAAAALgAo aXNzdWVyLWZwckBub3RhdGlvbnMub3BlbnBncC5maWZ0aGhvcnNlbWFuLm5ldDZE QkIwN0NDNEYwREFEMDZFQTBBRkU0MUIwN0ExQUVBRUZCNDQ2NEUSHG1nb3JueUBn ZW50b28ub3JnAAoJELB6GurvtEZOtucQAMx7CUjk9LlDlfwablH3yFZm34RpWG91 0eQ7r1BJz0F/zINGAl+//2M1I36wHXNxq4Vlz3hiKcHEq394J2z78hc3mjU820eq oorS2FmXLe+jCFZALgcZ71+co9WOujJ5z/uRZ6Wm+Pp854c1S2NNrTtFlsp1xE6v Zxpovjxt+6hn9ZHTXmSailQT0R+ygrxxoRlCV4DdfcWbsvUIl1hJDpUnfiUH7AYP eb3IvB+8mYaskAlqgA9b3reRjCdPTKdReJ3BZsnOj81ww8o1ZDymVaMW65f/AtEU 2vc/OebN7VevFlRvHZhBb4VKp6/cbKbGfzsWqtblk9U8mZW+j+IkQ4fJorcdF63z HgZUVb7NJmaJXdjIj6y9+YTtJ+ChffxX5fsEH2gYD6itWDvl2MhYwUhAzfq/VClx GL2PteB9yF8kvJInR5RXsV7DroXQwEPXLDRXkZyoTl0Skjsgvkosykf3ZjJFmcvT ClVpbHmjtzexN33k1OWAAPtjEmX6PyaTjQ+jPbwhl+MUNi7yBt/lIBma8j+oLHOa 35yr6KBwkjwnnPE/S7ILHIwwb+hTV4Yz2nC3OqXDe1XTVrwfhbOyixziyY4teZ2+ 6D1WKtJFKt7nosAhLknr0SxzoQ1vwrQiobzBqxAkkH+sD9FmYzt0KwgBFwtRyESn TatTYrl0hoaJ =9LHG -----END PGP SIGNATURE----- --=-/L6eTstQh7sLjXEyL8TE--