[ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Vegard Nossum]

Hi,

I just wanted to say that I've been accepted into this year's Google
Summer of Code program and will spend this summer working on improving
the kconfig system in a very particular direction: I want to integrate
a proper boolean constraint satisfiability solver into the
configuration editors (menuconfig, etc.) in order to allow
partial/incomplete configuration specifications. In short, this means
that the user can choose to not specify a particular value for some
config options, but let the system deduce their values. This will
hopefully improve usability and also solve the select problem once and
for all.

A slightly shortened version of the project proposal that was accepted
can be found here:

http://userweb.kernel.org/~vegard/gsoc2010/proposal-short.html

In case anybody would like to track my progress throughout the summer,
I have set up my public project repositories at:

http://github.com/vegard/dpll
http://github.com/vegard/linux-2.6-kconfig-sat

I am also planning to post some updates to LKML as milestones are
completed.  (Please let me know if you would like to be added to or
removed from the Cc list.) The official end date is August 16, by
which time I hope to have submitted my work for mainline inclusion.

Feedback is appreciated -- I am also prepared to respond to
constructive criticism.

Lastly, I would like to thank Google for sponsoring me, and to thank
Portland State University and my mentor Bart Massey for believing in
this idea and project.


Vegard

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Andi Kleen]

Vegard Nossum <vegard.nossum@gmail.com> writes:

> I just wanted to say that I've been accepted into this year's Google
> Summer of Code program and will spend this summer working on improving
> the kconfig system in a very particular direction: I want to integrate
> a proper boolean constraint satisfiability solver into the
> configuration editors (menuconfig, etc.) in order to allow
> partial/incomplete configuration specifications. In short, this means
> that the user can choose to not specify a particular value for some
> config options, but let the system deduce their values. This will
> hopefully improve usability and also solve the select problem once and
> for all.

Nice idea. I read your proposal and it looks good.

I assume you got inspired by the libzypp use of a SAT solver
for package dependencies?  One problem that is visible there 
is that it can be hard to display conflicts in a nice and understandable
way to the user, especially if there are lots of dependencies.

It might be worth planning in some time to solve that nicely.

-Andi

-- 
ak@linux.intel.com -- Speaking for myself only.

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Vegard Nossum]

On 17 May 2010 14:13, Andi Kleen <andi@firstfloor.org> wrote:
> Vegard Nossum <vegard.nossum@gmail.com> writes:
>
>> I just wanted to say that I've been accepted into this year's Google
>> Summer of Code program and will spend this summer working on improving
>> the kconfig system in a very particular direction: I want to integrate
>> a proper boolean constraint satisfiability solver into the
>> configuration editors (menuconfig, etc.) in order to allow
>> partial/incomplete configuration specifications. In short, this means
>> that the user can choose to not specify a particular value for some
>> config options, but let the system deduce their values. This will
>> hopefully improve usability and also solve the select problem once and
>> for all.
>
> Nice idea. I read your proposal and it looks good.
>
> I assume you got inspired by the libzypp use of a SAT solver
> for package dependencies?  One problem that is visible there
> is that it can be hard to display conflicts in a nice and understandable
> way to the user, especially if there are lots of dependencies.
>
> It might be worth planning in some time to solve that nicely.

Thanks! I didn't actually get inspired by libzypp -- but somebody else
mentioned it too, so I guess I should take a look!

You bring up a valid point, and I admittedly haven't given it VERY
much thought yet, but I think that conflicts could be displayed in the
following way: If an instance is unsolvable, then it means that all
possible valuations/assignments make at least one clause (disjunction)
false. Each clause is usually generated by exactly one dependency
specification (the "depends on" directive), so we could print these
dependencies to the screen as suggestions for how to resolve the
conflict.


Vegard

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[James Bottomley]

