How does lake handle transitive dependencies?

Stream: general

[Li Xuanji]

Is the dependency resolution algorithm of lake update specified anywhere? I'd like to know how it handles transitive dependencies, e.g. package A depends on package B at version 1 and package C, and package C depends on package B at version 2. From digging around the CLI output and the .lake file, my understanding is that lake update must choose one version of package B to install, either version 1 or version 2.

(If so, one common solution adopted by other package managers is to choose the more recent version, but I noticed when reading the docs for how versions are specified that git dependencies are specified by "rev" which is a git commit hash or a git tag (and maybe some other options? It's not documented), but neither are linearly ordered in general. Reservoir dependencies are specified by version which is more promising, but the version format is also not documented)

(Another question is that in situations like this, packages ought to be able to declare range dependencies, e.g. this package is compatible with mathlib v4.5-v4.10, e.g. like so in python, but I couldn't find the syntax for range dependencies in the docs)

(For context, I was debugging a situation where B=mathlib, C=LeanTeX-Mathlib)

[Ruben Van de Velde]

This is not supported as far as I'm aware

[Kim Morrison]

From memory it is just a depth-first search. Lake looks at the first dependency, and pulls in all its dependencies, then moves on, ignoring repeats even if the rev field differs. Obviously this is not not good enough, and Mac is working on it! :-)

[Li Xuanji]

Lake looks at the first dependency, and pulls in all its dependencies, then moves on, ignoring repeats even if the rev field differs.

Thanks! Is this true even if all the dependencies are reservoir dependencies?

[Mac Malone]

To elaborate a bit, Lake does not exactly use a depth-first search. It resolves all dependencies of the same package at once then does progresses depth-first. That is, the dependencies of the top-level package take precedence over any nested dependencies. This is explained in a comment in the code.

This is not documented more publicly because this is expected to change (as Kim said), and we would prefer users avoid relying on a particular ordering at this time.

[Li Xuanji]

Thanks! That's a helpful comment.

Understood about not exposing this implementation detail, but perhaps the following could be documented, since these sound like they will be around forever?

1. lake will choose exactly one version for each dependency in the transitive closure of the dependency graph (i.e. it won't do something like npm where version 1 and version 2 can coexist in the resolved dependency tree)
2. If you want to "override" a dependency's transitive dependency, include it in your own lakefile.toml

[Kim Morrison]

I agree it would be great to have this documented, but it's certainly not the plan for this to be around forever.

[Alok Singh]

Well in 'worse is better', my documentation on this for an AI agent is just linking this zulip issue.

[Li Xuanji]

not the plan for this to be around forever.

Oh? I was under the impression that the "npm strategy" isn't feasible for dependently-typed languages if you're writing proofs.