Lake uses a wrong commit

Stream: lean4

[Arthur Paulino]

Hello! I'm not being able to make Lake download the right revision for our YatimaStdLib.lean repo (see PR here)

The lakefile explicits the hash 877d4fe8d42fbef22cd151efabe7e319bf325e6f but Lake is downloading a previous one (35aecd8951778f45a47d12376635c26a815dcb25). Help is much appreciated. Thanks in advance!

[Arthur Paulino]

How come is it memorizing 35aecd8951778f45a47d12376635c26a815dcb25? Is Lake caching something in my computer? I tried to find it and I couldn't find anything. I've already deleted the build and lean_packages folder and it keeps downloading the wrong revision

[Julian Berman]

I can reproduce here FWIW, so whatever it is isn't some local state.

[Arthur Paulino]

Thank you very much for your input Julian! :heart:

[Julian Berman]

Easiest thank you I ever got, I ran 2 commands :) but you're welcome. I don't see anything wrong FWIW, and I want to say I've had to manually mess with lean_packages myself previously IIRC so I'd love to know what's wrong here too.

[Gabriel Ebner]

https://github.com/leanprover/lake/issues/85

[Julian Berman]

That's not this is it? This happens even after blowing away the lean_packages folder.

[Gabriel Ebner]

Maybe it uses the revision from the ipld lakefile. See also https://github.com/leanprover/lake/issues/70

[Arthur Paulino]

Oh my, that must be precisely it!

[Julian Berman]

Probably the "real" "real" fix is Lake having a dependency solver, which I assume is a decent chunk of effort.

[Julian Berman]

And then blowing up for impossible / incompatible dependencies?

[Henrik Böving]

Julian Berman said:

Probably the "real" "real" fix is Lake having a dependency solver, which I assume is a decent chunk of effort.

Dependency solving as a SAT tactic! :P

[Arthur Paulino]

A low-hanging fruit might be a simple warning that a dependency uses a different version than the one that is required by the lib