customizing vscode

Stream: new members

[Dima Pasechnik]

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]

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]

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]

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]

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]

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

[Dima Pasechnik]

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]

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]

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]

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

[Dima Pasechnik]

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

[Mario Carneiro]

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

[Dima Pasechnik]

I have

$ cat leanpkg.path
builtin_path
path _target/deps/mathlib/src
path ./src/solutions
path ./src/exercises #      <-  Added by me

[Dima Pasechnik]

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]

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]

from the readme

[Mario Carneiro]

You are apparently supposed to copy the contents of the src/exercises folder to src/, not source it directly

[Dima Pasechnik]

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]

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]

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]

but that should be fine for the tutorial

[Dima Pasechnik]

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]

I've never touched that icon ever

[Dima Pasechnik]

Mario Carneiro said:

I've never touched that icon ever

perhaps the warning is there, it just did not pop up?

[Mario Carneiro]

I just followed Bryan's instructions and got the same result

[Mario Carneiro]

0 notifications

[Dima Pasechnik]

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]

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

[Patrick Massot]

tutos.gif

[Patrick Massot]

This is what is meant by the instructions.

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Dima Pasechnik]

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]

my_exercises is not baked anywhere

[Mario Carneiro]

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]

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]

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

[Patrick Massot]

@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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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.

[Patrick Massot]

Yes

[Mario Carneiro]

that should be a warning, yes?

[Patrick Massot]

Yes, gentle warning offering help.

[Dima Pasechnik]

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]

because the leanpkg.path file defines the root

[Mario Carneiro]

everything is relative to that file

[Gabriel Ebner]

Mario Carneiro said:

that should be a warning, yes?

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

[Patrick Massot]

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]

You can still click cancel.

[Mario Carneiro]

What happens if the folder cannot be located?

[Gabriel Ebner]

Then nothing changes compared to now.

[Gabriel Ebner]

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

[Bryan Gin-ge Chen]

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]

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]

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]

maybe you'd prefer using the emacs plugin

[Jalex Stark]

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]

and I click on the root directory of a project

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Patrick Massot]

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]

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".

[Dima Pasechnik]

cf. https://docs.microsoft.com/en-us/visualstudio/get-started/tutorial-projects-solutions

[Anatole Dedecker]

Visual Studio is quite different from Visual Studio Code

[Anatole Dedecker]

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]

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

[Anatole Dedecker]

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

[Dima Pasechnik]

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]

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]

Anatole Dedecker said:

Visual Studio is quite different from Visual Studio Code

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

[Dima Pasechnik]

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]

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

[Dima Pasechnik]

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]

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]

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]

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

[Dima Pasechnik]

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

[Johan Commelin]

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