From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id CF774139083 for ; Sat, 9 Dec 2017 17:07:38 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 901CFE10EB; Sat, 9 Dec 2017 17:07:37 +0000 (UTC) Received: from smtp.laposte.net (smtpoutz26.laposte.net [194.117.213.101]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 35697E10DF for ; Sat, 9 Dec 2017 17:07:37 +0000 (UTC) Received: from smtp.laposte.net (localhost [127.0.0.1]) by lpn-prd-vrout014 (Postfix) with ESMTP id D7BCD11F94F for ; Sat, 9 Dec 2017 18:07:34 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=laposte.net; s=mail0; t=1512839254; bh=ob5EYz4nbwkmBuOXhe5OEZa96W3i7fL0KZ2rlFKguEE=; h=To:From:Subject:Date; b=hrOkBqW2KiLO5RY2HbxklT2a/WLYKLnjWkgIXCV7oX/vYBSVK9gqQMwrf2mrUdzT/ NpOt4utGLQeo8e/tqnNRV2R2ssNnEslEyhtQfkdtkn6TV7NTDjVyaks5xPwURPzzJc DSVI7cHlmdKS9F3VbeUutUoAcnJgCxzBHvRWQEbu10z4eQK6xjBmgUHpFEz3RM9wk8 /RoLer8Vtq3FajIekylOu0MrXgzvftYR2CkvCAodB7Go9ElrjIbYiI/oiU7sO+YGWN ZOAjNVhPo8s/HTBz6QorxoQulTDpp391qk8uBR67CcUCYfCqZy4ExIt2ZoJcx9FrFj /WX697A0RZ5ag== Received: from smtp.laposte.net (localhost [127.0.0.1]) by lpn-prd-vrout014 (Postfix) with ESMTP id CAFD1121B51 for ; Sat, 9 Dec 2017 18:07:34 +0100 (CET) Received: from lpn-prd-vrin001 (lpn-prd-vrin001.laposte [10.128.63.2]) by lpn-prd-vrout014 (Postfix) with ESMTP id C618711F94F for ; Sat, 9 Dec 2017 18:07:34 +0100 (CET) Received: from lpn-prd-vrin001 (localhost [127.0.0.1]) by lpn-prd-vrin001 (Postfix) with ESMTP id B0A5136B0C8 for ; Sat, 9 Dec 2017 18:07:34 +0100 (CET) Received: from [192.168.1.2] (unknown [151.32.51.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by lpn-prd-vrin001 (Postfix) with ESMTPSA id 78AB936B0BC for ; Sat, 9 Dec 2017 18:07:34 +0100 (CET) To: gentoo-portage-dev@lists.gentoo.org From: Michael Lienhardt Subject: [gentoo-portage-dev] Constraint-Based Dependency Solver for Portage: a prototype Message-ID: <0f376a7a-8ec1-1374-df2a-bc6a591eaa04@laposte.net> Date: Sat, 9 Dec 2017 18:07:36 +0100 User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.5.0 Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-portage-dev@lists.gentoo.org Reply-to: gentoo-portage-dev@lists.gentoo.org MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15; format=flowed Content-Language: en-US Content-Transfer-Encoding: 7bit X-VR-SrcIP: 151.32.51.19 X-VR-FullState: 0 X-VR-Score: 0 X-VR-Cause-1: gggruggvucftvghtrhhoucdtuddrgedtuddrvddvgdelkecutefuodetggdotefrodftvfcurfhrohhf X-VR-Cause-2: ihhlvgemucfntefrqffuvffgnecuuegrihhlohhuthemucehtddtnecunecujfgurhepvffhuffkffgf X-VR-Cause-3: gggtgfesthejredttdefleenucfhrhhomhepofhitghhrggvlhcunfhivghnhhgrrhguthcuoehmihgt X-VR-Cause-4: hhgrvghlrdhlihgvnhhhrghrughtsehlrghpohhsthgvrdhnvghtqeenucffohhmrghinhepohhssgho X-VR-Cause-5: gigvshdrohhrghdpghgvnhhtohhordhorhhgpdhgihhthhhusgdrtghomhenucfkphepudehuddrfedv X-VR-Cause-6: rdehuddrudelnecurfgrrhgrmhepmhhouggvpehsmhhtphhouhhtpdhhvghloheplgduledvrdduieek X-VR-Cause-7: rddurddvngdpihhnvghtpeduhedurdefvddrhedurdduledpmhgrihhlfhhrohhmpehmihgthhgrvghl X-VR-Cause-8: rdhlihgvnhhhrghrughtsehlrghpohhsthgvrdhnvghtpdhrtghpthhtohepghgvnhhtohhoqdhpohhr X-VR-Cause-9: thgrghgvqdguvghvsehlihhsthhsrdhgvghnthhoohdrohhrghenucevlhhushhtvghrufhiiigvpedt X-VR-AvState: No X-VR-State: 0 X-VR-State: 0 X-Archives-Salt: d802a016-5bf7-46da-87c6-2ba2bd04f3af X-Archives-Hash: 1db12054437ea3ce28247cfaf7b4b975 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