using CUDF for SAT solving

[Jackson Isaac]

On Wed, Mar 25, 2015 at 4:06 AM, Clemens Lang <cal at macports.org> wrote:
> Hi,
>
> ----- On 24 Mar, 2015, at 16:24, Jackson Isaac jacksonisaac2008 at gmail.com wrote:
>
>> I saw the apt-get and other implementations using CUDF. From what I
>> understood was that the cudf solver is installed on the machine and if
>> it is found we will send our portfile to cudf solver after
>> interpreting and modifying the PortFile format to cudf format.
>
> Yeah, somewhat. The CUDF format is a list of all available packages,
> though, so it wouldn't only contain the information from one Portfile,
> but the info from all Portfiles.
>
>
>> libCUDF C bindings are available so we could use that. Or we stick to
>> the Boolean SAT solving technique?
>
> We could either use libCUDF bindings or just write the CUDF file on our
> own – it's not a particularly difficult file format.

So one single CUDF file will contain information about all the
packages and dependencies?

I was going through the cudf 2.0 specifications:
http://www.mancoosi.org/reports/tr3.pdf and it says in one CUDF file
there would be a preamble, list of dependent packages followed by one
requested package.

> Using CUDF has the
> advantage of already "knowing" what dependencies and packages are, so we
> don't have to do the mapping to boolean formulas.
>

We can extract Portfile information using the dlist Datastructure
from which we can get the package to be installed and list of
dependencies and create a CUDF.

What to do with this CUDF that we get?
Do we need to implement a module which will solve (probably interpret)
this CUDF and then pass that information to the installer (after
displaying the output and confirming from the user) as I can't find
how will this cudf file solve the dependencies and conflicts? Is it
using libCUDF ? If so, we could implement our own file as you
mentioned above, so that we could add more features to it.

>
>> If we use Bool SAT solver, we will need to implement the wheel (didn't
>> quite understand what it actually means, but does it mean creating the
>> dependency tree and then finding the best plan).
>
> I was trying to say we should avoid "reimplementing the wheel", which is
> a play on words on "reinventing the wheel", which you'd normally try to
> avoid because, well, the wheel has been invented a couple of thousand
> years ago already.
>
>
>> CUDF already provides this and in an efficient way then we could
>> probably go with that since many package managers are implementing
>> them. One reason would be better and clean results using CUDF.
>>
>> So why not MacPorts also join in the league with them :)
>
> Yeah, that's what I'm thinking.
>
>
>> As there is already a cache with the dependency information, we can
>> update/better create another cache (cudfindex) with the required
>> information from PortIndex and checking for variants when we run port
>> install. This might not take ~15 minutes or so I guess as most of the
>> information is already there. Also, it depends on number of variant
>> combination as Mihai had mentioned.
>
> Yeah, I guess rather than dealing with all the dirty details right at
> the start we should do that and then later in the summer look into what
> needs to be done to get variants right.
>
>
>>> The problem is that this is not static. See above. There are 2^n*
>>> different states for n variants. For a port like mplayer-devel (or my
>>> own ports, mpv and audacious-plugins), the amount of variant
>>> combinations is *very* high and for each combination the dependencies
>>> differ.
>>>
>>> You do NOT want to record this in PortIndex, which is supposed to be
>>> fast cache.
>>
>> I don't think normal users will always make use of variant, also if
>> they do they won't keep changing the variants too much. Considering
>> the same variant would be passed in future, we could probably make use
>> of this cudfindex.
>
> Yeah, but even if the users might not use it a lot, the dependency
> management must still support it. It's a feature a MacPorts after all, and
> a lot of ports support it.
>
>
>> Also, I would prefer stable and reliable build rather than a fast and
>> shaky installation.
>
> Correct. I guess we can work on improving performance later, if it works
> reliably and produces correct results.
>
> --
> Clemens Lang



-- 
Jackson Isaac
S6 B.Tech CSE
Amrita Vishwa Vidyapeetham
jacksonisaac.wordpress.com
Github/JacksonIsaac