public inbox for gentoo-portage-dev@lists.gentoo.org
 help / color / mirror / Atom feed
* [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype
@ 2017-12-09 17:07 Michael Lienhardt
  2017-12-10 18:27 ` Alexander Berntsen
  2019-06-20 19:02 ` [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: again michael.lienhardt
  0 siblings, 2 replies; 12+ messages in thread
From: Michael Lienhardt @ 2017-12-09 17:07 UTC (permalink / raw
  To: gentoo-portage-dev

Dear Portage developers,

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.

The first result of our work is a prototype for a constraint-based dependency solver for Portage:
  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.
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.
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.

With this prototype, we also compiled (90% of) a documentation on how portage manages package configuration (USE flags declaration, selection, masking, keywording, ...).

Link to the prototype: https://github.com/HyVar/gentoo_to_mspl
Link to the documentation: https://github.com/HyVar/gentoo_to_mspl/blob/master/PORTAGE.md


We would really like to know your opinions, impressions and suggestions about this work.
We would also like to know how useful this tool could be for the community:
  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
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).


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.

Best Regards,
Michael Lienhardt


PS: list of uninstallable packages:
  dev-java/jruby-1.7.12
  media-video/nvidia-settings-340.58
  dev-ruby/bitescript-0.0.9
  dev-java/spring-core-3.2.4
  app-i18n/ibus-table-code-1.2.0.20100305
  dev-ruby/weakling-0.0.4
  sci-libs/ogdi-3.1.5-r1
  dev-java/jcs-2.0
  net-misc/asterisk-rate_engine-0.5.4
  games-fps/doom3-mitm-20070129
  app-office/impressive-0.10.5
  dev-java/spring-aop-3.2.4
  dev-ruby/duby-0.0.2-r1
  dev-db/mycli-9999


^ permalink raw reply	[flat|nested] 12+ messages in thread

end of thread, other threads:[~2019-10-08 22:55 UTC | newest]

Thread overview: 12+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2017-12-09 17:07 [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype Michael Lienhardt
2017-12-10 18:27 ` Alexander Berntsen
2017-12-13  1:52   ` Re : " michael.lienhardt
2017-12-16 13:39     ` Alexander Berntsen
2018-01-08  2:06       ` Michael Lienhardt
2018-01-08 11:54         ` Alexander Berntsen
2019-06-20 19:02 ` [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: again michael.lienhardt
2019-06-20 20:23   ` Zac Medico
2019-06-21 10:41     ` Re : " michael.lienhardt
2019-08-30 14:34       ` [gentoo-portage-dev] Constraint-Based Dependency Solver: initial results michael.lienhardt
2019-10-08 22:21         ` Michael Orlitzky
2019-10-08 22:55         ` Zac Medico

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox