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 73DB6139694 for ; Tue, 30 May 2017 09:26:09 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id E72AA21C0CC; Tue, 30 May 2017 09:25:28 +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 9507E21C0AB for ; Tue, 30 May 2017 09:25:28 +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 0512A3416C2 for ; Tue, 30 May 2017 09:25:26 +0000 (UTC) Date: Tue, 30 May 2017 11:25:18 +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: <20170530112518.65b4f9e9@gentoo.org> In-Reply-To: <20170530095607.1adbc0b8@snowblower> 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> 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=US-ASCII Content-Transfer-Encoding: 7bit X-Archives-Salt: 42e6827e-22ee-4edc-b657-d7beadb7ae22 X-Archives-Hash: 7dea7beffb29f16df1d6fce5b9ff75b9 On Tue, 30 May 2017 09:56:07 +0100 Ciaran McCreesh wrote: > On Tue, 30 May 2017 10:46:54 +0200 > Alexis Ballier wrote: > > On Tue, 30 May 2017 09:22:45 +0100 > > Ciaran McCreesh wrote: > > > On Tue, 30 May 2017 09:42:45 +0200 > > > Alexis Ballier wrote: > > > > Oh crap, this requires to solve SAT. > > > > > > The main problem would not be solving SAT, in this case. The > > > problem is providing the right answer when not enough information > > > is given. Spitting out a resolution which satisfies every > > > dependency isn't typically that difficult. Spitting out a > > > resolution which doesn't just turn off all your use flags and > > > uninstall most of your programs is the hard part. > > > > I don't really understand here: Assuming the formula is reduced > > where user-set useflags and profile-masked/forced ones are already > > assigned their true/false values, this leaves a formula with > > variables where changing any of those won't turn off (or on) > > anything you didn't want. If you can solve SAT on this reduced > > instance then you're safe, aren't you ? > > First problem: encoding "don't change this from its current setting > unless you have a reason to do so" is an utter pain in SAT. There are > other models like ASP that can just about get around this, but > expressing it properly is best done by just writing your own solver. > Remember that you have to allow the solver to toggle some flags, so > you can't just lock everything, but at the same time, you don't want > the solver to randomly toggle a flag that isn't specified by the user > or the profile, unless it absolutely has a good reason to do so. > > Second problem: a solver will spit out an arbitrary solution. If the > user then runs it again, there's no guarantee that it will spit out > the same arbitrary solution. That can be addressed by the right > choice of restart policies and tiebreaking etc if you're prepared to > muck around with the solver enough. But even if you do, suppose the > user thinks "yes, that's almost fine, but let me change one other > thing" (or if the install fails half-way through and the user tries > to carry on after fixing it). The solver will then spit out a totally > different arbitrary solution that looks nothing like the first one. The way I see it, this boils down to spec'ing something that guarantees there's a unique solution given an input. The solution does not have to be good or bad (we don't have a good metric on that anyway), it just has to be deterministic so that developers can arrange their REQUIRED_USE constraints to have PM chose the proper solution. Note: To me, the problems you describe are really the root of SAT solving problems (or any NP problem FWIW): An algorithm has to make choices that might have consequences arbitrary far and it might realize after running for a while that its initial assumption was invalid.