On Mon, 2010-05-17 at 15:09 +0200, Vegard Nossum wrote:
> On 17 May 2010 14:13, Andi Kleen <andi@firstfloor.org> wrote:
> > Vegard Nossum <vegard.nossum@gmail.com> writes:
> >
> >> I just wanted to say that I've been accepted into this year's Google
> >> Summer of Code program and will spend this summer working on improving
> >> the kconfig system in a very particular direction: I want to integrate
> >> a proper boolean constraint satisfiability solver into the
> >> configuration editors (menuconfig, etc.) in order to allow
> >> partial/incomplete configuration specifications. In short, this means
> >> that the user can choose to not specify a particular value for some
> >> config options, but let the system deduce their values. This will
> >> hopefully improve usability and also solve the select problem once and
> >> for all.
> >
> > Nice idea. I read your proposal and it looks good.
> >
> > I assume you got inspired by the libzypp use of a SAT solver
> > for package dependencies?  One problem that is visible there
> > is that it can be hard to display conflicts in a nice and understandable
> > way to the user, especially if there are lots of dependencies.
> >
> > It might be worth planning in some time to solve that nicely.
> 
> Thanks! I didn't actually get inspired by libzypp -- but somebody else
> mentioned it too, so I guess I should take a look!
> 
> You bring up a valid point, and I admittedly haven't given it VERY
> much thought yet, but I think that conflicts could be displayed in the
> following way: If an instance is unsolvable, then it means that all
> possible valuations/assignments make at least one clause (disjunction)
> false. Each clause is usually generated by exactly one dependency
> specification (the "depends on" directive), so we could print these
> dependencies to the screen as suggestions for how to resolve the
> conflict.

Actually, the problem is a bit different from the zypper one: Since each
package supplies its own dependencies and obsoletes, it is possible to
get an unsolvable installation problem.  What zypper tries to do in
these situations is recommend possible courses of action (like remove
these five packages from your current system, or downgrade this one
etc.).  For the Kconfig system, an unsolvable configuration is actually
a bug in the Kconfig files.  You can proceed on the premise that it's a
single symbol that has the wrong depends or selects and isolate it from
there.  Done right, the Kconfig SAT solver shouldn't detect this problem
only when a triggering configuration is input, but all the time, so it
becomes impossible to introduce buggy Kconfig directives into the kernel
tree.

James

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Andi Kleen]

> You bring up a valid point, and I admittedly haven't given it VERY
> much thought yet, but I think that conflicts could be displayed in the
> following way: If an instance is unsolvable, then it means that all
> possible valuations/assignments make at least one clause (disjunction)
> false. Each clause is usually generated by exactly one dependency
> specification (the "depends on" directive), so we could print these
> dependencies to the screen as suggestions for how to resolve the
> conflict.

The problem is that might be a lot of entries, e.g. for "depends on PCI"

You then end up displaying pages and pages of information, which
is very hard to make sense of.

You can see that by playing around with libzypp dependencies.

-Andi
-- 
ak@linux.intel.com -- Speaking for myself only.

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Vegard Nossum]

On 17 May 2010 15:21, James Bottomley
<James.Bottomley@hansenpartnership.com> wrote:
>> > I assume you got inspired by the libzypp use of a SAT solver
>> > for package dependencies?  One problem that is visible there
>> > is that it can be hard to display conflicts in a nice and understandable
>> > way to the user, especially if there are lots of dependencies.
>> >
>> > It might be worth planning in some time to solve that nicely.
>>
>> Thanks! I didn't actually get inspired by libzypp -- but somebody else
>> mentioned it too, so I guess I should take a look!
>>
>> You bring up a valid point, and I admittedly haven't given it VERY
>> much thought yet, but I think that conflicts could be displayed in the
>> following way: If an instance is unsolvable, then it means that all
>> possible valuations/assignments make at least one clause (disjunction)
>> false. Each clause is usually generated by exactly one dependency
>> specification (the "depends on" directive), so we could print these
>> dependencies to the screen as suggestions for how to resolve the
>> conflict.
>
> Actually, the problem is a bit different from the zypper one: Since each
> package supplies its own dependencies and obsoletes, it is possible to
> get an unsolvable installation problem.  What zypper tries to do in
> these situations is recommend possible courses of action (like remove
> these five packages from your current system, or downgrade this one
> etc.).  For the Kconfig system, an unsolvable configuration is actually
> a bug in the Kconfig files.  You can proceed on the premise that it's a
> single symbol that has the wrong depends or selects and isolate it from
> there.  Done right, the Kconfig SAT solver shouldn't detect this problem
> only when a triggering configuration is input, but all the time, so it
> becomes impossible to introduce buggy Kconfig directives into the kernel
> tree.

Even if the problem is different from zypper's, it is also here
possible to get an unsatisfiable instance. You are right that, yes,
the kconfig files on their own should always be satisfiable. But
that's before the user has made any choices at all. An example of an
unsatisfiable instance would be one where the user demands that 1.
some USB driver is enabled, while 2. USB support in general is
disabled.

