Zulip Chat Archive

Stream: new members

Topic: Question about VS Code

Brian Becsi (Oct 03 2020 at 18:24):

Hello, my name is Brian and I'm a new member. I have a question about Visual Studio Code.

I am on Linux, and have Lean and VS Code installed as well as the extension for Lean. I have downloaded the tutorial and opened it, but when I want to run something, VS Code seems to ask me for an environment. I don't see any "lean" environment.

What is going on?

Edward Ayers (Oct 03 2020 at 18:24):

How did you install Lean?

Edward Ayers (Oct 03 2020 at 18:25):

Also welcome!

Brian Becsi (Oct 03 2020 at 18:25):

I used the easy method and just copy pasted the sudo install command.

Brian Becsi (Oct 03 2020 at 18:25):

I checked, lean is installed on my machine

Edward Ayers (Oct 03 2020 at 18:26):

if you type elan in to the command line what does it say?

Brian Becsi (Oct 03 2020 at 18:27):

thats not comming up

Edward Ayers (Oct 03 2020 at 18:27):

hmm

Edward Ayers (Oct 03 2020 at 18:28):

Was this the thing you copied to install: curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh

Brian Becsi (Oct 03 2020 at 18:29):

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

Brian Becsi (Oct 03 2020 at 18:30):

okay i installed elan

Edward Ayers (Oct 03 2020 at 18:30):

hmm that command you pasted should have installed elan

Brian Becsi (Oct 03 2020 at 18:30):

yes it did

Edward Ayers (Oct 03 2020 at 18:31):

ok coolio

Brian Becsi (Oct 03 2020 at 18:31):

so now the infoview is coming up in VS Code

Edward Ayers (Oct 03 2020 at 18:32):

ok have you opened the tutorial project folder in vscode?

Brian Becsi (Oct 03 2020 at 18:32):

yes

Edward Ayers (Oct 03 2020 at 18:33):

ok and you got that by running leanproject get tutorials?

Brian Becsi (Oct 03 2020 at 18:34):

yes thats how i downloaded it

Edward Ayers (Oct 03 2020 at 18:34):

nice

Edward Ayers (Oct 03 2020 at 18:35):

ok so what do you see when you open src/exercises/00_first_proofs.lean in vscode?

Edward Ayers (Oct 03 2020 at 18:36):

eg do you see a squiggly line under #check upper_bounds?

Brian Becsi (Oct 03 2020 at 18:36):

let me see

Brian Becsi (Oct 03 2020 at 18:37):

yes

Edward Ayers (Oct 03 2020 at 18:37):

Nice I think it's working then

Edward Ayers (Oct 03 2020 at 18:37):

I'm not sure where this environment notification is coming fro

Brian Becsi (Oct 03 2020 at 18:38):

heh I was trying to compile, I'm very new to coding and I'm coming from PyCharm

Edward Ayers (Oct 03 2020 at 18:38):

Ah I see

Edward Ayers (Oct 03 2020 at 18:38):

you can compile by typing leanpkg build in the project folder

Edward Ayers (Oct 03 2020 at 18:39):

but the idea is that the environment is interactive, so it's continuously compiling when you make edits

Brian Becsi (Oct 03 2020 at 18:39):

that clears things up, thank you!

Edward Ayers (Oct 03 2020 at 18:39):

np!

Brian Becsi (Oct 03 2020 at 18:41):

okay so now i'm getting failed to open file leanpkg.toml

Brian Becsi (Oct 03 2020 at 18:41):

do I need the extensions that help with those files?

Edward Ayers (Oct 03 2020 at 18:42):

no that is just a little config file for a lean project

Brian Becsi (Oct 03 2020 at 18:42):

hmm

Edward Ayers (Oct 03 2020 at 18:42):

Does the error look like this: image.png

Brian Becsi (Oct 03 2020 at 18:44):

no, I managed to debug that one earlier

Brian Becsi (Oct 03 2020 at 18:46):

Okay, so I think I see how it's compiling, I'm just getting used to this editor. Thank you so much Edward!

Edward Ayers (Oct 03 2020 at 18:46):

ok so can you just make sure that you have opened vscode in the right folder?

Edward Ayers (Oct 03 2020 at 18:47):

eg code tutorials

Brian Becsi (Oct 03 2020 at 18:48):

yes I was opening VS code then opening the folder tutorials

Edward Ayers (Oct 03 2020 at 18:48):

Brian Becsi said:

okay so now i'm getting failed to open file leanpkg.toml

Was this in the command line? If I run leanpkg build in a folder without a leanpkg.toml then I get an error failed to open file 'leanpkg.toml' , so you have to make sure that you run it in the root directory of the project

Brian Becsi (Oct 03 2020 at 18:53):

so I right clicked 00_first_proofs.lean, clicked "open in integrated terminal" then typed leanpkg build

Edward Ayers (Oct 03 2020 at 18:53):

Ah I see

Edward Ayers (Oct 03 2020 at 18:54):

Yeah when you click that it opens the terminal in the subfolder and then leanpkg complains because it can't find the leanpkg file.

Brian Becsi (Oct 03 2020 at 18:54):

ah i see

Edward Ayers (Oct 03 2020 at 18:55):

cool!

Brian Becsi (Oct 03 2020 at 18:55):

I appreciate the help, thank you!

Edward Ayers (Oct 03 2020 at 18:56):

No problem! Happy Leaning!

Brian Becsi (Oct 03 2020 at 18:56):

it compiled!

Edward Ayers (Oct 03 2020 at 18:56):

woop!

Patrick Massot (Oct 03 2020 at 20:43):

Brian, it seems you haven't yet a clear picture of what interacting with Lean is meant to look like. I recommend watching https://www.youtube.com/watch?v=b59fpAJ8Mfs

Last updated: Dec 20 2023 at 11:08 UTC