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