Stream: new members

Topic: customizing vscode

Dima Pasechnik (Jul 03 2020 at 10:24):

I am trying to go through the tutorial with vscode (aka code) interface, and run into few gltches.

1) I get a message saying "You are running lean in a directory without leanpg.toml file. This is not supported" - this is despite starting code as code src/excercises& from turorials/  - and leanpg.toml is present there. Does it complain about absense of leanpg.toml somewhere else? Is it harmless? (it is strange that one toml file per project is not enough.)

2) there is an "overview column" with impossibly small font showing 00_first_proofs.leannext to the main 00_first_proofs.lean vertical split, and this column covers parts of the text, no matter what I do. Can it be turned off?

(Disclaimer: I never liked "modern" IDEs, and my main text editor is vim)

Rob Lewis (Jul 03 2020 at 10:29):

1) leanpkg.toml is in tutorials/, so you should start VSCode with code .
2) I'm not sure exactly what you're talking about, is it the minimap? There's an option to turn it off somewhere in one of the view menus. I agree it's annoying and wish VSCode didn't turn it on by default.

Dima Pasechnik (Jul 03 2020 at 11:00):

Rob Lewis said:

1) leanpkg.toml is in tutorials/, so you should start VSCode with code .

I tried this. This gives me just a welcome to vscode screen. If I open the directory tutorials/src/exercises I get the same message. Same if I invoke code . in tutorials/src/ (the latter seems to be the correct place, as from there at least I can open exercises/ without going to Files menu. A bug (of sorts)?

2) I'm not sure exactly what you're talking about, is it the minimap? There's an option to turn it off somewhere in one of the view menus. I agree it's annoying and wish VSCode didn't turn it on by default

yes, that was minimap, indeed, thanks!

Rob Lewis (Jul 03 2020 at 11:02):

There's a navigation menu on the left, open by default I think, but if not the documents icon above the search icon. Open . and then navigate to whichever files you want to open.

Kevin Kappelmann (Jul 03 2020 at 11:07):

Dima Pasechnik said:

...
(Disclaimer: I never liked "modern" IDEs, and my main text editor is vim)

I use VSCodeVim and it works quite well for me.

Dima Pasechnik (Jul 03 2020 at 11:07):

What does "editor" mean in VSCodish? An editor window?

Dima Pasechnik (Jul 03 2020 at 11:17):

Yes it was a bug, it seems: I appended the line

path ./src/exercises


to leanpkg.path and the warning went away. The latter file is not under revision control, however, so I don't know where to go to file a report.

Bryan Gin-ge Chen (Jul 03 2020 at 11:19):

