RFC Add external solver

[phadej]

Shortly: Allow to use external program for dependency solving.

Motivation: Even after the solver is split into a separate package, plugging new solvers into cabal-install would require it to (optionally) depend on new solver packages. Non-dependent - "plugin" - approach, where cabal-install executes external process would help with this.

For example I would like to experiment with SMT solvers, matrix.h.h.o might want to use own solver to exploit controversial install plans. Also experimenting with current solver would be easier, as one could have different variants, yet single cabal -executable.

Details:

• Input: constraints and preferences (AFAICS what is installed and what we want to be installed are the same from solver point of view,)
• Output: exact-configuration
• Format: ?

ping @kosmikus, @grayjay, @ezyang, @BardurArantsson

[kosmikus]

@phadej So in this proposal, it's the external solver's responsibility to read the package index?

(Also, let's talk about SMT at ZuriHac.)

[phadej]

@kosmikus

it's the external solver's responsibility to read the package index?

I'd say: yes.

I cannot come with easy way to transfer the index data, also reading the index yourself isn't that hard.

There are hidden problems though

• features like --index-snapshot (RFC: --index-snapshot <posix-time> #3378) which preprocess the index. Each external solver has to support it.
• format changes

[ezyang]

I am fine with this in principle but there needs to be a more detailed proposal, e.g., looking carefully at the input types of the solver and proposing a format, dealing with the hidden problems, etc.

[kosmikus]

@phadej Indeed, there are various index-processing steps that cabal-install unfortunately applies, and this complicates things significantly. Just to name one additional example: --allow-newer is implemented via index-preprocessing. I've often argued that these would be better done within the solver. But I guess there are a few contributors who are a bit more scared to touch the solver than to add a preprocessing step.

[phadej]

I would refrain from specifying too much details, the requirements and problems would be uncovered by implementation (the PR).

Few details:

• format will include cabal-install version.
• I'd like external solvers to be implementable as interactIO :: ByteString -> IO ByteString, where IO is only used by solver to access it's own external inputs

[phadej]

And probably we would need to preprocess index anyway, to apply manual flags etc. I'll have to think about how to stream package index into external solver.

[ezyang]

It's fine to write some code to prototype it. But this is the sort of thing where, eventually, you need a full specification (that other people can refer to when they write their own solver), so before any code gets merged, that needs to be written down somewhere.

Do you plan to develop an alternative solver in parallel with the external solver? That would help keep the interface from being too current solver specific. SMT seems like a good fit; ostensibly the top-down solver also counts?

[kosmikus]

I've already successfully used an SMT solver with the current internal solver interface, with the single change that the solver needs to be allowed to do IO (but that's a trivial change).

[grayjay]

See #1783 for a discussion of alternative solvers.