search

pypa / pip

The Python package installer
https://pip.pypa.io/
MIT License
9.4k stars 2.99k forks source link

New Resolver: technical choices #7406

Closed pradyunsg closed 4 years ago

pradyunsg commented 4 years ago

This issue is an overflow from #6536, intended to be scoped for discussion of the technical choices and tradeoffs for implementing a dependency resolver within pip.

uranusjr commented 4 years ago

My understanding to the existing choices: (I also list the current resolver as a baseline, although it likely should not/will not have a place in the eventual implementation under any circumstances)

The current resolver

Mixology (Poetry)

libsolv

ResolveLib / Zazo (more or less share the same characteristics)

youtux commented 4 years ago

About the Mixology being coupled to Poetry, I offered my help to @sdispater to help extracting it to its own package.

pradyunsg commented 4 years ago

@youtux Thanks! ^>^

One of the things worth noting here (as I hinted at in https://github.com/pypa/pip/issues/6536#issuecomment-553453055) -- it'd be nice to have the same abstractions as resolvelib/zazo in mixology. It's likely that both would have to change the abstractions a bit to make things easier but having "swappability" between these would be great to have IMO.

Assuming that work goes along well, mixology would basically become an independent port of PubGrub to Python -- https://medium.com/@nex3/pubgrub-2fb6470504f -- that can consume a "provider" from our common abstraction layer.

@uranusjr helpfully explained why SAT+Python packaging is an unexplored problem here: https://github.com/pypa/pip/issues/6536#issuecomment-558297132

If someone is aware of a SAT solver that allows for incrementally adding clauses, that'd be great! I'd looked at http://www.satcompetition.org/ in the past, to see what all "fast" SAT solvers are going around and if there are things we can use from them. IIUC, there isn't any SAT solver in the wild that allows adding clauses and certainly none that are written in Python (and efficient).

I'd love to be wrong here though. :)

pradyunsg commented 4 years ago

Looking at libsolv, I don't think we can use that as it stands today. From the docs: https://doc.opensuse.org/projects/satsolver/11.3/

The solver gets initialized by passing it the complete pool (all Solvables) and a single Source (called 'system', representing the installed Solvables).

We don't have the complete pool, so that wouldn't work for us (see https://github.com/pypa/pip/issues/6536#issuecomment-558297132)

uranusjr commented 4 years ago

I think the idea was to extend the pool as you go, something like: (pseudo code)

pool = collect_solvables(immediate_dependencies)

while True:
    try:
        result = sat.solve(constraints, pool)
    except UnrecognizedPackages as e:
        pool.add_packages(collect_solvables(e.names))
        continue
    except Unsolvable:
        # There must be no possible solutions.
        raise
    # If we reach here, all mentioned packages are recognized,
    # and a solution has been found.

Conceptually this could work, but I have no idea how well, and how suitable libsolv is to be used like this. I’m willing to believe when I actually see an implementation.

pradyunsg commented 4 years ago

I concur with you and am basically in the same position: I'm sure it's technically possible to have incremental addition of clauses to SAT solvers -- I don't know if there's any that we can easily vendor and what the use looks like.

brainwane commented 4 years ago

Ping @wolfv and @SylvainCorlay to follow up discussion here from https://github.com/pypa/pip/issues/6536#issuecomment-558194932 .

ilanschnell commented 4 years ago

Hello, I wrote C bindings for http://fmv.jku.at/picosat/ called pycosat back in 2013. Looking at the code, I don't think it would be too hard to add clauses iteratively, and the same is probably true for other solvers as well. Having implemented the first version of conda which uses a SAT solver (pycosat), I can say the following (and this is also true from other SAT problems I've worked on): The construction of clauses as Python objects is at least as expensive as the SAT problem itself. Picosat is very efficient and the memory footprint of the clauses is much smaller once they are passed to the C level. Having said this, I don't think incremental addition of clauses is a big problem. That is, you simply append more clauses to your list, and call the solver again.

@pradyunsg I assume that this is a necessary requirement because not all PyPI packages are initially available, and hence the dependency are not completely know.

pfmoore commented 4 years ago

I assume that this is a necessary requirement because not all PyPI packages are initially available, and hence the dependency are not completely know.

That's correct. There are two key reasons: (1) we only download data from PyPI as needed, and downloads are costly because (even for wheels) the full package must be downloaded to access the metadata, and (2) PyPI metadata is not always statically available - for sdists, the only guaranteed way to get the metadata is by running (at least part of) the build process.

sdispater commented 4 years ago

I finally managed to extract Mixology from the Poetry codebase, see https://github.com/sdispater/mixology

There is an example showing how the library should be used in the README. Mixology only uses three abstract concepts to work: Package, Version and Dependency, see https://github.com/sdispater/mixology/blob/master/mixology/package_source.py to know what is expected from each of these concepts. They must be exposed via a PackageSource subclass which must implement the required methods.

This is an early draft but should work in most cases. Any feedback is welcome.

Note that this version is not currently used in Poetry, which still uses a custom one, but this will eventually be the case so that might help to have a more complex example of Mixology's usage in a "real world" scenario.

@youtux Sorry for not getting back to you. I was so focused on this that I completely forgot to respond to your email. Feel free to take a look at the code and if you see anything that can be improved, please let me know :-)

youtux commented 4 years ago

No worries, I’m glad you managed so quickly! Great job!

pradyunsg commented 4 years ago

That is, you simply append more clauses to your list, and call the solver again.

If there's a way to prevent the solver from losing "tree-trimming" state between these calls (I think for picosat, that's only the learned clauses), then yes, that's what we'd want to be able to do here in an ideal scenario.

