Hi everyone, I'm Ryan. I'm going to give a talk on basically formalizing dependency resolution
and trying to show that every ecosystem is kind of doing the same thing underneath the
hood. As the title says, is a formal model so there will be a bit of Greek but I'm going
to try and get the intuition across as well. So there are a lot of package managers out there
as I'm sure everyone in this room knows. Every language and operating system has something else
going on. They each have subtly different semantics for dependency resolution. This fragmentation
prevents projects written in multiple languages from managing their dependencies in a unified
way and the mechanisms for depending on system dependencies are often sort of ad hoc and
unversioned. And that means there might be, you don't have filled knowledge of your dependencies
basically like your language package manager doesn't know what's going on with you system
package manager. So I present to you the package calculus, which is a small formalism trying to capture
the course semantics of dependency resolution. But there's hopefully able to capture the diversity
out there in the world which I'll get onto. So we have n as the possible package names v as the
possible package versions p as the Cartesian product of these two sets which means a package as
a name version pair and r as all the packages which exist for example in a repository.
We define the delta as a dependency relationship from a package to a package name and a set of
versions that you depend upon that package with. As in I depend on library A with versions 1.1 to
two for example. And given a set of the dependency relation and a root package R we define a resolution
s as valid if it one includes the root to satisfies the dependency closure. So for every package
in the resolution for each dependency of that package there has to exist a package in the resolution
that has the same name and a version that is in the version set. And also there is this criteria
version uniqueness. So if there's two packages in the resolution with the same name they have to have
the same version. Is that making sense so far? Okay. So for example we we can have this dependency
relation where we have a 1 depending on b1, a 1 depending on c1, b1 depending on d with versions
2 and 3. And the solution to this is to select d2 and all the other packages. And we can
diagram this as a hypergraph essentially where we have an edge from a package to a set of packages
it depends upon. This is NP complete finding the resolution to satisfy a root dependency relation.
The proof is via a reduction from three set which I will admit to save on a bit of time.
So as you probably know modern package managers often employ sat to solve this problem.
So an example of how you could do that in the package calculus is using a variable to represent
each package in the resolution which is true if the package is included in the resolution.
So a variable for each package in the repository which is true if it's in the resolution.
And then the conjunction of every dependency where we say we either don't have the package
which is depending upon the other package or we have any package which has the name we depend on
with a compatible version. And we can we can translate this to conductive normal form for a
set solver. And a similar thing for a version uniqueness if we have two packages in the
repository they they they they can't be in the resolution with the same version.
This has pretty bad complexity for a normal sat solver but a sat solver with an at most one primitive.
It's fine and this works in the real world. This is nothing super novel.
So we've described compatible versions as a set so far but in the real world you
can normally express version dependency versions with a range and this is predicated on having an
ordering for these versions. So this is basically to say that given a range of versions we can
collapse this to a set given a repository pretty intuitive. And we can talk about the freshness
of a resolution given this version ordering. So most ecosystems prefer to use the highest
compatible version. And we can make the sat solver prefer this by putting the freshest versions
earlier in the clause. And if it tries the clause variables in order it will prefer the more
fresh versions. So I think those systems don't do this. I think go prefer to the minimum version.
I'll get onto go in a little bit. There is no guarantee that there is actually a single maximum
resolution. For example in this scenario we have a depending on b with versions 1 or 2 and c with
versions 1 or 2. But b2 depends on c1. So we can't select c2. So there's a trade off there.
You can either select b1 and c1 or b1 and c2. There is some work exploring this in a little
more detail but we're just focusing on the satisfaction of dependency resolution.
So can we avoid the empty hardness of this problem of finding the resolution to satisfy
dependencies? Well go has an approach called minimum version selection where we only specify
the minimum version by infer dependency. So we only describe one version which is the minimum
we can depend upon. And the maximum is implicit up to the next major version. So
it's a linear time traversal of the dependencies in order to find a resolution. You just take
the maximum of all the minimum version byns. This is reliant on strict semantic versioning.
There is no facility to express a maximum other than the next major version bump. So we have to
always have compatible minor and patch versions. Only major versions can break the APIs.
But this isn't suitable to all ecosystems. For example, a camo which is a language
and more familiar with. Any API changes potentially breaking due to module
includes of types. So getting into the technical details. Basically any API change could
be breaking. So there's no meaningful distinction between major and minor versions. And we
devolve into expressing precise dependencies. As in nix's model, we can only depend on a singular
version. So we can't express dependencies on multiple major versions. Make sense? Okay.
So now that I've described the core package calculus, I'm going to try and convince you that this
is expressive enough to model most of the all. I'll say all of the, improve me wrong. I'd
love to be improve me wrong. All the package manager dependency resolution semantics out there.
So the first one is very simple. Version formula. We have Pi which is a version formula such as
greater than 1.2.3 less than 2.0. As I mentioned before, we can basically collapse this to a set
given a repository. We just take all the versions in that repository which is in that formula.
The next one is conflicts. So many package managers support anti dependencies. Let's say I have a
fork of a project which is packaged under a new name. There might be some reasons why that can't
be co-installible with another package. So apps, RPM and Opam also support a conflict from one package
to another package name. So for example, Pi gamma and Vs means P cannot be constable with N where
any V is in Vs. You might think given we have nothing in the core calculus to support this.
This might not be possible to represent, but we can use a trick to encode this in the core calculus.
Oh yeah, basically this is the semantics of the resolution in the conflict calculus where
if we have a conflict on an NVS then we can't have a V existing in the resolution with a V in Vs.
But we can reduce this to the core calculus using these virtual packages. So we create a virtual
package called NVS. So this is for the package N with the set of versions Vs with two versions,
zero or one and the package that is in conflict with NVS depends on this package with version one
and every NVS depends on this package with version zero. And this means we're using the
version uniqueness in order to give conflicts. So if A1 depends upon, sorry, conflicts with B1 of
E2 we can encode it as this in the core calculus. And what this means is package management
ecosystems that don't support conflicts can solve ecosystems that do. The next one is concurrent versions.
So as mentioned in the previous talk, there's this diamond dependency problem in
partition management where you depend on two packages each of which depend upon another with
different versions. No valid resolution for this exists under our version unit is criteria.
But some package managers allow multiple versions of the same name to exist in a resolution.
Cargo allows packages to coexist only when they have different major versions.
NPM allows any different version to coexist. NIX using hash-based paths allows
anything to coexist as well. So we can define a granularity function which maps
versions to a granularity. So for Cargo we take the major version for NPM and NIX we can take
the granularity of the version as the version itself. And for the core calculus we can we can
define your granularity of every version as being the same which is epsilon here. And we define
a concurrent version resolution as instead of version uniqueness. It's the same as the core
calculus but instead of version uniqueness we have version granularity. So for any two packages
that exist in the resolution the versions not being the same implies that their granularity
is also not the same. So if we have two versions of the same major version in Cargo then this would
not apply. But if they are different major versions then this would apply and it would be a valid
resolution. Okay sorry for all the Greek. We can readjust this to the core calculus using
again made up packages. There's a lot of Greek here but let me just give you the intuition. So we have
an example where we have the dumb-independency problem. We have A1 depending on B1 and C1. B1 depends
upon D1, D2 and D2.0.1 and similarly C depends on the two's and three. And under the core calculus
there wouldn't be a valid resolution for this but we can encode this from the extension to the core
using these proxy packages. So the key thing is here we have a proxy package for the C the C
package at version 1.0.0 to package name D and then we have the versions as the granularity function
of its dependencies and then D2 can depend upon D2.0.0 and 2.0.1 as well as the three major
versions. So we use an intermediary in order to be able to depend upon packages with different
major versions. Okay and the point of this, the point of this is any ecosystem which doesn't support
concurrent versions can still interoperate with another ecosystem that does. Okay. Another weird
thing out there is features. These are basically parameterized dependencies. So cargo and
pip support optional functionality of a package being enabled by depending upon it with a
feature in cargo or the called extras in pip. So the one of the key points here is that
the resolver unifies features across the resolution. So if I have package A depending on the package
B with feature alpha and package C depending on package D with feature beta, alpha and beta will be
unified and B will be built with features alpha and beta. Okay. We define a parameterized dependency
where you can depend upon a package with a set of features and we define additional dependencies
that can be enabled by the enablement of a feature. So if we have package P enabled with feature
F we can add an additional dependency. Okay. Okay. Can I get a show of hands are people following
along? Okay good. Now there is a lot of Greek for this one but I'm again going to just give
you the intuition. Okay. The resolution criteria are for features that you depend upon a package
with that package to be provided with those features. Unsurprisingly and if a package is provided
with a feature then you depend upon the additional packages enabled by that feature. So if we have
a package A1 which depends on B1 and C1, B1 depends on D1 with features alpha and beta.
C1 depends on D1 with features beta and D1 if it is dependent upon with alpha depends upon
the additional package E. So to give you this could be a functionality like support for PNG images
for example and if you depend upon this package with the PNG functionality it needs to link in
a library to support PNG images. And then maybe this is JPEG images so you need a JPEG library.
So D1 depends on E1 if it is dependent upon with alpha and F1 if it is dependent upon with beta.
And we can register this to the core calculus again with these intermediate packages.
We create a virtual package for every feature that D1 supports. So we have D1 with feature alpha
and D1 with feature beta. And when you depend upon a package with a feature you include that
as depending upon this virtual package and then that itself depends upon D1 and any additional
packages enabled by that feature. Now if you go into the weeds of the maps you run across some
complexities with different versions of packages with different features just if you want you can go and
look at the slides and dig through the maps and convince yourself that this is right but
basically this encoding supports different versions of packages and different features.
Okay. Now we also have something called peer dependencies in the MPM world.
This is where a child tells its parent what versions of a dependency it can depend upon.
Okay. This is used for plugins so like if I have a if I have a package and I
and I depend upon some JavaScript framework and a plugin for that framework.
That plugin can constrain the versions of the system. Yes. Yes.
So we model the legacy peer dependencies behavior where a peer dependency is only included if
it's parent also depends upon it so when you depend on plugins they don't implicitly
bring in the the framework which it uses but you can also model the new behavior where a plugin
brings in its framework when you depend upon it with some minor tweaks.
So we define theta as this peer dependency model where if we have a package which
peer depends on a M with versions Vs this means package envy has a peer dependency on M with versions Vs
so its parent will need to satisfy the Vs version constraints there.
So we have this parent function pi which maps the package to its parent.
I've admitted for the sake of brevity how that is created but you can you can do this in the
gore calculus. The the the the the criteria is if a package peer depends upon another package
second time poster and the parent of that package also depends upon that peer dependency
then the package used to satisfy this dependency must satisfy the disjunction of the peer dependency
version constraints and the parent dependency version constraints.
Here is an example of how we can register to the core calculus I've admitted the maths here
just giving you the the an example we have A1 which depends upon this framework C and we have a plugin
B1 which depends upon the the the the the framework C with these particular versions and you notice
the only overlap of these two version constraints is C2 we can record this in the core calculus with
these two proxy packages we have this representing the version selection of C2 for this peer dependency
A1 on C and we have A1 pending upon that so other packages can depend upon B as well
which might have different peer dependencies so this is why we need this proxy package and basically
this package here gives us the unification of these two version sets and we can support peer
dependencies in the core calculus. I've got five minutes left right something like that okay I'm going to
I'm going to I'm going to skip past some stuff so we can we can support we can support package formula
so opam and debion allow you to say I depend upon package A or package B or package A
and package B the conjunction is simpler you just depend upon both of them but the
dist junction requires you to introduce a proxy package so we have this hypothetical dependency here
where A1 depends upon a dist junction of two conjunctions and we introduce a proxy package one
is the left one is the right and the version selection basically gives you the dist junction we
either select or the left or the right and the the left depends upon B2 and C1 the right depends
upon B1 and not C1 notice this encoding is the same as the conflict encoding from before
now these formulas can also variables in them sometimes such as the operating system or
like a with test or a with doc we can introduce proxy that we can introduce virtual packages to
represent these variables in the dependency resolution this is different from how it's implemented
in a lot of package manager ecosystem so it's basically a pre-processing step where you filter
the packages that don't match the operating system you're on for example but by putting these
variables in the dependency resolution it can allow us to do things like solve for the particular
operating system we might want to use so I can say I have a I can spin up a debion vm or a
I don't know another vm and I can solve for which operating system might provide the system
dependencies I need there there's also this idea of virtual packages in debion so
two packages can provide something like an SSH server and there is another mechanism for
including this in the package calculus where you create a virtual patch again there's a patch in here
so sometimes there's dependency cycles in packages managers different ecosystems have different ways
of breaking these dependencies um opam has a post variable that says this particular
cyclical can be broken here at I think just arbitrarily breaks at a certain point but the most of the
cycles are in the core of the the core dependencies in debion and I think they are provided
in a bundle so it's not that much of an issue mpm you have cycles everywhere the language breaks
that the package manager doesn't care it just fits the files in the file system there is also
this concept of optional dependencies in opam which took me a while to figure out how we can
represent in the core calculus but it turns like you don't have to um optional dependencies basically
say I use a package if it's present in the resolution but otherwise I don't care it's opam's way
of doing features essentially um it's a little less elegant but we can basically just represent it
in the build order it doesn't affect the resolution semantics as tall
um next has basically no um constraints on versions you depend on a specific package right
and you you get the possibility to depend on different packages by parameterizing derivations in the
next DSL um so the the the actual resolution is either completely turning complete or non-existent
depending on your perspective um so we can represent the the sort of core derivation building part
very simply by just constraining the versions set to be the size of one but this means that next
isn't expressive enough to do the the the the dependency resolution the other ecosystems do
um and this is why you have like all these extra next tools out there um that do versions
solving in the ecosystem specific tooling and then programmatically generate the next renovations
with the bunch of versions pinned um so I'm kind of interested can we can we can we solve dependencies
across ecosystems in a more unified and holistic way um and I I'm thinking my I'm proposing that the
core calculus is basically the minimum you need in order to support all these weird and
wonderful features like that are in the wild and we can create a language as the lingo franca
for these ecosystems so if you want to talk to open from cargo you can go through pack
reduce it down to pack expand it out for the features functionality support and then we can do
cross ecosystem resolution um yeah any questions yeah the implementation is a working
example or something I think I've got a bunch of hacks like they're translating various
ecosystem repositories to open repositories but in doing so I realized it was sort of it was
ad hoc this is an end times I'm a problem right um so I started thinking about what the minimum
commonality you need is I think it's this but the implementation is a working progress
do you want more examples of things that you have an included yes please yeah yeah yeah yeah yeah
yeah if there's something that breaks there's it would be good to know that um so if anyone has
an ideas yeah let me know you can somebody email her yeah so in maven or regular you can
you can have different confide and run time dependencies you have a way to model that in the
core calculus hmm so oh yeah sorry um so the question was in maven you can have different
compile time and run time dependencies do you have a way to model this in the core calculus
and I think the answer to that is basically the uh the versions the variables um we can have
we can have something like a uh is build time variable on dependencies or is run time and then you can
set that variable in the root of parameter test dependency yeah
I'll do some of the ideas we have some more questions okay
um
reason by masking is all expected managers have their own strengths and weaknesses.
Right.
Great.
And I also want some package menus.
The strictness needs is.
I was just curious.
Have you also thought about it?
Yeah.
The potential.
Have you thought about it?
Maybe some of the lessons from one package menu.
Thank you.
People would have the fact.
It has when working with the Opham containers.
It has been a useful way of thinking about things.
Like they do a lot of bulk build testing and they were trying to figure out, you know,
on a new release, what do we need to recalculate in order to figure out what dependencies
we need to rebuild?
And this has been a sort of useful framework for thinking about it.
That's the only other use case of finding for it so far.
But I am thinking about this.
If you have any ideas, let me know.
Yeah.
Feel free to email me or message me any other questions.
Thanks.
Thank you.
OK, thank you.
Thanks you, baby.
Thanks for joining us.