On Tue, 30 May 2017 20:11:38 +0200 Michał Górny <mgo...@gentoo.org> wrote: [...] > > > 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. > > > > Adding a 2^n check to repoman isn't gonna work well. > > > > 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. > > 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.
:) 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. 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. 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='foo -bar' in make.conf. This could be used to trigger a repoman warning but basically every single ebuild would trigger those.
