how does lake resolve/deduplicate transitive dependencies?

Stream: lean4

[David Renshaw]

Imagine three projects, named A, B, and C.

• Project A requires std at revision abcd1234.
• Project B requires std at revision efef5656.
• Project C requires both project A and project B.

How does lake decide which version of std to use for project C? Does it change anything if project A requires std at a tag named something like v4.6.0, rather than a commit ID?

[David Renshaw]

I did some experimentation, and it looks like the answer is: it depends on which order the require statements appear in projects C's lakefile.

[David Renshaw]

It seems that earlier requirements win. (And that maybe git requires are prioritized over local path requires?)

[Ruben Van de Velde]

I think the current suggestion is "try not to get yourself in that situation", which isn't great but might well improve as the ecosystem matures

[Mac Malone]

David Renshaw said:

I did some experimentation, and it looks like the answer is: it depends on which order the require statements appear in projects C's lakefile.

David Renshaw said:

It seems that earlier requirements win.

This is correct assessment of how Lake works (except for the git > path -- they should both be treated the same). As Lake has no semantic version information at present, it cannot do more intelligent resolving at this time.

[Eric Wieser]

Can running lake update a or b change the version resolved?