We'd still have a few major challenges though:

  1. packaging up a implemented-in-C SAT solver for distribution with pip
    • implications of this have been discussed above
  2. crafting the model for translating the requirements into SAT expressions in a partially explored graph:
    • representing "this dependency is not available until further exploration"
    • detecting the difference between conflict in dependency requirements vs need more dependency information
  3. generating decent error messages
    • I don't have any idea on prior art for this TBH.

For 2, the only approach that I can think of is having variables represent "need exploration for \<name>" and keeping UNSAT as representative of dependency conflicts -- this seems super tricky to craft based on my not-so-sharpened intuition.

JustinCappos commented 4 years ago

The "download as needed" aspect is definitely a complicating factor here.

As I understand it, evaluating candidate packages can do dynamic things wrt dependency management, etc. which also change things. Do I have this right?

Note, I may be misunderstanding things. Please forgive errors and help to set me straight. 😄

Assuming I'm not totally off base, these other things I've bolded below could be added to @uranusjr 's classification:

The current resolver

  • Advantages: Kind of works. No backward incompatibility.
    Also handles dynamic dependencies and download as needed.
  • Disadvantages: It’s bad and we don’t want people to use it. Perhaps not the easiest to understand when things go wrong.

Mixology (Poetry)

  • Type: Simple PubGrub

  • Advatages

    • Has current Python packaging usage.
    • Easy to vendor (pure Python). Very clear and understandable output. Efficient computationally.

  • Disadvanteges

    • Needs extra work to decouple from Poetry.
    • Less current understanding (documentation) to implementers/maintainers (unless Sébastien becomes a pip maintainer). Doesn't handle dynamic dependencies or download as needed (as I understand it).

libsolv

  • Type: SAT

  • Advantages

    • Battle-tested.
    • The most performant (I believe).

  • Disadvantages

    • The most difficult to vendor (implemented in C).
    • Likely needs a pure-Python fallback (does not currently exist).
    • Needs most work to wire up (no known Python packaging usage). Doesn't handle dynamic dependencies or download as needed (as I understand it). Also it isn't clear why it made a specific decision. It just finds some valid solution but the result may be unintuitive...

ResolveLib / Zazo (more or less share the same characteristics)

  • Type: Simple backtracking

  • Advantages:

    • Easy to vendor (pure Python).
    • Known to be compatible with Python packaging. Handles dynamic dependencies and download as needed. Should hopefully be understandable, but is somewhere between the PubGrub / SAT.

  • Disadvantages

    • Lacks real-world use. The least efficient computationally.
uranusjr commented 4 years ago

Not sure what counts “dynamic” in the sense you have in mind (there are quite several levels of dynamic-ism in the current ecosystem). Does environment markers count? (e.g. add dependency X only if on Windows)

I ask because pip’s particular resolver requirements nullify the dynamic problem. Specifically, pip only needs to care about one platform (the one it’s running on), so (most) dynamic dependencies can trimmed/expanded eagerly. So at least for PubGrub the problem is not significant (if at all), if I understand it correctly.

pradyunsg commented 4 years ago

@sdispater would likely have more context to comment on this here, around poetry/mixology's implementation of PubGrub.

