On Thu, 15 Jun 2017 17:32:40 +0100 Ciaran McCreesh <ciaran.mccre...@googlemail.com> wrote:
> On Thu, 15 Jun 2017 18:30:10 +0200 > Alexis Ballier <aball...@gentoo.org> wrote: > > On Thu, 15 Jun 2017 17:22:26 +0100 > > Ciaran McCreesh <ciaran.mccre...@googlemail.com> wrote: > > > On Thu, 15 Jun 2017 18:19:04 +0200 > > > Alexis Ballier <aball...@gentoo.org> wrote: > > > > On Thu, 15 Jun 2017 17:13:57 +0100 > > > > Ciaran McCreesh <ciaran.mccre...@googlemail.com> wrote: > > > > > On Thu, 15 Jun 2017 18:07:00 +0200 > > > > > Alexis Ballier <aball...@gentoo.org> wrote: > > > > > > > The best way to convince me is through valid > > > > > > > examples. > > > > > > > > > > > > It is also easier to be convinced when you try to understand > > > > > > and ask for clarifications instead of just rejecting without > > > > > > thinking :) > > > > > > > > > > The problem with this entire proposal is that it's still in > > > > > "well I can't think of how it could possibly go wrong" > > > > > territory. We need a formal proof that it's sound. History has > > > > > shown that if something can be abused by Gentoo developers, it > > > > > will be abused... > > > > > > > > Had you read the thread you would have noticed that I provided > > > > an algorithm giving sufficient conditions for the solver to > > > > work. That is, if developers pay attention to repoman > > > > warnings/errors, it will never fail. Obviously, since we're > > > > still in the SAT space, you can ignore the errors and make it > > > > fail, but it'll never be worse than what we currently > > > > have. > > > > > > You have shown that you produce a solution, not the solution > > > that's actually wanted. > > > > Since 'wanted' is still undefined, I'd say it produces the defined > > solution and you can adapt to the definition to get what you want. > > So you're saying that at the end of this, there's an ENFORCED_USE > solver that spits out some answer that may or may not be in any way a > sane solution to the conflict. > > I don't see how that's helpful to a user. > Define sane. The definition of the solver is made to change the least possible of the inputs and is completely and easily predictable by the person writing the constraint. That is something I would call sane.
