lake build updating manifest?

Stream: lean4

[James Gallicchio]

I'm not really sure how to reproduce this elsewhere, but in my quest to get LeanColls docs building, I noticed lake build is modifying my std entry when an update is pushed to std... Is this intentional? My impression was that only lake update should touch the manifest.

[James Gallicchio]

Or I guess better question, in what situations should I expect lake build to modify the manifest?

[James Gallicchio]

This is on lake version nightly 09-24

[James Gallicchio]

It also seems like even lake clean clones std and mathlib into lean_packages for some reason. I'm gonna dig into Lake but wondering if someone knows why that is (i.e. why they're treated specially)

[James Gallicchio]

I think this is to do with lake locking transitive dependencies. Seems like a dependency was locked on revision A but lake update was setting it to revision B.

[Thomas Murrills]

in case it helps, I ran into the same problem, and a bit of digging into it was done in this thread!

[James Gallicchio]

Ah, good to know -- there was related discussion in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/doc-gen4.20broken this thread, I think the conclusion was that lake changes your manifest on lake build if a dependency version is locked by some other dependency

[Mac]

I think this is the bug mentioned in lake#119 's comment .