1 |
Dear Portage developers, |
2 |
|
3 |
I am a Post-doc in formal methods and software engineering. With my colleagues, we are working on a formal model for software composition, and were looking for a concrete example of such model to motivate and guide our work. I knew portage from using gentoo since 2007, and knew that it is the perfect use case for us. |
4 |
|
5 |
The first result of our work is a prototype for a constraint-based dependency solver for Portage: |
6 |
like the emerge tool, it takes in parameter a list of atoms to install, and computes a full list of packages to install to satisfy the package dependency relation. |
7 |
Up to bugs, this tool is correct and complete: it will always find a solution if it exists, and always tell if there are none. |
8 |
For instance, it successfully computed that gnome-base/gnome cannot be installed by default (on a udev system), but found a solution that replaces sys-fs/eudev by sys-apps/systemd when we allow the tool to change the USE flag selection of the packages. |
9 |
|
10 |
With this prototype, we also compiled (90% of) a documentation on how portage manages package configuration (USE flags declaration, selection, masking, keywording, ...). |
11 |
|
12 |
Link to the prototype: https://github.com/HyVar/gentoo_to_mspl |
13 |
Link to the documentation: https://github.com/HyVar/gentoo_to_mspl/blob/master/PORTAGE.md |
14 |
|
15 |
|
16 |
We would really like to know your opinions, impressions and suggestions about this work. |
17 |
We would also like to know how useful this tool could be for the community: |
18 |
as for now, it is a prototype of a dependency solver (that would definitively need some work to be usable in production), but it also offers the possibility of any kind of formal analysis on the REQUIRED_USE and dependencies in packages, like the one described in https://bugs.gentoo.org/417753 |
19 |
For instance, our tool already checks for obvious reasons (inconsistent REQUIRED_USE or unmet dependencies) causing a package not to be installable. In particular, on the Portage version available in http://www.osboxes.org/gentoo/ , our tool identified 14 packages that could not be installed for these reasons (the full list in in post-scriptum). |
20 |
|
21 |
|
22 |
Additionally, our implementation is based on what I understood of the portage's documentation, which I compiled in the PORTAGE.md document: it would be very helpful if you could point error that I made or subtleties that I didn't understand or missed. |
23 |
|
24 |
Best Regards, |
25 |
Michael Lienhardt |
26 |
|
27 |
|
28 |
PS: list of uninstallable packages: |
29 |
dev-java/jruby-1.7.12 |
30 |
media-video/nvidia-settings-340.58 |
31 |
dev-ruby/bitescript-0.0.9 |
32 |
dev-java/spring-core-3.2.4 |
33 |
app-i18n/ibus-table-code-1.2.0.20100305 |
34 |
dev-ruby/weakling-0.0.4 |
35 |
sci-libs/ogdi-3.1.5-r1 |
36 |
dev-java/jcs-2.0 |
37 |
net-misc/asterisk-rate_engine-0.5.4 |
38 |
games-fps/doom3-mitm-20070129 |
39 |
app-office/impressive-0.10.5 |
40 |
dev-java/spring-aop-3.2.4 |
41 |
dev-ruby/duby-0.0.2-r1 |
42 |
dev-db/mycli-9999 |