using CUDF for SAT solving

[Clemens Lang]

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. 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.


> 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