But yes, once the basic infrastructure is in place, checking the
consistency of the kconfig files alone (not taking user's config into
account) should be trivial.


Vegard

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[James Bottomley]

On Mon, 2010-05-17 at 16:21 +0200, Vegard Nossum wrote:
> On 17 May 2010 15:21, James Bottomley
> <James.Bottomley@hansenpartnership.com> wrote:
> >> > I assume you got inspired by the libzypp use of a SAT solver
> >> > for package dependencies?  One problem that is visible there
> >> > is that it can be hard to display conflicts in a nice and understandable
> >> > way to the user, especially if there are lots of dependencies.
> >> >
> >> > It might be worth planning in some time to solve that nicely.
> >>
> >> Thanks! I didn't actually get inspired by libzypp -- but somebody else
> >> mentioned it too, so I guess I should take a look!
> >>
> >> You bring up a valid point, and I admittedly haven't given it VERY
> >> much thought yet, but I think that conflicts could be displayed in the
> >> following way: If an instance is unsolvable, then it means that all
> >> possible valuations/assignments make at least one clause (disjunction)
> >> false. Each clause is usually generated by exactly one dependency
> >> specification (the "depends on" directive), so we could print these
> >> dependencies to the screen as suggestions for how to resolve the
> >> conflict.
> >
> > Actually, the problem is a bit different from the zypper one: Since each
> > package supplies its own dependencies and obsoletes, it is possible to
> > get an unsolvable installation problem.  What zypper tries to do in
> > these situations is recommend possible courses of action (like remove
> > these five packages from your current system, or downgrade this one
> > etc.).  For the Kconfig system, an unsolvable configuration is actually
> > a bug in the Kconfig files.  You can proceed on the premise that it's a
> > single symbol that has the wrong depends or selects and isolate it from
> > there.  Done right, the Kconfig SAT solver shouldn't detect this problem
> > only when a triggering configuration is input, but all the time, so it
> > becomes impossible to introduce buggy Kconfig directives into the kernel
> > tree.
> 
> Even if the problem is different from zypper's, it is also here
> possible to get an unsatisfiable instance. You are right that, yes,
> the kconfig files on their own should always be satisfiable. But
> that's before the user has made any choices at all. An example of an
> unsatisfiable instance would be one where the user demands that 1.
> some USB driver is enabled, while 2. USB support in general is
> disabled.

Actually, these are two separate problems.  The first is basic
consistency within the Kconfig subsytstem (something that select
currently damages for us).  The second is what to present to the user,
which is where the inception of the select problem came from.  A user
doesn't really want to know that USB device X depends on usb storage,
SCSI and a raft of other things ... they just want it to configure a
kernel that supports their device.  In particular, we don't want to
present every possible option to users and then try to work out a
solution, we really need guided configuration (which, in some measure,
is what we have today: if you don't select general USB, you won't see
any USB drivers.  Or more importantly, if you select an Adaptec SCSI
card, we just enable whichever transport library it needs).

> But yes, once the basic infrastructure is in place, checking the
> consistency of the kconfig files alone (not taking user's config into
> account) should be trivial.

Right, this will solve our current kernel developer issue ... I'm
betting the guiding users one will be slightly harder.

James

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[david]

On Mon, 17 May 2010, James Bottomley wrote:

> On Mon, 2010-05-17 at 16:21 +0200, Vegard Nossum wrote:
>> On 17 May 2010 15:21, James Bottomley
>>
>> Even if the problem is different from zypper's, it is also here
>> possible to get an unsatisfiable instance. You are right that, yes,
>> the kconfig files on their own should always be satisfiable. But
>> that's before the user has made any choices at all. An example of an
>> unsatisfiable instance would be one where the user demands that 1.
>> some USB driver is enabled, while 2. USB support in general is
>> disabled.
>
> Actually, these are two separate problems.  The first is basic
> consistency within the Kconfig subsytstem (something that select
> currently damages for us).  The second is what to present to the user,
> which is where the inception of the select problem came from.  A user
> doesn't really want to know that USB device X depends on usb storage,
> SCSI and a raft of other things ... they just want it to configure a
> kernel that supports their device.  In particular, we don't want to
> present every possible option to users and then try to work out a
> solution, we really need guided configuration (which, in some measure,
> is what we have today: if you don't select general USB, you won't see
> any USB drivers.  Or more importantly, if you select an Adaptec SCSI
> card, we just enable whichever transport library it needs).

