Lean won't stop loading

Stream: new members

[Christian Kolker]

So I recently installed VScode and downloaded the Lean tutorial projects. However, every time I clicked in on something in the projects It will never stop loading. I think it is a problem with the path, but I am not sure exactly what is wrong?

[Martin C. Martin]

What commands did you use to download? You often need to download the compiled files separately from the .lean files.

[Martin C. Martin]

If you use leanproject to download them, instead of git directly, it downloads both.

[Martin C. Martin]

What exactly happens in VS Code? Is there an animated icon or a message or something?

[Christian Kolker]

In VS Code, I can open the tutorial projects and have access to them, but it just continuously loads every single line. The message just says loading

[Christian Kolker]

I used "leanproject get tutorials" in git bash for my command to download it all

[Kevin Buzzard]

That's the correct way to download the tutorial; did the command give you any errors? And did you open the root directory of the project folder with VS Code's "open folder" functionality (as opposed to just opening a random file in the tutorial, which will not work)?

[Kevin Buzzard]

That's the correct way to download the tutorial; did the command give you any errors? And did you open the root directory of the project folder with VS Code's "open folder" functionality (as opposed to just opening a random file in the tutorial, which will not work)?

[Patrick Massot]

Kevin, aren't you supposed to be out there cheering on your queen?

[Kevin Buzzard]

oh lol maybe. I'm actually in France ;-) (or possibly Switzerland)

[Martin C. Martin]

70 years is an impressively long reign.

[Julian Berman]

Kevin's probably more focused on when she gets to 37 * 2. I guess that will be her platinum jubilean.

[Christian Kolker]

I ended up fixing it by re-downloading the tutorials and setting up the path correctly
Thank you for responding though