1 |
On Wed, 31 May 2017 08:55:17 +0200 |
2 |
Michał Górny <mgorny@g.o> wrote: |
3 |
|
4 |
> On wto, 2017-05-30 at 20:46 +0200, Alexis Ballier wrote: |
5 |
> > On Tue, 30 May 2017 20:11:38 +0200 |
6 |
> > Michał Górny <mgorny@g.o> wrote: |
7 |
> > [...] |
8 |
> > > > > Of course, we could just validate all the possible cases via |
9 |
> > > > > repoman, and reject the ebuild if there's at least one |
10 |
> > > > > conflict between them. Not sure how to express that properly |
11 |
> > > > > in the spec though. Not sure how it would work |
12 |
> > > > > practically. |
13 |
> > > > |
14 |
> > > > Adding a 2^n check to repoman isn't gonna work well. |
15 |
> > > > |
16 |
> > > |
17 |
> > > I'm not saying it's the most optimal algorithm of verifying |
18 |
> > > the correctness of the constraints. It's just the one that's quite |
19 |
> > > obvious -- relatively simple and reliable. If someone can come up |
20 |
> > > with something better that covers at least the most common cases, |
21 |
> > > I'm all for it. |
22 |
> > > |
23 |
> > > That said, this wouldn't be that much of a problem if we can keep |
24 |
> > > the n low. For a start, we can rule out all flags that don't |
25 |
> > > appear in REQUIRED_USE at all. Furthermore, I think we could also |
26 |
> > > ignore the constraints for flags that don't appear there at least |
27 |
> > > 'twice', and so on. |
28 |
> > |
29 |
> > :) |
30 |
> > |
31 |
> > You're applying classical techniques to lower the size of a SAT |
32 |
> > instance so that your exponential algorithm does not explode, but |
33 |
> > it's still hard. |
34 |
> > |
35 |
> > I'm not sure what you want: If you want to detect that there is an |
36 |
> > impossible constraint, well, ebuild writer will notice soon enough |
37 |
> > when testing it. If you want to detect that there is a way to have a |
38 |
> > conflict between useflags, then there will be valid cases where this |
39 |
> > will happen. |
40 |
> > |
41 |
> > That said, assuming we have REQUIRED_USE in CNF form, its negation |
42 |
> > is in DNF form. Solving SAT on DNF formulas is easy (linear I |
43 |
> > think), and this would give you an assignment of useflags |
44 |
> > triggering an impossible constraint. e.g. 'foo? ( bar )' with |
45 |
> > USE='foo -bar' in make.conf. This could be used to trigger a |
46 |
> > repoman warning but basically every single ebuild would trigger |
47 |
> > those. |
48 |
> |
49 |
> Not sure if we understand each other. |
50 |
> |
51 |
> I'd like the constraints to be plain straightforward, to the point of |
52 |
> having only one acceptable solution. No special Portage-style |
53 |
> algorithms that attempt to provide a reasonable solution to |
54 |
> unreasonable input, resulting in horrible solutions that need 20 more |
55 |
> hacks every few months. |
56 |
|
57 |
Yes, we definitely agree here. For that, you need to kill the SAT |
58 |
solver and define (spec) what is the straightforward solution, aka a |
59 |
deterministic and straightforward (*) algorithm. Otherwise, you fall |
60 |
into the problems Ciaran explained in an earlier email. |
61 |
|
62 |
|
63 |
(*) It's better for the algorithm to be simple enough so that |
64 |
REQUIRED_USE can be written easily for achieving a given behavior. |
65 |
|
66 |
|
67 |
> For example: |
68 |
> |
69 |
> foo? ( bar ) |
70 |
> |
71 |
> would mean 'if you have USE=foo, then USE=bar is enabled as well'. Not |
72 |
> 'find some random solution which satisfies this'. In other words, here |
73 |
> changing USE=foo into USE=-foo is not an acceptable solution. |
74 |
|
75 |
|
76 |
What if I specifically set USE=-bar in make.conf ? Do we really want PM |
77 |
to override that without telling me ? |
78 |
|
79 |
I believe that, from the ebuild POV, the ternary useflag model is more |
80 |
appropriate: You have a whole bunch of ways to specify useflags with |
81 |
portage (make.conf, package.use, profiles, command line, ...). From the |
82 |
ebuild those are collapsed into 'user input'. You only have IUSE (with |
83 |
its defaults) and that's what the auto-solver should play with: those |
84 |
are the flags that can be toggled. |
85 |
|
86 |
|
87 |
> Now, this also means that every constraint that can't be solved in |
88 |
> this easy fashion is invalid. We want to detect that, and warn the |
89 |
> developer. Some of those could be tricky. Simple example: |
90 |
> |
91 |
> foo? ( baz ) bar? ( !baz ) |
92 |
> |
93 |
> This one is invalid because USE='foo bar' requires both 'baz' and |
94 |
> '!baz' as a solution. Remember that we don't want to do any changes |
95 |
> besides what's explicitly written there, no guessing. |
96 |
|
97 |
Besides that, what makes it invalid ? How is it more invalid than '?? |
98 |
( foo bar )' ? |
99 |
|
100 |
> However, the |
101 |
> following should be valid: |
102 |
> |
103 |
> foo? ( baz ) bar? ( !foo !baz ) |
104 |
> |
105 |
> Because now we clearly indicate that USE=bar disables USE=foo, |
106 |
> and therefore makes the first constraint inapplicable. It clearly |
107 |
> indicates course of action for all combinations: |
108 |
|
109 |
Ok, I now think you're aiming for giving full power to the solver, |
110 |
overriding user inputs if necessary. Before going further, I think we |
111 |
should first agree on what are the useflags such a solver can toggle. |
112 |
I'm not sure 'USE=foo emerge blah' should disable foo instead of |
113 |
failing for example. |
114 |
|
115 |
|
116 |
Alexis. |