There are two modes people can be in when configuring a kernel.

1. I want to configure a kernel to support my hardware, enable anything 
else needed to make it work.

2. I really care about having a small kernel, don't enable anything I have 
disabled (but help me figure out why something I want isn't available)

I don't think that hiding hardware from the user is ever the best thing to 
do. for approach #1 you obviously don't want to hide anything, but even 
for approach #2, someone may not realize that by disabling one option they 
are making it impossible to support something, and as someone who spent a 
bunch of time hunting through config to find options that I ended up 
finding were not available without enabling something else, I much prefer 
to see the option, but see it disabled rather than not being sure if it 
should be there, or somewhere else in the config.

David Lang

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Jon Smirl]

On Tue, May 18, 2010 at 2:03 AM,  <david@lang.hm> wrote:
> On Mon, 17 May 2010, James Bottomley wrote:
>
>> On Mon, 2010-05-17 at 16:21 +0200, Vegard Nossum wrote:
>>>
>>> On 17 May 2010 15:21, James Bottomley
>>>
>>> Even if the problem is different from zypper's, it is also here
>>> possible to get an unsatisfiable instance. You are right that, yes,
>>> the kconfig files on their own should always be satisfiable. But
>>> that's before the user has made any choices at all. An example of an
>>> unsatisfiable instance would be one where the user demands that 1.
>>> some USB driver is enabled, while 2. USB support in general is
>>> disabled.
>>
>> Actually, these are two separate problems.  The first is basic
>> consistency within the Kconfig subsytstem (something that select
>> currently damages for us).  The second is what to present to the user,
>> which is where the inception of the select problem came from.  A user
>> doesn't really want to know that USB device X depends on usb storage,
>> SCSI and a raft of other things ... they just want it to configure a
>> kernel that supports their device.  In particular, we don't want to
>> present every possible option to users and then try to work out a
>> solution, we really need guided configuration (which, in some measure,
>> is what we have today: if you don't select general USB, you won't see
>> any USB drivers.  Or more importantly, if you select an Adaptec SCSI
>> card, we just enable whichever transport library it needs).
>
> There are two modes people can be in when configuring a kernel.
>
> 1. I want to configure a kernel to support my hardware, enable anything else
> needed to make it work.
>
> 2. I really care about having a small kernel, don't enable anything I have
> disabled (but help me figure out why something I want isn't available)
>
> I don't think that hiding hardware from the user is ever the best thing to
> do. for approach #1 you obviously don't want to hide anything, but even for
> approach #2, someone may not realize that by disabling one option they are
> making it impossible to support something, and as someone who spent a bunch
> of time hunting through config to find options that I ended up finding were
> not available without enabling something else, I much prefer to see the
> option, but see it disabled rather than not being sure if it should be
> there, or somewhere else in the config.

I have to agree with this. An example is audio drivers that disappear
because something like SPI is turned off. Sometimes I have to read the
Kconfig files to figure out what subsystems I need enabled in order to
make the driver appear as a choice.

Another way this could work...
Enable the platform
this causes all subsystems on the platform (usb, spi, pci, etc) to be
soft enabled
user selects device drivers or hard enables the subsystem
on save, if the subsystem wasn't hard enabled for some reason or
dependency, disable it.

---------------

I'd also find it useful if Kconfig had an option that analyzed the
system it is running on and then generated the minimal set of drivers
needed to support it. Assume that the system is running something like
the Ubuntu kernel with every driver enabled. Then figure out the
minimal build footprint for a custom kernel to support the same
hardware.  I do this by hand, but a button for doing it would be a lot
easier.

>
> David Lang
> --
> To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> Please read the FAQ at  http://www.tux.org/lkml/
>



-- 
Jon Smirl
jonsmirl@gmail.com

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Vegard Nossum]

