Mathlib dependency fails to build?

Stream: lean4

[James Gallicchio]

It seems like every time I lake update and bump my toolchain, some parts of Mathlib fail to update. I just did a bump to 09-11, and it errors trying to build Mathlib/Data/Option/Basic.lean:

error: > LEAN_PATH=./lean_packages/Cli/build/lib:./lean_packages/leanInk/build/lib:./lean_packages/doc-gen4/build/lib:./lean_packages/Unicode/build/lib:./lean_packages/mathlib/build/lib:./build/lib:./lean_packages/std/build/lib:./lean_packages/lake/build/lib:./lean_packages/CMark/build/lib LD_LIBRARY_PATH=/home/james/.elan/toolchains/leanprover--lean4---nightly-2022-09-11/lib:./lean_packages/mathlib/build/lib /home/james/.elan/toolchains/leanprover--lean4---nightly-2022-09-11/bin/lean ./lean_packages/mathlib/././Mathlib/Data/Option/Basic.lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/build/lib/Mathlib/Data/Option/Basic.olean -i ./lean_packages/mathlib/build/lib/Mathlib/Data/Option/Basic.ilean -c ./lean_packages/mathlib/build/ir/Mathlib/Data/Option/Basic.c
error: stdout:
./lean_packages/mathlib/././Mathlib/Data/Option/Basic.lean:6:0: error: import failed, environment already contains 'Option.elim._cstage2'

Am I doing something wrong in the process of updating? It looks like it's building fine on the mathlib github...

[Scott Morrison]

Maybe you could post your lakefile? Have you tried lake clean? I've experienced transient errors on upgrading that it seems lake clean resolved.

[James Gallicchio]

lake clean and even deleting the lean_packages folders doesn't seem to resolve it... the repo is up to date: https://github.com/JamesGallicchio/LeanColls
lakefile: https://github.com/JamesGallicchio/LeanColls/blob/main/lakefile.lean
manifest.json: https://github.com/JamesGallicchio/LeanColls/blob/main/lean_packages/manifest.json

[James Gallicchio]

I haven't spent much time investigating, just was hoping someone else had experienced this :thinking:

[Gabriel Ebner]

This usually means you have the wrong Lean version.

cp lean_packages/mathlib/lean-toolchain .

[Mauricio Collares]

@Arthur Paulino once mentioned lake update can help with these sorts of issues too

[Arthur Paulino]

Having so many dependencies is a bit terrifying in my experience. You also have to check the entire chain of dependencies of their dependencies and make sure it's all coherent and consistent

[Arthur Paulino]

An issue I faced once was that I had dependencies A and B, but A also depended on an older version of B. And Lake downloaded the older version of B to satisfy A but then my own project ended up depending on an incompatible version of B

[Gabriel Ebner]

That bug has been fixed now.

[James Gallicchio]

Gabriel Ebner said:

This usually means you have the wrong Lean version.

cp lean_packages/mathlib/lean-toolchain .

They are identical... :/

[James Gallicchio]

I have also run lake update, which is how I got to my current manifest

[Sebastian Ullrich]

Does it work if you first delete lean_packages/mathlib/build?

[James Gallicchio]

Deleting everything in lean_packages (minus the manifest.json) does not resolve anything. I'm gonna investigate where the errors are actually coming from, see if I can figure out where the version mismatch is

[Sebastian Ullrich]

Ah... I missed that

[James Gallicchio]

Regardless, this situation seems not ideal :joy: Maybe I am updating my dependencies way more frequently than everyone else but this has been a recurring issue. Does lake check that all dependencies' toolchains match the current project's?

[James Gallicchio]

Oh, I never updated this thread -- I must have been lake updateing during a period when std4 and mathlib4 were out of sync, and lake evidently doesn't check that toolchains match

[James Gallicchio]

(std4 was already updated to 09-15; mathlib and my lib were on 09-11. lake downloaded the most recent packages for everything)

[James Gallicchio]

This is definitely made worse by being on nightly, maybe it'll be less bad when development calms down a bit, but is there any improvement that could be made here?

My ideal would be for lake to poll which toolchain versions the various dependencies have releases for, compute the highest version that everything has a release for, and then update the local project + all dependencies to be on that toolchain version. Not sure how possible that is, though

[James Gallicchio]

Actually, that isn't even really good enough -- just also had to manually fix my manifest because mathlib relied on a different version of std4 than what lake update pulled (because mathlib was behind)

Don't know if I have suggestions for how to improve this. :/

[James Gallicchio]

I assume it's not okay for a project to depend on multiple versions of the same library, since namespaces would conflict

[Gabriel Ebner]

That bug has been fixed now.

Apparently not entirely: see https://github.com/leanprover/lake/issues/119 (And then there was always the issue that it didn't pick up updates if the branch changed, but that's not the case here.)

[James Gallicchio]

Ahh, I missed that ticket, that makes sense