Based on my reading of PubGrub's technical documentation, PubGrub has "lazy formulas", intentionally meant to address the "download as needed" requirement in dependency resolution scenarios -- https://github.com/dart-lang/pub/blob/master/doc/solver.md#lazy-formulas.

sdispater commented 4 years ago

Yes, PubGrub supports the "download as needed" scenario which is why I settled on it when developing Poetry. It helps the resolver tremendously to have all the dependency information beforehand (this is particularly true for packages like botocore where a pool of hundreds of version can be cut down to a few dozens) but it's not mandatory.

JustinCappos commented 4 years ago

Okay, so once again please forgive my potential confusion here.

As I understand it, you have to download a package in order to have the scripts you need to run to see how those scripts may change dependencies dynamically. For example, if a version of a package does look at the set of dependencies and the platform and then dynamically decide its dependencies, how can you know what its dependencies are without downloading and running it? If so, then it seems you either have to download and execute package scripts or some crazy legacy situations won't work right. If you do download and execute everything sequentially with backtracking, then I think this would devolve to the simple backtracking case, which would be a shame, since PubGrub has some nice advantages.

Even if I do understand this correctly, I'm not saying that dynamic alteration of dependencies would be a bad thing to remove. It just may require a bit more work to see how to keep legacy compatibility in all "important" cases. It certainly seems like removing dynamic alteration of dependencies would make dependency resolution easier for the user to understand, regardless.

chrahunt commented 4 years ago

you have to download a package in order to have the scripts you need to run to see how those scripts may change dependencies dynamically

Wheels provide static dependency metadata, and more projects are providing wheel-format packages every day. For source distributions that is correct, we have to download and execute something in order to get metadata. I started a discussion here with an idea for letting source distributions opt-in to static metadata, but haven't acted on it since. I don't know if this would need a PEP or just an update to the Core Metadata spec.

dralley commented 4 years ago

Hey, I'm a little late to this discussion, but I have some experience with actually using Libsolv (Python bindings) for several months so I'll chime in.

edit: I just noticed that the author of Libsolv commented in one of the other threads which also has a more complete discussion, generally. Definitely listen to them, not me.

I concur with @uranusjr and @pfmoore that the lack of having a local copy of all the package metadata is a problem for using Libsolv (and probably SAT solvers generally). Every platform that Libsolv currently supports (RPM, Debian, Arch, Conda) doesn't have this problem because they have a single file or JSON blob that provides all the package metadata up-front and they can load up the pool of "solvables" very quickly.

Libsolv also has a bunch of platform-specific code to handle the differences between RPM, Debian, Conda, and so forth. The same would probably be necessary for Python.

So, the concerns as expressed by others are accurate based on my experience with it. It's probably not a good fit.

As a sidenote:

Having such repository information available would be super beneficial regardless and is worth considering as a "long-term goal" of PyPA, although it's definitely way out of scope for this project. I don't have numbers but I can only imagine that being able to do depsolving 100% locally without waiting on incremental API calls is a big win for speed, and probably infrastructure management as well. At least a couple of other language-specific package managers use this approach, like cargo.

pradyunsg commented 4 years ago

I think this would devolve to the simple backtracking case, which would be a shame, since PubGrub has some nice advantages.

PubGrub's derivation graph would still be able to construct a "reasonably" good message for why the conflicts occurred -- something we wouldn't have with a simple backtracking algorithm. (IIUC)

JustinCappos commented 4 years ago

PubGrub's derivation graph would still be able to construct a "reasonably" good message for why the conflicts occurred -- something we wouldn't have with a simple backtracking algorithm. (IIUC)

Yes, I really like that aspect of the system too. I do think it would be possible to take failed decision information out of simple backtracking resolution and reconstruct what is essentially the PubGrub output. However, it seems more natural to just use PubGrub as an algorithm assuming that the dynamic dependency manipulation issue isn't important in practice.

pradyunsg commented 4 years ago

I do think it would be possible to take failed decision information out of simple backtracking resolution and reconstruct what is essentially the PubGrub output.

I concur -- OTOH PubGrub's derivation graph does make that process easier in some sense, by surfacing relevant information more directly in a data structure that follows the state of the resolver itself.

Another thing that's pretty tempting about the PubGrub port, is that it's already implemented and tested out in the wild, as an opt-in users of poetry.

pfmoore commented 4 years ago