On 18 May 2010 14:26, Jon Smirl <jonsmirl@gmail.com> wrote:
> On Tue, May 18, 2010 at 2:03 AM,  <david@lang.hm> wrote:
>> There are two modes people can be in when configuring a kernel.
>>
>> 1. I want to configure a kernel to support my hardware, enable anything else
>> needed to make it work.
>>
>> 2. I really care about having a small kernel, don't enable anything I have
>> disabled (but help me figure out why something I want isn't available)
>>
>> I don't think that hiding hardware from the user is ever the best thing to
>> do. for approach #1 you obviously don't want to hide anything, but even for
>> approach #2, someone may not realize that by disabling one option they are
>> making it impossible to support something, and as someone who spent a bunch
>> of time hunting through config to find options that I ended up finding were
>> not available without enabling something else, I much prefer to see the
>> option, but see it disabled rather than not being sure if it should be
>> there, or somewhere else in the config.
>
> I have to agree with this. An example is audio drivers that disappear
> because something like SPI is turned off. Sometimes I have to read the
> Kconfig files to figure out what subsystems I need enabled in order to
> make the driver appear as a choice.
>
> Another way this could work...
> Enable the platform
> this causes all subsystems on the platform (usb, spi, pci, etc) to be
> soft enabled
> user selects device drivers or hard enables the subsystem
> on save, if the subsystem wasn't hard enabled for some reason or
> dependency, disable it.
>
> ---------------
>
> I'd also find it useful if Kconfig had an option that analyzed the
> system it is running on and then generated the minimal set of drivers
> needed to support it. Assume that the system is running something like
> the Ubuntu kernel with every driver enabled. Then figure out the
> minimal build footprint for a custom kernel to support the same
> hardware.  I do this by hand, but a button for doing it would be a lot
> easier.

Consider this a response to both of the above e-mails. Just to clear
any confusion, a consequence of using SAT for kconfig is that you can
now say for example only the following: "I want drivers A, B, and C. I
don't care if that means I can't use FOO and I don't care if that
means that I have to use BAR, just give me A, B, and C."

I suppose another way to see it is that configuring the kernel using
the current menuconfig is a top-down process, since you have to select
USB before you can select any driver that depends on USB. Using SAT
for kconfig puts this on its head, and the configuration process
becomes bottom-up; you say only what you want to have (or not have),
and the system figures out the rest. If you choose a driver that
requires USB (and you haven't said that you also don't want USB
support, which would be impossible), then USB _will_ be enabled
automatically.

For the record, I think that there are already scripts that take a
running system and builds a config for that.


Vegard

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[kevin granade]

On Tue, May 18, 2010 at 7:54 AM, Vegard Nossum <vegard.nossum@gmail.com> wrote:
> On 18 May 2010 14:26, Jon Smirl <jonsmirl@gmail.com> wrote:
>> On Tue, May 18, 2010 at 2:03 AM,  <david@lang.hm> wrote:
>>> There are two modes people can be in when configuring a kernel.
>>>
>>> 1. I want to configure a kernel to support my hardware, enable anything else
>>> needed to make it work.
>>>
>>> 2. I really care about having a small kernel, don't enable anything I have
>>> disabled (but help me figure out why something I want isn't available)
>>>
>>> I don't think that hiding hardware from the user is ever the best thing to
>>> do. for approach #1 you obviously don't want to hide anything, but even for
>>> approach #2, someone may not realize that by disabling one option they are
>>> making it impossible to support something, and as someone who spent a bunch
>>> of time hunting through config to find options that I ended up finding were
>>> not available without enabling something else, I much prefer to see the
>>> option, but see it disabled rather than not being sure if it should be
>>> there, or somewhere else in the config.
>>
>> I have to agree with this. An example is audio drivers that disappear
>> because something like SPI is turned off. Sometimes I have to read the
>> Kconfig files to figure out what subsystems I need enabled in order to
>> make the driver appear as a choice.
>>
>> Another way this could work...
>> Enable the platform
>> this causes all subsystems on the platform (usb, spi, pci, etc) to be
>> soft enabled
>> user selects device drivers or hard enables the subsystem
>> on save, if the subsystem wasn't hard enabled for some reason or
>> dependency, disable it.
>>
>> ---------------
>>
>> I'd also find it useful if Kconfig had an option that analyzed the
>> system it is running on and then generated the minimal set of drivers
>> needed to support it. Assume that the system is running something like
>> the Ubuntu kernel with every driver enabled. Then figure out the
>> minimal build footprint for a custom kernel to support the same
>> hardware.  I do this by hand, but a button for doing it would be a lot
>> easier.
>
> Consider this a response to both of the above e-mails. Just to clear
> any confusion, a consequence of using SAT for kconfig is that you can
> now say for example only the following: "I want drivers A, B, and C. I
> don't care if that means I can't use FOO and I don't care if that
> means that I have to use BAR, just give me A, B, and C."
>
> I suppose another way to see it is that configuring the kernel using
> the current menuconfig is a top-down process, since you have to select
> USB before you can select any driver that depends on USB. Using SAT
> for kconfig puts this on its head, and the configuration process
> becomes bottom-up; you say only what you want to have (or not have),
> and the system figures out the rest. If you choose a driver that
> requires USB (and you haven't said that you also don't want USB
> support, which would be impossible), then USB _will_ be enabled
> automatically.
>
> For the record, I think that there are already scripts that take a
> running system and builds a config for that.

At least some of what you want is provided by 'make localmodconfig'

-Kevin Granade

>
>
> Vegard
> --
> To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> Please read the FAQ at  http://www.tux.org/lkml/
>

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Felipe Contreras]

On Mon, May 17, 2010 at 3:02 PM, Vegard Nossum <vegard.nossum@gmail.com> wrote:
> Hi,
>
> I just wanted to say that I've been accepted into this year's Google
> Summer of Code program and will spend this summer working on improving
> the kconfig system in a very particular direction: I want to integrate
> a proper boolean constraint satisfiability solver into the
> configuration editors (menuconfig, etc.) in order to allow
> partial/incomplete configuration specifications. In short, this means
> that the user can choose to not specify a particular value for some
> config options, but let the system deduce their values. This will
> hopefully improve usability and also solve the select problem once and
> for all.
>
> A slightly shortened version of the project proposal that was accepted
> can be found here:
>
> http://userweb.kernel.org/~vegard/gsoc2010/proposal-short.html
>
> In case anybody would like to track my progress throughout the summer,
> I have set up my public project repositories at:
>
> http://github.com/vegard/dpll
> http://github.com/vegard/linux-2.6-kconfig-sat
>
> I am also planning to post some updates to LKML as milestones are
> completed.  (Please let me know if you would like to be added to or
> removed from the Cc list.) The official end date is August 16, by
> which time I hope to have submitted my work for mainline inclusion.
>
> Feedback is appreciated -- I am also prepared to respond to
> constructive criticism.
>
> Lastly, I would like to thank Google for sponsoring me, and to thank
> Portland State University and my mentor Bart Massey for believing in
> this idea and project.

Very nice! I thought on this idea too.

Does this means that if you have a pristine kernel, and you do 'make
menuconfig' and don't change anything, the .config file will be empty?
And then, anything that you change will be in the .config file?

On another case I do 'make ARCH=arm omap3_beagle_defconfig' then my
.config file will point to that particular defconfig, and I can add
only the changes that I want. Also, omap3_beagle_defconfig probably
points omap3_defconfig and only makes certain changes.

If so, that would be awesome :)

