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 35374139694 for ; Tue, 30 May 2017 08:56:29 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id C30B0E0ED8; Tue, 30 May 2017 08:56:20 +0000 (UTC) Received: from mail-wm0-x242.google.com (mail-wm0-x242.google.com [IPv6:2a00:1450:400c:c09::242]) (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 58833E0EA2 for ; Tue, 30 May 2017 08:56:20 +0000 (UTC) Received: by mail-wm0-x242.google.com with SMTP id g15so23554003wmc.2 for ; Tue, 30 May 2017 01:56:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20161025; h=date:from:to:subject:message-id:in-reply-to:references:mime-version :content-transfer-encoding; bh=Bg7o9P3Dd5jsrrGDT5tWnLVRgvNI4JZRhoJy0lC9/ec=; b=UfHNN8xrFfW9I6Sgs7B0Ar8jXEfgBqFZFhBY+8Zc2zlf9mYwIj0O2/SDPTOAqH3La9 OOkTqXfvEXYtFKY3VR/1Lxcb4+4yNZf8ToTJ+1RxyiLRvC2xxH5eBBfKUCGxwVB2rhyg GlMwtg1AJeB28rnMmxxlKvP63JMEL5Rm5ABfBEOMSsVbE1H/xd6oEun6Ssp7OA+rq9uz yl0eSjWC2G6qTH4o7rn5yhJtP1Mcer28ZQiopaw3P5zzLFGrC1df8otAHwyWZ8xwr9Ur q0gjR4WGBXl2HU9cTc4960xZ1xh/pjsoGE5ye5xJTfE6UzECVtxAXMtQjEezSPuD/MKO FVYQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:date:from:to:subject:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=Bg7o9P3Dd5jsrrGDT5tWnLVRgvNI4JZRhoJy0lC9/ec=; b=lKGF9vTnP/u9662vZrI9ir1EUWH7E8VYVdAJqVQ5U40tAXiq5yfrJ+VqLoJthR0RFZ fBoWYfWGze8sD8rB6J0QBdsGjajG7Zm9idk9pgtvHV4m/YB3uH5eFFysJs9aMq42TCrK wKI3c0001XDI4H32kaVKETe/mwADnCg/SPFwZFUvArC6zpRVr3ncLwMJTqTvccx5RWS1 T/ZyCPWnD2uvQMREEklYn4XfdZgewY49zQf/Jd2YHLpbSfMDdOiR6B5CQv36uzdVQtSp nT6UkTVuJGDv1pZIUSCrwM6B3o7/OhsKcwD/fc7pTma56PwrSZQVhZb1GFTLT20/ZT+I H4Gw== X-Gm-Message-State: AODbwcBlXgYaj7gQTkD8rdJJfrHkv1VlKAKZdI4GDTcdSFoo5r3Lly9+ 5Ytr6nH5LJDpSE+r X-Received: by 10.28.230.200 with SMTP id e69mr1016488wmi.70.1496134578653; Tue, 30 May 2017 01:56:18 -0700 (PDT) Received: from snowblower (cpc4-broo7-2-0-cust35.14-2.cable.virginm.net. [82.8.215.36]) by smtp.gmail.com with ESMTPSA id b78sm1132239wrd.29.2017.05.30.01.56.18 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Tue, 30 May 2017 01:56:18 -0700 (PDT) Date: Tue, 30 May 2017 09:56:07 +0100 From: Ciaran McCreesh To: gentoo-dev@lists.gentoo.org Subject: Re: [gentoo-dev] [RFC] Forced/automatic USE flag constraints (codename: ENFORCED_USE) Message-ID: <20170530095607.1adbc0b8@snowblower> In-Reply-To: <20170530104654.31b89e10@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> X-Mailer: Claws Mail 3.13.0 (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: 404765a2-ab31-4502-b104-566234549764 X-Archives-Hash: a24547ed76789d0d81677a0ab6985f57 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. -- Ciaran McCreesh