I've been looking at mixology today, to try to get a feel for how its API would fit with pip. One thing I hit was the fact that as far as I can see, Mixology uses its own constraint abstraction (the Constraint class), which doesn't seem to be interoperable with packaging.SpecifierSet, and I don't see an obvious way to convert between the two.

I think this could be a problem for us, as we'd presumably want to stick with PEP 440, as implemented in packaging - and if we need to convert between that and mixology's custom constraint type, that could be an annoying impedance mismatch. @sdispater am I correct in this? Or is there a way to get Mixology to work with the SpecifierSet for constraint semantics?

Apologies if this is easy and I've missed something obvious - I'm just starting to try to get my head round the library.

sdispater commented 4 years ago

@pfmoore Mixology only understands its own Constraint class. So you will need to convert a SpecifierSet to something Mixology can understand. You can check the example here https://github.com/sdispater/mixology#example and the convert_dependency() method to see how.

As long as you can represent a SpecifierSet as a Range, a Union of ranges or an intersection of any of the two, it should work.

pfmoore commented 4 years ago

As long as you can represent a SpecifierSet as a Range, a Union of ranges or an intersection of any of the two, it should work.

Thanks, that's what I thought. Sadly, there's no public API for introspecting a SpecifierSet in a way that would let us do that. So we'd probably have to either dig into the internals (nasty) or add an introspection API. Or write our own requirement parser (which defeats the purpose of having a standard and a library that implements it, IMO).

Let's just call it a disadvantage for Mixology in the analysis of resolver options above for now. We can work out the details later.

@pradyunsg @uranusjr I know you've looked at the resolver options in more detail than I have - is this something you were aware of, and if so did you have any ideas on how to address it?

pradyunsg commented 4 years ago

@uranusjr and I have not discussed this in detail.

I was aware that poetry/mixology have been using a different version/specifier handling code, but I'd definitely not thought about the possibility that it could require more operations than SpecifierSet provides, even though I'd thought of that when I was looking at PubGrub itself. 🤷‍♂

Looking more closely at the implementations here, it does seem like it would not be easy to implement a mixology's Constraint-like object with packaging's SpecificerSet internals either -- specifically the overlapping and intersecting checks. It'd certainly be possible though, if we want to add more set-like functionality to SpecifierSet, which looks like a significant multi-week task.

Counting this as a disadvantage of going the mixology route, sounds reasonable to me. :)

pfmoore commented 4 years ago