-- 
Felipe Contreras

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Vegard Nossum]

On 19 May 2010 13:05, Felipe Contreras <felipe.contreras@gmail.com> wrote:
> On Mon, May 17, 2010 at 3:02 PM, Vegard Nossum <vegard.nossum@gmail.com> wrote:
>> Hi,
>>
>> I just wanted to say that I've been accepted into this year's Google
>> Summer of Code program and will spend this summer working on improving
>> the kconfig system in a very particular direction: I want to integrate
>> a proper boolean constraint satisfiability solver into the
>> configuration editors (menuconfig, etc.) in order to allow
>> partial/incomplete configuration specifications. In short, this means
>> that the user can choose to not specify a particular value for some
>> config options, but let the system deduce their values. This will
>> hopefully improve usability and also solve the select problem once and
>> for all.
>
> Very nice! I thought on this idea too.
>
> Does this means that if you have a pristine kernel, and you do 'make
> menuconfig' and don't change anything, the .config file will be empty?
> And then, anything that you change will be in the .config file?
>

Yes and no -- I think the plan is to retain the .config file as it is
(i.e. it specifies more or less every option completely), so that it
remains backwards compatible; bisection, for example, is very
important. But yes, I think there will be a new file, say, .satconfig,
which contains only the specific choices of the user. And this one
would be empty, as you say, with a pristine kernel.

I think, then, that the .config file will be regenerated from the
.satconfig one each time .satconfig changes.

> On another case I do 'make ARCH=arm omap3_beagle_defconfig' then my
> .config file will point to that particular defconfig, and I can add
> only the changes that I want. Also, omap3_beagle_defconfig probably
> points omap3_defconfig and only makes certain changes.
>
> If so, that would be awesome :)

