Update on the progress of the project

22 views
Skip to first unread message

Patrick Franz

unread,
Jan 27, 2020, 10:03:42 AM1/27/20
to kconfig-sat
Hi everyone,

I have made a video about our project. It includes an explanation of our
general approach and a short demo at the end:

https://www.youtube.com/watch?v=-HtjApu1S5g


So far, it looks promising, but the project is not finished yet. Things
that still need to be done:

* So far we have worked with smaller examples which we had constructed
by ourselves. We still need to make the entire kernel configuration work.
The biggest problem at the moment is, that we are getting the symbol
type "unknown" for some symbols, which are e.g. boolean or tristate. The
type is correct for the vast majority of symbols though. If anyone has
ever encountered this or has an idea, why this could be the case, please
contact me.
* We need to decide how to handle weak reverse dependencies (imply).
* The "Apply"-button (see the demo) does not work yet. Unfortunately, it
is not as trivial as it may sound to apply multiple changes at once
since the kernel was not built for this. We have a promising idea, but
if you have any idea, feel free to contact me.

And generally, any type of feedback is welcome.


--
Med vänliga hälsningar

Patrick Franz


Paul Gazzillo

unread,
Jan 27, 2020, 1:18:06 PM1/27/20
to Patrick Franz, kconfig-sat
On Mon, 27 Jan 16:03:38, Patrick Franz wrote:
> Hi everyone,
>
> I have made a video about our project. It includes an explanation of our
> general approach and a short demo at the end:
>
> https://www.youtube.com/watch?v=-HtjApu1S5g
>

Very nice to see work on this!

>
> So far, it looks promising, but the project is not finished yet. Things
> that still need to be done:
>
> * So far we have worked with smaller examples which we had constructed
> by ourselves. We still need to make the entire kernel configuration work.
> The biggest problem at the moment is, that we are getting the symbol
> type "unknown" for some symbols, which are e.g. boolean or tristate. The
> type is correct for the vast majority of symbols though. If anyone has
> ever encountered this or has an idea, why this could be the case, please
> contact me.

This is just a guess, but it could be configuration options that are
used in a dependency, but never defined. This can happen with
architecture-specific configuration options, i.e., those that are only
defined from a particular architecture's top-level Kconfig file. I
could be wrong though.

> * We need to decide how to handle weak reverse dependencies (imply).
> * The "Apply"-button (see the demo) does not work yet. Unfortunately, it
> is not as trivial as it may sound to apply multiple changes at once
> since the kernel was not built for this. We have a promising idea, but
> if you have any idea, feel free to contact me.

For reverse dependencies, we've got a model of them in propositional
logic that (I think) is pretty accurate. This should allow you treat
them like any other constraint, avoiding any conflicts due to selects
that override previously enabled options. This remains to be seen in
your application though...

The behavior of select is different depending on whether the option is
visible is nonvisible (i.e., has a prompt or not). The propositional
formulas for both that we use can be found here on lines 798 and 835:
https://github.com/paulgazz/kmax/blob/v2.0-rc32/kmaxtools/kclause

Best,
Paul
Reply all
Reply to author
Forward
0 new messages