Mathlib with Visual Studio

Stream: new members

[Brandon Sisler]

Hey all, I am having a heck of a time getting mathlib to work in Visual Studio. I have gone over the instructions and everything is coming back correctly except for the step when I run
"which python" to which I am supposed to get "/c/Users/<user>/AppData/Local/Programs/Python/Pythonxx-xx/python" but end up getting /c/Users/<user>/AppData/Local/Programs/Python/Python310/python
I do not know what the issue could be besides this, since everything else seems fine.
Thanks for the help in advance

[Kevin Buzzard]

That looks fine to me! The xx on the website just means "whatever number python is up to now"

[Eric Wieser]

Just to be sure, you're using Visual Studio Code, right? Visual Studio is a different product that likely does not support lean.

[Newell Jensen]

What error are you running into?

[Brandon Sisler]

Yes, as an example, if I try and use data.real.basic from the first tutorial then I get this :

image.png

and cannot use anything included in that package.

[Kevin Buzzard]

Fire up the terminal at the bottom of the screen and type leanproject get-mathlib-cache and see if that fixes it.

[Brandon Sisler]

Eric Wieser said:

Just to be sure, you're using Visual Studio Code, right? Visual Studio is a different product that likely does not support lean.

Yes, if I understand the question right. I can run lean code just fine, just not with the packages in matlib.

[Kevin Buzzard]

It looks like you didn't install the project correctly. The orange bars just mean that Lean is working fine and just compiling mathlib. If you wait for 6 hours or so it should work fine, and the room your computer is in will be nice and hot as well. The command I'm suggesting will download precompiled binaries from the internet which will hopefully solve your problem.

[Kevin Buzzard]

No stop, I take that back. You have got the wrong folder open, that's your mistake.

[Kevin Buzzard]

On the left you can see that there is a visible directory called tutorials. That directory shouldn't be visible -- that should be the directory which you open with VS Code. I don't know for sure but it looks to me like you have got two copies of the tutorials lean project, one inside another one, and right now you have opened one of the projects with VS Code and are trying to use files in the other project; this will not work.

[Kevin Buzzard]

For example I can see two directories called src. This is evidence that you have a pretty borked set-up. If you haven't started doing anything yet then I recommend deleting everything (i.e. both projects) and redownloading the tutorials project, just once, with leanproject get tutorials or whatever it's called. This command will create a new folder called tutorials. Open that folder with VS Code and you'll be fine. Right now you have a corrupted project (or more precisely a project within a project, which is not a setup which is supported)

[Brandon Sisler]

Well shucks, yah I don't have anything I can't just save in a note app, I'll do as you recommend and see if that does it. Thank you
.

[Brandon Sisler]

Hey, that did it, thanks so much!