Re: Re : Re: [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype
On 08/01/18 03:06, Michael Lienhardt wrote: > Many thanks for the advices. I started few discussions on the forum > and will go to FOSDEM. I'll see where it will go. Consider mentioning this in #gentoo-fosdem on irc.freenode.net, which is where the Gentoo devs & users who are going to FOSDEM generally gather. Maybe you can meet up with everyone. There's usually a few Gentoo dinners (one actual "Gentoo dinner" that everyone sign sup to, and just informal dinners throughout the weekend as well), and an OpenPGP key-signing event, for instance. Good luck, and enjoy FOSDEM. -- Alexander berna...@gentoo.org https://secure.plaimi.net/~alexander signature.asc Description: OpenPGP digital signature
Re: Re : Re: [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype
Dear Alexander, Many thanks for the advices. I started few discussions on the forum and will go to FOSDEM. I'll see where it will go. Best, Michael Il 16/12/2017 14:39, Alexander Berntsen ha scritto: On 13/12/17 02:52, michael.lienha...@laposte.net wrote: But maybe there are things we can do to help start a dialog, like: - reaching in other mailing lists I don't think a post to gentoo-dev would be remiss in this case. - posting on a Gentoo forum Always useful, I'm told, though I don't venture there. But that way you're far more likely to engage *users*. - participating in a workshop/conference/other where we could directly meet and discuss with the community FOSDEM and Linux Days are probably the best choices. - or simply starting an informal discussion by email where instead of having to look into the Github repository, you could directly ask me If someone has the time, that'll probably naturally happen through the MLs. Christmas time tends to be peak bikeshedding hours at Gentoo, so maybe cross-post to -dev closer to the holidays?
Re : Re: [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype
Dear Alexander, Many thanks for your reply and your encouragements. The point that you raised is very interesting and was partially done in Debian (they defined a wrapper around apt-get instead of refactoring it): http://manpages.ubuntu.com/manpages/zesty/man8/apt-cudf-get.8.html Part of their work was formalized in coq and implemented in OCaml. In our case, we don't have any mechanized formalization of our model (maybe in the future). I too (and my colleagues) hope that someone on the team could have some time to look into our project. But maybe there are things we can do to help start a dialog, like: - reaching in other mailing lists - posting on a Gentoo forum - participating in a workshop/conference/other where we could directly meet and discuss with the community - or simply starting an informal discussion by email where instead of having to look into the Github repository, you could directly ask me Does anyone have suggestions on that topic? Again, many thanks. I really hope that with everyone's feedback, suggestions, and help, we could make something useful from this prototype. Michael Lienhardt PS: I forgot in my previous mail to talk about the other persons involved in this project: - Jacopo Mauro, Post-doc in UiO (Norway), developer of the solver backend - Simone Donetti, Engineer in Unito (Italy), he helped me perform some tests - Ferruccio Damiani (Unito), Einar Broch Johnsen and Ingrid Chieh Yu (UiO), our supervisors
Re: [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype
Unfortunately I am way too busy to even entertain looking into this in any detail. A few years ago I was hoping to work on something like this, though in Agda (or possibly in Haskell or Coq), and do work on making Portage much more modular so that you could actually pick whatever dependency resolver you wanted -- even going as far as "Don't like the resolution you were presented now? Try using another resolver" messages. But alas that job ended before I got very far. However, I wanted to take the time to drop you a tiny note of encouragement. I think this looks really great, and I hope someone on the team finds the time to look into it in more detail than me. -- Alexander berna...@gentoo.org https://secure.plaimi.net/~alexander signature.asc Description: OpenPGP digital signature
[gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype
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-