Do you mean essentially a sort of cascade of configurations that
inherit options from a different file? That shouldn't be very hard to
do -- I'll make a note of it for when I get that far! That has the
potential to make the defconfig files a bit shorter and more
manageable (not sure how big a problem that is in practice today,
though).

Thanks,


Vegard

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Felipe Contreras]

On Wed, May 19, 2010 at 9:31 PM, Vegard Nossum <vegard.nossum@gmail.com> wrote:
> On 19 May 2010 13:05, Felipe Contreras <felipe.contreras@gmail.com> wrote:
>> Does this means that if you have a pristine kernel, and you do 'make
>> menuconfig' and don't change anything, the .config file will be empty?
>> And then, anything that you change will be in the .config file?
>
> Yes and no -- I think the plan is to retain the .config file as it is
> (i.e. it specifies more or less every option completely), so that it
> remains backwards compatible; bisection, for example, is very
> important. But yes, I think there will be a new file, say, .satconfig,
> which contains only the specific choices of the user. And this one
> would be empty, as you say, with a pristine kernel.
>
> I think, then, that the .config file will be regenerated from the
> .satconfig one each time .satconfig changes.

I see. As long as people can use .satconfig only if they want, I think
that's great.

>> On another case I do 'make ARCH=arm omap3_beagle_defconfig' then my
>> .config file will point to that particular defconfig, and I can add
>> only the changes that I want. Also, omap3_beagle_defconfig probably
>> points omap3_defconfig and only makes certain changes.
>>
>> If so, that would be awesome :)
>
> Do you mean essentially a sort of cascade of configurations that
> inherit options from a different file? That shouldn't be very hard to
> do -- I'll make a note of it for when I get that far! That has the
> potential to make the defconfig files a bit shorter and more
> manageable (not sure how big a problem that is in practice today,
> though).

Exactly. Well, I don't know if anybody considers that a problem, but
just check arch/arm/configs/*. All of them are much bigger than
needed, and some have not been updated in a long time (even as old as
2.6.11). So if you do make ARCH=arm assabet_defconfig and do a 'diff
.config assabet_defconfig' they would be completely different. This
way it's hard to keep track of the general config changes, and ARM
related changes, and OMAP3 changes, and compare with board-specific
ones.

Cheers.

-- 
Felipe Contreras

Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

[Pavel Machek]

Hi!

> >>Even if the problem is different from zypper's, it is also here
> >>possible to get an unsatisfiable instance. You are right that, yes,
> >>the kconfig files on their own should always be satisfiable. But
> >>that's before the user has made any choices at all. An example of an
> >>unsatisfiable instance would be one where the user demands that 1.
> >>some USB driver is enabled, while 2. USB support in general is
> >>disabled.
> >
> >Actually, these are two separate problems.  The first is basic
> >consistency within the Kconfig subsytstem (something that select
> >currently damages for us).  The second is what to present to the user,
> >which is where the inception of the select problem came from.  A user
> >doesn't really want to know that USB device X depends on usb storage,
> >SCSI and a raft of other things ... they just want it to configure a
> >kernel that supports their device.  In particular, we don't want to
> >present every possible option to users and then try to work out a
> >solution, we really need guided configuration (which, in some measure,
> >is what we have today: if you don't select general USB, you won't see
> >any USB drivers.  Or more importantly, if you select an Adaptec SCSI
> >card, we just enable whichever transport library it needs).
> 
> There are two modes people can be in when configuring a kernel.
> 
> 1. I want to configure a kernel to support my hardware, enable
> anything else needed to make it work.
> 
> 2. I really care about having a small kernel, don't enable anything
> I have disabled (but help me figure out why something I want isn't
> available)

There are more...

...part of the problem is that kconfig is both user-dependend (what
filesystems do I use) and machine dependend (what does hw need).

Current defconfig system is unfortunately not quite there :-(.

What would be nice for machines like Sharp Zaurus (spitz) would be
defconfig which answered =Y for hardware spitz definitely has (sound),
=N for hardware that can't be connected (anything pci), and something
different (=M?)  for hardware that can be connected to it
(pcmcia)... leaving 'user' options like filesystems configured ... up
to the user.
								Pavel

-- 
(english) http://www.livejournal.com/~pavelmachek
(cesky, pictures) http://atrey.karlin.mff.cuni.cz/~pavel/picture/horses/blog.html