I don't know how to make VS Code work, I've tried so much

Stream: new members

[Mark Santa Clara Munro]

Hey everyone, I used this link: https://leanprover-community.github.io/install/windows.html , so that I could use Lean, but from the jump it didn't work. I also followed the setup guide on VS Code as much as I could and thought it was maybe because of where I was storing everything or where I was creating the project but I wasn't able to make anything work. I have uninstalled everything and reinstalled it again and it still didn't work. I also tried to change the path variables on my computer to see if it would work.

The following screenshots are the messages/output that are shown most often, and where stuff is within my files:

screenshotlean2.png
screenshotlean3.png
screenshotlean4.png
screenshotlean5.png
screenshotlean1.png

Thank you in advance for the help!!

[Marc Huisinga]

What does the "Troubleshooting: Show Setup Information" command yield?

[Mark Santa Clara Munro]

screenshotlean6.png

[Sebastian Ullrich]

It might be the case that the space in your user name is the problem (though that's a bit confusing as you really shouldn't be the first one with that problem). We're investigating.

[Mark Santa Clara Munro]

Unfortunately I have tested for that, my dad tried with a space and it still worked in his computer.

[Sebastian Ullrich]

A space in his user name?

[Mark Santa Clara Munro]

"You can't do that as it is tied to the Windows user and OneDrive. I created a local account on my PC with your full name and it all installed fine." This is what he just texted me

[Mark Santa Clara Munro]

What I ended up doing is creating a whole new user and doing the process again, which worked!