Installation issues

Stream: LFTCM 2024

[Harald Helfgott]

I've installed Lean on my new laptop, and opened Test.lean, but I'm not getting any blue squiggles (or any squiggles of any other color, for that matter). What is not working?

[Jireh Loreaux]

Did you install the lean4 extension on VS Code? Also, you probably want to open the folder not the file.

[Harald Helfgott]

I did install the lean4 extension. Oh. I clicked on the icon (showing two pages) in the upper left corner, and now the blue squiggle is where it should be! Thanks!

[Anatole Dedecker]

In any case we should have some time to fix any installation issues, so don't worry.

[Kevin Buzzard]

This conversation is happening in the wrong thread

[Anatole Dedecker]

(Please tell me if I did the move wrong, it's the first time I've done that I think :sweat_smile:)

[Riccardo Brasca]

It's fine, thanks!

[JB Stiegler]

hello, i have an issue with lake. I guess it's related to my strange linux distribution (Mageia), it's a permission error. Could somebody help me ? I'm in the amphitheater

[JB Stiegler]

alright problem fixed, the problem was sitting in front of the keyboard