I tried this. This gives me just a welcome to vscode screen. If I open the directory tutorials/src/exercises I get the same message. Same if I invoke code . in tutorials/src/ (the latter seems to be the correct place, as from there at least I can open exercises/ without going to Files menu. A bug (of sorts)?

It seems you're still launching VS Code from the wrong directory somehow. You need to either run code . from the root directory of the Lean project, the one containing leanpkg.toml (in this case tutorials/), or you can open VS Code, hit "open..." from the File menu, and then open the tutorials/ directory.

Dima Pasechnik (Jul 03 2020 at 11:22):

Bryan Gin-ge Chen said:

I tried this. This gives me just a welcome to vscode screen. If I open the directory tutorials/src/exercises I get the same message. Same if I invoke code . in tutorials/src/ (the latter seems to be the correct place, as from there at least I can open exercises/ without going to Files menu. A bug (of sorts)?

It seems you're still launching VS Code from the wrong directory somehow. You need to either run code . from the root directory of the Lean project, the one containing leanpkg.toml (in this case tutorials/), or you can open VS Code, hit "open..." from the File menu, and then open the tutorials/ directory.

I tried them all, but until I modified leanpkg.path the warning persisted.

Mario Carneiro (Jul 03 2020 at 11:23):

the modification looks really suspicious. What error are you getting?

Dima Pasechnik (Jul 03 2020 at 11:24):

I don't get errors, I was getting a warning.

Mario Carneiro (Jul 03 2020 at 11:24):

Does the "explorer" tab show the contents of the tutorials/ directory? With leanpkg.toml at the root?

I have

$cat leanpkg.path builtin_path path _target/deps/mathlib/src path ./src/solutions path ./src/exercises # <- Added by me  Dima Pasechnik (Jul 03 2020 at 11:25): Mario Carneiro said: Does the "explorer" tab show the contents of the tutorials/ directory? With leanpkg.toml at the root? yes it does Mario Carneiro (Jul 03 2020 at 11:27): Then, in the tutorials/src folder, create a copy of the exercises folder for you work. This way it won't be overwritten if you update the project to get new exercices. You can then open the tutorials folder in VS code. The first file 00_first_proofs.lean does not contain any exercise, it is meant as an overview of the basics. You can skip it if you are really eager to start coding, but this is not recommended. You don't need to understand everything while reading this file, only try to get a feel for what it's looking like, and maybe start picking up some key words. Mario Carneiro (Jul 03 2020 at 11:27): from the readme Mario Carneiro (Jul 03 2020 at 11:28): You are apparently supposed to copy the contents of the src/exercises folder to src/, not source it directly Dima Pasechnik (Jul 03 2020 at 11:33): Mario Carneiro said: You are apparently supposed to copy the contents of the src/exercises folder to src/, not source it directly here is what it says: Then, in the src folder, create a copy of the exercises folder for you work.  I.e., make a copy of the folder. It does not mean copying files one by one. Neeedless to say, I did cp -a exersices myexercises, and tried in myexcercises, getting the same warning. Then I tried inexcercises, getting the same warning... Bryan Gin-ge Chen (Jul 03 2020 at 11:35): This is very strange. I couldn't reproduce the warning at all. I'm not sure what we're doing differently. Here's the full list of steps I took: 1) Run leanproject get tutorials in the terminal. This cloned the tutorials repo into a subdirectory tutorials/ and then downloaded the olean files for appropriate version of mathlib. 2) code tutorials/. This opened VS Code in the tutorials/ directory. I didn't see any warning and the explorer tab on the left showed the root of tutorials/. 3) I opened src/exercises/00_first_proofs.lean from the explorer tab. This opened an editor window in the middle column and an info view window at the right (with title "Lean goal"). After the orange bars disappeared (in a few seconds), the file behaved as I expected. No warning popped up. Mario Carneiro (Jul 03 2020 at 11:35): The project seems to be set up in an unusual way. The root directory is set to src/solutions, which means that you can import tuto_lib for example but not import your own exercise files Mario Carneiro (Jul 03 2020 at 11:35): but that should be fine for the tutorial Dima Pasechnik (Jul 03 2020 at 11:39): Bryan Gin-ge Chen said: This is very strange. I couldn't reproduce the warning at all. I'm not sure what we're doing differently. Here's the full list of steps I took: 1) Run leanproject get tutorials in the terminal. This cloned the tutorials repo into a subdirectory tutorials/ and then downloaded the olean files for appropriate version of mathlib. 2) code tutorials/. This opened VS Code in the tutorials/ directory. I didn't see any warning and the explorer tab on the left showed the root of tutorials/. 3) I opened src/exercises/00_first_proofs.lean from the explorer tab. This opened an editor window in the middle column and an info view window at the right (with title "Lean goal"). After the orange bars disappeared (in a few seconds), the file behaved as I expected. No warning popped up. yes, that's what I did. Any notifications on the "bell" button in the bottom right corner for you? Mario Carneiro (Jul 03 2020 at 11:39): I've never touched that icon ever Dima Pasechnik (Jul 03 2020 at 11:40): Mario Carneiro said: I've never touched that icon ever perhaps the warning is there, it just did not pop up? Mario Carneiro (Jul 03 2020 at 11:43): I just followed Bryan's instructions and got the same result Mario Carneiro (Jul 03 2020 at 11:43): 0 notifications Dima Pasechnik (Jul 03 2020 at 11:48): Strange. Is there a caching of some sort taking place between the sessions of Lean? Cause after removing that line I added in leanpkg.path I can't reproduce it either. Dima Pasechnik (Jul 03 2020 at 11:54): I am able to reproduce the warning: quite code, make a copy of excersises directory, say $ cd tutorials/src/
\$ cp -a exercises/ tst/


start code, and open a file in tutorials/src/tst.  You should see the warning


tutos.gif

Patrick Massot (Jul 03 2020 at 11:55):

This is what is meant by the instructions.

Patrick Massot (Jul 03 2020 at 11:55):

We can easily add a shell code block to the readme, but then describing clicks is always harder.

Mario Carneiro (Jul 03 2020 at 11:56):

when you say "start code" @Dima Pasechnik , how did you start it?

Patrick Massot (Jul 03 2020 at 11:57):

Oh, the screencast doesn't show the mouse, that's a bit annoying.

Dima Pasechnik (Jul 03 2020 at 11:57):

Patrick Massot said:

This is what is meant by the instructions.

Will you get a warning if instead of my_excercises you used some other, new, name? Cause this is what happens to me.

Mario Carneiro (Jul 03 2020 at 11:58):

my_exercises is not baked anywhere

Mario Carneiro (Jul 03 2020 at 11:59):

but the main reason you get the "no toml" warning is because you didn't open code to the root of the project, in this case the tutorials/ directory

Patrick Massot (Jul 03 2020 at 11:59):

I should also add that hopefully MIL is very close to being able to fully replace that tutorial. There will always be a style difference of course, MIL is much more verbose, so maybe we'll keep them both, but we may have to update the learning resource page to discuss this is those terms.

Mario Carneiro (Jul 03 2020 at 12:00):

Is there a tutorial/template project with a more typical setup?

Patrick Massot (Jul 03 2020 at 12:01):

@Gabriel Ebner would it make sense for the VSCode extension to try to override people's opinion here? It already tests whether there is a leanpkg.toml in the correct place, what about searching for it in parents folder and reopening the correct folder, maybe after asking for confirmation? The good point is that many people fail to understand this and it would work anyway. The bad point is it would encourage people in having the wrong idea.

Mario Carneiro (Jul 03 2020 at 12:02):

I realize that tutorial projects have their own design constraints because of having to put solutions and exercises somewhere, but when a user starts a new project it won't have this kind of toml file

Patrick Massot (Jul 03 2020 at 12:02):

But maybe if the warning/confirmation dialog is good enough we could mitigate this bad point.

Patrick Massot (Jul 03 2020 at 12:03):

Mario, the template is what leanproject new will create for you.

Patrick Massot (Jul 03 2020 at 12:03):

And indeed the tutorials project has a very unusual setup, for the reasons you describe, and MIL is even worse from this point of view.

Gabriel Ebner (Jul 03 2020 at 12:11):

Patrick Massot said:

Gabriel Ebner would it make sense for the VSCode extension to try to override people's opinion here? It already tests whether there is a leanpkg.toml in the correct place, what about searching for it in parents folder and reopening the correct folder, maybe after asking for confirmation? The good point is that many people fail to understand this and it would work anyway. The bad point is it would encourage people in having the wrong idea.

Is this what you propose?

1. User opens tutorials/src in vscode.
2. Extension sees no leanpkg.toml file, but finds one at ../leanpkg.toml.
3. Shows error message with button to switch folder to tutorials.

Yes

Mario Carneiro (Jul 03 2020 at 12:14):

that should be a warning, yes?

Patrick Massot (Jul 03 2020 at 12:14):

Yes, gentle warning offering help.

Dima Pasechnik (Jul 03 2020 at 12:15):

Mario Carneiro said:

but the main reason you get the "no toml" warning is because you didn't open code to the root of the project, in this case the tutorials/ directory

Why doesleanpkg.path contain relative paths, and not absolute ones? IMHO it seems it could be asking for problems this way...

Mario Carneiro (Jul 03 2020 at 12:19):

because the leanpkg.path file defines the root

Mario Carneiro (Jul 03 2020 at 12:19):

everything is relative to that file

Gabriel Ebner (Jul 03 2020 at 12:28):

Mario Carneiro said:

that should be a warning, yes?

A modal error message it is. leanprover/vscode-lean#201
gentle_help.png

Patrick Massot (Jul 03 2020 at 12:34):

Maybe add the traditional "unless you are sure you know what you are doing"? Maybe not actually, we've seen many people being sure and wrong.

Gabriel Ebner (Jul 03 2020 at 12:35):

You can still click cancel.

Mario Carneiro (Jul 03 2020 at 12:43):

What happens if the folder cannot be located?

Gabriel Ebner (Jul 03 2020 at 12:43):

Then nothing changes compared to now.

Gabriel Ebner (Jul 03 2020 at 12:44):

That is, you get a small warning on the bottom right.

Bryan Gin-ge Chen (Jul 03 2020 at 14:12):

Just a heads up, I think we tried to fix this before, but I think I still see the leanpkg.toml warning pop up when opening markdown files in other non-lean projects.

Gabriel Ebner (Jul 03 2020 at 14:14):

Yes, we check if there are any *.lean files and then we skip the error message. Please file an issue if you can reproduce it again.

Dima Pasechnik (Jul 03 2020 at 16:07):

I can't be certain about what "open the directory" means, and judging by the different advices I got here from different people, I am not alone in being confused here. One (correct) way to read it is to open code from terminal with the directory given as the argument.

But cd to the directory followed by code . does not work (afk now, so this is from memory).

Again, I don't spend a lot of time with IDEs, and perhaps in the IDE world there is no confusion here.

Jalex Stark (Jul 03 2020 at 16:16):

maybe you'd prefer using the emacs plugin

Jalex Stark (Jul 03 2020 at 16:18):

in VSCode, when I press ctrl+o, it opens up a little GUI for me to click through my directories and find a file to open

Jalex Stark (Jul 03 2020 at 16:18):

and I click on the root directory of a project

Jalex Stark (Jul 03 2020 at 16:20):

if it's a project i'm opening in VSCode for the first time, I get a useless "Welcome" tab

Jalex Stark (Jul 03 2020 at 16:21):

and I get a sidebar called "explorer" that contains a collapsible filetree of my project

Jalex Stark (Jul 03 2020 at 16:22):

if I use that sidebar to navigate to a lean file, it opens and automatically spawns a a window for lean messages to come out of

Jalex Stark (Jul 03 2020 at 16:22):

i would not be surprised if VSCode is agnostic about the directory it's run from

Patrick Massot (Jul 03 2020 at 16:41):

Dima Pasechnik said:

I can't be certain about what "open the directory" means, and judging by the different advices I got here from different people, I am not alone in being confused here.

It seems these differences come from people having different guesses about what you did wrong.

Dima Pasechnik (Jul 03 2020 at 17:34):

I think "directory x" actually means "project located/rooted in directory x". At least that how such things in IDE world I knew were called: "projects".

Anatole Dedecker (Jul 03 2020 at 18:00):

Visual Studio is quite different from Visual Studio Code

Anatole Dedecker (Jul 03 2020 at 18:03):

What I do is : in the terminal, go to the project folder, which, if you initiated your project with leanproject, contains src/, .gitignore, _target/ and most importantly leanpkg.path. Then I just type code . and everything works fine

Kevin Buzzard (Jul 03 2020 at 19:30):

I just use the "open folder" functionality of VS Code and open the folder containing the project

Anatole Dedecker (Jul 03 2020 at 19:34):

That works too, I'm just used to the command line

Dima Pasechnik (Jul 03 2020 at 20:45):

Gabriel Ebner said:

Mario Carneiro said:

that should be a warning, yes?

A modal error message it is. leanprover/vscode-lean#201
gentle_help.png

I get a different message, without "(which is <....>/tutorials) and without "Switch to correct folder" button.
The "(which is ...)" part is replaced by "More details inside" clickable text, clicking on which brings up
a pop-up sayng

Do you want Code to open external website
https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

with buttons "Configure trusted domains", "Cancel", "Copy", "Open".

And this is confising, isn't it?

Bryan Gin-ge Chen (Jul 03 2020 at 20:48):

The PR to the extension with the new help message has been merged, but not released. (The release is waiting on me to update the README, and this is in progress but not done.)

Dima Pasechnik (Jul 03 2020 at 20:49):

Anatole Dedecker said:

Visual Studio is quite different from Visual Studio Code

I haven't used Visual Studio since 2001 or so :-)

Dima Pasechnik (Jul 03 2020 at 20:54):

Bryan Gin-ge Chen said:

The PR to the extension with the new help message has been merged, but not released. (The release is waiting on me to update the README, and this is in progress but not done.)

I see. By the way, that updated pop-up says "please open the directory" and then its button says "switch to correct folder".

Which makes it doubtful that the button will do the right thing.

I'd prefer that it said "please switch to the correct directory", and the button said "switch to correct directory".

Patrick Massot (Jul 03 2020 at 20:55):

Dima, Anatole is trying to tell you that you posted a link to the documentation of the wrong software.

Dima Pasechnik (Jul 03 2020 at 20:58):

Patrick Massot said:

Dima, Anatole is trying to tell you that you posted a link to the documentation of the wrong software.

I posted the link just as an illustration of the IDE's "project" concept, not as anything more specific.

Anatole Dedecker (Jul 03 2020 at 21:07):

I actually tend to say that vscode is a text editor (like atom, Sublime Text, ...) more than an IDE : it doesn't really have this notion of project. You open it in a directory and you can edit whatever is in this directory. Here the "project" part comes from lean : the lean extension needs you to open the editor in a certain directory which lean can work with, and I described the content of this directory earlier. So in theory if you used leanproject and do code . in the right directory everything should just work fine

Dima Pasechnik (Jul 04 2020 at 07:38):

sure, vscode is an extendable text editor, and various vscode plugins make it into an IDE by creating projects.

vscode+lean extension is basically an IDE - I don't know whether it can create empty projects, or create projects from a collection of files, as some IDE's can.

Johan Commelin (Jul 04 2020 at 07:41):

I'm not aware of such functionality. I guess it could be added as feature to the lean extension.

Dima Pasechnik (Jul 04 2020 at 08:05):

What is the reason for leanpkg.path to contain the line path src/solutions ? (something that got me sidetracked :))

Johan Commelin (Jul 04 2020 at 08:09):

I don't know. I've never edited leanpkg.path`.

Last updated: May 13 2021 at 04:21 UTC