Zulip Chat Archive

Stream: new members

Topic: Question about VS Code


view this post on Zulip 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?

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:24):

How did you install Lean?

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:25):

Also welcome!

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:25):

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

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:25):

I checked, lean is installed on my machine

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:26):

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

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:27):

thats not comming up

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:27):

hmm

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:30):

okay i installed elan

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:30):

hmm that command you pasted should have installed elan

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:30):

yes it did

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:31):

ok coolio

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:31):

so now the infoview is coming up in VS Code

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:32):

ok have you opened the tutorial project folder in vscode?

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:32):

yes

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:33):

ok and you got that by running leanproject get tutorials?

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:34):

yes thats how i downloaded it

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:34):

nice

view this post on Zulip 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?

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:36):

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

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:36):

let me see

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:37):

yes

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:37):

Nice I think it's working then

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:37):

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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:38):

Ah I see

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:38):

you can compile by typing leanpkg build in the project folder

view this post on Zulip 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

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:39):

that clears things up, thank you!

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:39):

np!

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:41):

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

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:41):

do I need the extensions that help with those files?

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:42):

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

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:42):

hmm

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:42):

Does the error look like this: image.png

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:44):

no, I managed to debug that one earlier

view this post on Zulip 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!

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:46):

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

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:47):

eg code tutorials

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:48):

yes I was opening VS code then opening the folder tutorials

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:53):

Ah I see

view this post on Zulip 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.

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:54):

ah i see

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:55):

cool!

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:55):

I appreciate the help, thank you!

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:56):

No problem! Happy Leaning!

view this post on Zulip Brian Becsi (Oct 03 2020 at 18:56):

it compiled!

view this post on Zulip Edward Ayers (Oct 03 2020 at 18:56):

woop!

view this post on Zulip 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: May 08 2021 at 04:14 UTC