Skip to content

Change how requests are resolved to have strict order

Karel Koci requested to merge fix-condition-injection into master

The original implementation tries to satisfy maximum number of requests in given priority level. This has been seen as ideal solution because this way most of the user's requests are satisfied. This changes this behavior to rather be strictly defined. This means that we do not care about number of requests satisfied. We care only about priority of request and satisfy them in order.

This also removes error raised when there was Install and Uninstall request for same package with same priority. Now Install request is simply preferred.

This was required because of conditions. The demonstration of this issue can be done on two packages. Let's have package 'a' and 'b'. There are three requests of same priority:

  • To install 'a'
  • To unistall 'b'
  • To install 'b' with condition 'a' The intuitive resolution is that user clearly wants to install 'a' and not to have 'b'. The third request need not apply as there is more accurate request to not have 'b'. The original implementation tries to solve this by maximizing number of satisfied requests. This has three solution, which is on its own pretty problematic. The first solution is the intuitive one. Second solution is to install 'a' as well as 'b'. But the third solution is to not install any package. This is because third request can be satisfied either by installing 'b' or by not installing 'a'. All of these solutions are equivalent in solvers conditions as they all result in only one of the requests to not be satisfied, thus we have no direct way to hint solver what to do. What is even worst we even don't know what should be the correct solution without defining additional resolution rules.

Using the new algorithm the solution for problematic request combination is simply that we order them using our new defined rules, that is also the order they are ordered in example. Now we take and resolve one request at the time. We can clearly satisfy installation of 'a' and thus first request. We can also satisfy not-installation of 'b' and thus second request. The third request now can't be satisfied and thus resulting in just 'a' installed.

Full order rules are described in documentation. Reasoning for them is also hinted but to be complete there are also alternative orders we could choose. The reasoning is as follows:

  • We need to resolve critical packages first to make sure that all of them can be satisfied (so we would not close some combination by regular requests).
  • The user specified priority has to be abided.
  • The requests without condition are preferred as they clearly state what should happen. Conditions can have side effect such as forcing some specific combination to satisfy given request. This is of course highly undesirable as condition should control only if request is satisfied not to influence packages specified in condition. Given the nature of satisfiability solver this backward injection is just going to happen so we instead simply prioritize requests that have no such effect.
  • Another major change buried in these changes is that Install and Uninstall requests for same package no longer raise error. We prefer Install requests as a choice. The removal of error is because it was arbitrary anyway. There are simple ways Install and Unistall requests can be in direct collision without specifying same package name, such example being if package 'a' depends on 'b' and there is request to install 'a' and to unistall 'b'.
  • The last resort order is order of definition is scripts. In the effect this is not that important. This affects only requests that have same priority, same type (install or uninstall) and both have or not have condition. Such requests effectively want the same thing so they hopefully should not collide that much in their requests.

Merge request reports