Cool, for now I can continue playing with prototypes using resolvelib. (If I'm honest, I prefer resolvelib's set of abstractions, but I'm trying not to let personal preferences influence things at this stage).

Having a clean, well-defined interface to the resolver means we can always revisit any decision, in any case 🙂

pradyunsg commented 4 years ago

Given that there are major concerns around vendoring a SAT solver and a significant difference between mixology's version-range representation from packaging's specifier-based approach, we seem to be landing on the resolvelib/zazo model for the implementation.

sdispater commented 4 years ago

I just took a look at resolvelib and it seems one of the inspirations is Molinillo. That's what I settled on initially for Poetry but the algorithm is not at all efficient for the Python ecosystem due to the fact that you need to download distributions to discover dependencies which lead to catastrophic performances on conflicts and when backtracking was necessary, even with a cache.

That's the reason why I implemented the PubGrub algorithm because, from my experience, it's the one most suited for the Python packaging ecosystem.

The other implementation in languages like Rust (Cargo) or Molinillo (Ruby) work because they have a static registry of package dependencies.

And it seems that an alternative package manager in Ruby (https://github.com/gel-rb/gel) is in progress and uses the PubGrub algorithm. It seems to give significant speed bumps compared to bundler.

uranusjr commented 4 years ago

Personally I agree PubGrub is the best technical choice for Python, and also the best choice for pip in theory. The problem here however is that there is no Python implementation suitable for pip’s usage. As mentioned above, it is difficult to integrate Mixology into pip due to data structure incompatibilities; on the other hand, both of our backtracking choices are designed to fit well into pip.

I’ve been thinking about implementing a PubGrub resolver (maybe based on Mixology, maybe not) that expose a similar interface to ResolveLib and Zazo, that can be better used by projects without forcing them into using dedicated data structures. But I don’t believe it is the best use of my time in the near term given my responsibilities (including bringing a resolver into pip within a deadline).

Given that proper resolvers are functionally interchangeable, my choice now is to pursue a more reachable goal. [insert Perfect is the Enemy of Good cliche here] But I also intend to help line up goals and efforts for a future alternative implementation, and work on that after pip has something to show for.

pfmoore commented 4 years ago

+1 on what @uranusjr says. I think the key here is that we're landing on the resolvelib/zazo interface, because it doesn't have any fundamental technical issues, and it comes with an implementation that's sufficiently good right now (and also because it's a nice, flexible API, IMO, but conceded people's opinions may vary there).

Implementing a PubGrub algorithm to work behind something close to the resolvelib API would be nice, but the priority, specifically for the funded work, is to pay off the technical debt that the pip resolver is currently fighting with, and then implement a replacement resolver. Having to implement a better resolver is additional work that IMO comes into the "nice to have" category - if we have the time, then let's do it, but if not, let's get pip to a state where plugging in a replacement resolver isn't the massive problem it is right now, and follow up with a better resolver later.

The other choice would be to go for Mixology, but the showstopper there is the fact that the API doesn't integrate with packaging.SpecifierSet based requirements. Modifying the implementation and API to fix that is another piece of additional work, but unlike the resolvelib case, if we don't do that extra work, we don't have any new resolver.

@sdispater one thing that would be useful is if you have some good real-world examples of where dependency discovery does become a problem. Having those as test cases and/or examples we can measure performance against would help a lot.

sdispater commented 4 years ago

@pfmoore I understand the constraints and requirements to integrate a new resolver into pip. I was merely pointing out that I already went through what you are currently going through, so I was just sharing my experience to warn about the issues and shortcomings that you will most likely stumble upon when implementing your own resolver.

And even PubGrub is not the silver bullet here. As long as we need to download distributions to retrieve metadata and dependencies we will always hit a bottleneck and we won't be able to make optimizations to existing algorithms.

An example of this is botocore which has something like 900 releases and if you hit a conflict with it you will need to discard releases one by one, downloading wheels or sdists each time, because we don't know the dependencies beforehand. If we knew them we could reduce the candidates to something like 30 releases.

pfmoore commented 4 years ago

Thanks @sdispater - that's really helpful, I hope I didn't come across as dismissive of what you are sharing here, I definitely didn't mean to if I did!

I'll definitely look at botocore - it's a good example, I've been thinking mostly in terms of complex dependencies and not so much about cases with massive numbers of candidates. As you say, that's largely a problem with the ecosystem, where we have to download and potentially build to get dependency data. I'm slightly hopeful that pip's caching of downloads might alleviate the problem here - at least we'll only download each of those releases once! And maybe we could add a persistent dependency cache - map project/version to dependencies once and save the data on disk. Is that something you've done any investigation on?

sdispater commented 4 years ago

@pfmoore

I hope I didn't come across as dismissive of what you are sharing here, I definitely didn't mean to if I did!

Not at all!

I've been thinking mostly in terms of complex dependencies

One example i have is pyrax==1.9.8. There is a lot of transitive dependencies incompatible with each other. This one is also easily solvable by having the dependency information available beforehand but there are more dependencies involved.

And maybe we could add a persistent dependency cache - map project/version to dependencies once and save the data on disk. Is that something you've done any investigation on?

That's already what Poetry is doing, the package metadata is stored locally in a cache which speeds up the resolution process drastically.

chrahunt commented 4 years ago

Another option for wheels could be to only download the dependency metadata instead of the whole wheel. For example, I have a script here for getting a list of all files in all wheels in PyPI that only downloads the bytes required to get the zip central directory and each of the local header entries in the zip. If we go that route we'd probably need to know how it may impact the caching in front of PyPI, though.

uranusjr commented 4 years ago

@chrahunt Ah briliiant idea! I’m going to steal it for sarugaku/resolvelib#27. I wonder how well HTTP range requests are supported in common HTTP server implementations…

brainwane commented 4 years ago

@ewdurbin ping re: thinking about how this will affect PyPI and whether PyPI could facilitate this information need in any way.

chrahunt commented 4 years ago

I wonder how well HTTP range requests are supported in common HTTP server implementations…

We could decide to do it only after an HTTP HEAD request shows that it is supported. We may also want to do that anyway and only use this approach for larger files (as indicated by Content-Length in the response) to avoid potentially taking longer for small files because of the latency for multiple requests.

sbidoul commented 4 years ago

FWIW is saw an experiment with partial downloads at https://github.com/python-poetry/poetry/pull/1803

ewdurbin commented 4 years ago

As far as HTTP range requests, PyPI's CDN currently supports these as is, caches fetch the full artifact from origin and are able to serve range requests from that object.

techalchemy commented 4 years ago

the resolver algorithm isn't the particularly difficult part of this question -- before doing a ton of research, my early iterations on resolution looked basically like pubgrub. The challenge is always metadata -- the edge cases are not really only at the edges, pretty much every install operation requires executing a setup.py.

As far as HTTP Range requests, isn't this basically just a workaround for poor metadata availability? Can we just scan the wheels and make the metadata for each wheel available? For platform- and python-version specific wheels we could even do the courtesy of adding on a 'markers' field in the json api with the additional constraints

dstufft commented 4 years ago

Pip cannot rely on the JSON api as is because it’s a non standard api. If we wanted to start using it we would need to write a PEP that standardizes it.

Sent from my iPhone

On Feb 9, 2020, at 3:05 PM, Dan Ryan notifications@github.com wrote:

 the resolver algorithm isn't the particularly difficult part of this question -- before doing a ton of research, my early iterations on resolution looked basically like pubgrub. The challenge is always metadata -- the edge cases are not really only at the edges, pretty much every install operation requires executing a setup.py.

As far as HTTP Range requests, isn't this basically just a workaround for poor metadata availability? Can we just scan the wheels and make the metadata for each wheel available? For platform- and python-version specific wheels we could even do the courtesy of adding on a 'markers' field in the json api with the additional constraints

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

uranusjr commented 4 years ago

Can we just scan the wheels and make the metadata for each wheel available?

The answer is custom indexes (and --find-links sources). Even if PyPI does this, pip still needs to implement medatada-via-wheel because the API isn’t required (can’t be, at least in the short term). So we’ll need to focus on implementing that first, and work on improving metadata availability afterwards.

That said, if anyone has free time to put efforts into standardising the JSON API (and metadata availability in general), it would be most welcomed. Please feel free to propose!

tgamblin commented 4 years ago

Hi folks. I'm late to this conversation, but @brainwane asked me to add some comments based on some discussions we had at the ECP meeting she was at last week.

ASP & SMT Solving

I'm in the process of redoing the concretizer (what we call the resolver) in Spack. The main difference between Spack and pip, at least in this regard, is that (AFAIK) pip is resolving mainly packages and versions, while Spack is throwing a lot of other things into the solve as well. Specifically, we're resolving packages, versions, compilers, features and options, compiler flags, target microarchitectures, compiler flags, and some ABI issues like different implementations of the same interface (like OpenMPI & MPICH for MPI, or OpenBLAS vs. MKL for BLAS/LAPACK).

The Spack solver doesn't just take any valid solution, it tries to find an optimal one according to a fairly long list of criteria. From what I understand, pip, PubGrub, libsolv, etc. "optimize" by exploring versions from newest to oldest -- and doing multi-criteria optimization would be hard to add. So far, I've been able to put together a solver that optimizes for version preferences, build option preferences, targets, preferred compilers, interface implementations, and things like DAG size.

I'm currently using Clingo, the Answer Set Programming (ASP) solver from the Potassco suite. You may have heard of it as it's what PubGrub was inspired by (though Natalie ended up writing her own solver based on the book and didn't use the ASP solver directly). I'm also looking at Z3 from Microsoft Research, which is probably the best known SMT solver. There are more details in this FOSDEM talk from a week ago.

Fetching metadata & incremental solving

Anyway, from the discussion above, it seems like fetching remote metadata is the biggest issue at the moment, and you'd need something that can do incremental solving. Spack comes with all its own metadata (like homebrew), so I did not have to go this route, but both Z3 and Clingo can do incremental solving. See this post on Z3 and Section 6.3 in the Clingo guide.

I'm not sure exactly how this would need to be formulated for pip's particular case, but both of these packages have python bindings that you can use to add new clauses to existing solves, and the solvers are fast (Clasp, clingo's solver, has performed well in competitions, and Z3 is extremely well known in the SMT world). You can't reuse all the things the solver has learned, but it seems you can recycle the solver state from one stage to another.

Optimization

I bring up the optimization thing based on a recent discussion on discourse. If you did ever want to prefer some tags from a repo over others -- as will likely be the case if you start solving for compatible/performant binaries -- the ability to combine SMT/ASP and optimization will be really handy. It has been extremely liberating to be able to do this in the Spack solver; I think it would've been a big pain to introduce it on top of pure SAT.

Error messages

This is the part I'm still working on. Currently Clingo doesn't have great ways to get information on why a particular problem is unsatisfiable. Z3 seems to have the ability to extract unsatisfiable cores (this is what Conda seems to do), and it can also generate proofs of why a problem is unsatisfiable. I am still working on how I might parse such a proof out of Z3 (it's not trivial) but it's essentially a more general version of what PubGrub does -- PubGrub is building up a proof (through all the learned conflicts of why a problem is unsatisfiable) and generating smart error messages from them. I think you could do something similar with Z3.

Summary

Anyway, that's the best i could do to relate what we're doing to pip. Hope it helps, and I'm happy to chat about this on a call if people are interested.

dralley commented 4 years ago

Hi all,

I know Libsolv and SAT solving in general has already been effectively ruled out for various technical reasons (chiefly the metadata availability problem), but I just wanted to announce that I've now published Libsolv binary wheels to PyPI: https://pypi.org/project/solv/

That takes care of some of the distribution-related "disadvantages" that were listed above, although it does not solve the other problems with SAT solvers in this particular scenario. Still, if anyone would like to experiment, it should be much easier to do so now.

Here's the patch that enables building it as a Python package: https://github.com/openSUSE/libsolv/compare/master...dralley:python-package

sub-mod commented 4 years ago

This topic seems like a good one to talk about in the packaging summit.

pradyunsg commented 4 years ago

@sub-mod I don't think this would still be up for discussion when the Packaging Summit happens - work on the resolver has been funded through grants (see https://wiki.python.org/psf/Pip2020DonorFundedRoadmap) and we're working on "bringing a resolver into pip within a deadline".

The Packaging Summit happens really late in that timeline, to be making such a fundamental decision about the direction of the funded work (since knowing which API we're going to integrate with, helps determine which parts of pip need refactoring).

cosmicexplorer commented 4 years ago

I left a comment at https://github.com/pypa/pip/issues/6536#issuecomment-594975052 which describes how I believe static dependency information may be performantly queried for use by a SAT solver. #7819 contains a prototype of these techniques, used for a potential pip resolve command (just using the current greedy resolution algorithm). I believe I may be able to hack around a bit more and try to get real performance numbers for the techniques from #7819 as applied to an actual SAT solver in the next 2 weeks.

cosmicexplorer commented 4 years ago

I have expanded the pip resolve prototype from #7819 to use the pure-python ResolveLib library, in a new file src/pip/_internal/resolution/resolver.py -- see https://github.com/pypa/pip/compare/master...cosmicexplorer:requirement-dependencies-cache?expand=1. 

> time pip resolve -d tmp/ --quickly-parse-sub-requirements tensorflow==1.14
Resolve output:
tensorflow==2.1.0 (https://files.pythonhosted.org/packages/35/55/a0dbd642e68e68f3e309d1413abdc0a7aa7e1534c79c0fc2501defb864ac/tensorflow-2.1.0-cp37-cp37m-macosx_10_11_x86_64.whl#sha256=2e8fc9764b7ea87687a4c80c2fbde69aeeb459a536eb5a591938d7931ab004c2)
termcolor==1.1.0 (https://files.pythonhosted.org/packages/8a/48/a76be51647d0eb9f10e2a4511bf3ffb8cc1e6b14e9e4fab46173aa79f981/termcolor-1.1.0.tar.gz#sha256=1d6d69ce66211143803fbc56652b41d73b4a400a2891d7bf7a1cdf4c02de613b)
...
5.05s user 0.50s system 88% cpu 6.264 total

This is not quite as fast as the original greedy pip resolve algorithm with the changes from #7819 (~900ms), but playing around more with the preference weighting might get us closer. As described in https://github.com/pypa/pip/issues/6536#issuecomment-594975052, I'm now going to experiment with libsolv, and hopefully will be able to figure out a reliable way for pip to build the C source code too along the way.

pradyunsg commented 4 years ago

We chose to go ahead with the resolvelib API (see #7317 for more details), and are open to changing the underlying resolution algorithm in the future.

We're grateful to all of you for your thoughts, which we tried to learn from -- sorry that we did not get as thorough a consultation as we would have if we'd had more time.

I'm closing this issue to reflect that we've made this decision, and to reduce the chances anyone will be confused about what decision we made. We are open to revisiting this discussion in 2021, in case we need to replace resolvelib or change the underlying resolution algorithm.