issue about mathlib install

Stream: new members

[Wilber Du]

I am trying to install the mathlib but I got this error message:

Cannot initialize project. Command output: info: downloading mathlib `lean-toolchain` file info: mathlib: no previous manifest, creating one from scratch info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4 info: leanprover-community/mathlib: checking out revision 'a79df06b3d23fb6a3c42fb65a949009dc241862d' info: toolchain not updated; already up-to-date error: dependency cycle detected: mathlib mathlib

[Emily Riehl]

This is for my class and I'm confused about the error message dependency cycle detected: mathlib mathlib. Everyone just installed VSCode and Lean and we're trying to create our first project using mathlib. Is this the right channel for installation help? I can't remember.

[Mac Malone]

This is quite odd. What does the lakefile.lean / lakefile.toml look like for this project?

One possible way I could see this happening is if the project was given the name mathlib and then required mathlib. For example:

lakefile.toml

name = "mathlib"

[[require]]
name = "mathlib"
scope = "leanprover-community"

[Emily Riehl]

Thanks. I think that was the issue.

[Emily Riehl]

Now we've got everyone set up! Phew :sweat_smile:

[Wilber Du]

Thank you so much! Everything works well now