## Stream: general

### Topic: weird vscode troubles?

#### Gabriel Ebner (Mar 06 2020 at 14:48):

Sometimes the error squiggles in vscode appear at the beginning of the file instead of the correct position. The info view is correct, though? Does this happen to anyone else?

#### Bryan Gin-ge Chen (Mar 06 2020 at 14:49):

Uh-oh. I wonder if I introduced a bug when I edited the diagnostics file.

#### Bryan Gin-ge Chen (Mar 06 2020 at 14:50):

I'm not sure but my guess would be that these lines are failing and you end up with a bad range.

#### Bryan Gin-ge Chen (Mar 06 2020 at 14:51):

Do you have a reliable reproduction? I can try to look into this.

#### Gabriel Ebner (Mar 06 2020 at 14:53):

Not really. Most of the time restarting vscode seems to fix it. If I see it the next time, is there anything I can do to gather more information?

#### Sebastien Gouezel (Mar 06 2020 at 14:53):

Yes, it also happens to me currently.

#### Bryan Gin-ge Chen (Mar 06 2020 at 15:02):

I don't know of an easy way to collect more info when it fails, unfortunately. Does it tend to happen when you're opening a file or just randomly when you're editing and errors pop up?

#### Gabriel Ebner (Mar 06 2020 at 15:03):

It used to only happen while I was editing a file. Now it also happens when I first open the file. And restarting vscode does not fix it.

#### Bryan Gin-ge Chen (Mar 06 2020 at 15:05):

OK, I can reproduce the bug after some random editing. Let me work on this for a bit.

#### Bryan Gin-ge Chen (Mar 06 2020 at 15:42):

https://github.com/leanprover/vscode-lean/pull/147

#### Gabriel Ebner (Mar 06 2020 at 15:56):

I've just released 0.15.8. Let's hope that this was the issue!

#### Scott Morrison (Mar 06 2020 at 16:32):

Yep, that fixed it.

#### Gabriel Ebner (Mar 06 2020 at 16:38):

That's good to hear. In the future please feel free to complain about the vscode extension, in particular if it suddenly gets worse.

#### Scott Morrison (Mar 06 2020 at 16:39):

I only noticed it late last night, and hadn't gotten around to complaining. :-)

#### Kevin Buzzard (Mar 06 2020 at 17:10):

We also noticed it at Xena, I just assumed it was some student who had done a crazy thing -- and then it happened to me later :-)

#### Floris van Doorn (Mar 06 2020 at 19:32):

Gabriel Ebner said:

That's good to hear. In the future please feel free to complain about the vscode extension, in particular if it suddenly gets worse.

One thing I'm noticing lately (since a couple of weeks) is that it takes longer for the extension to "start up" (it sometimes takes 5+ seconds to even start showing the "busy" yellow lines). My guess is that this has to do with the different versions of Lean. I never updated my "default" Lean version, so maybe it's busy changing Lean to the version specified in leanpkg.toml.
I just tested: opening a file that doesn't import anything from mathlib took about 1 second before starting to show yellow lines, but opening a file that imports all of mathlib took ~20 seconds before starting to show yellow lines.

#### Kevin Buzzard (Mar 06 2020 at 19:39):

I haven't had this problem on Ubuntu, but then again I'm not sure I know how to import all of mathlib.

#### Kevin Buzzard (Mar 06 2020 at 19:39):

Is your lean executable path set to something funny in VS Code? Mine just says lean

#### Kevin Buzzard (Mar 06 2020 at 19:40):

oh wow, on my laptop this field is empty. On my desktop it says lean. I don't even know which one is right.

#### Floris van Doorn (Mar 06 2020 at 19:41):

It just says lean.

#### Kevin Buzzard (Mar 06 2020 at 19:46):

Try deleting it and see if it helps :-)

#### Gabriel Ebner (Mar 06 2020 at 20:04):

I fear that's not the fault of the vscode extension. mathlib just keeps growing. :shrug:

$echo import all > import_all.lean$ time lean import_all.lean
9.80user 0.38system 0:10.13elapsed 100%CPU (0avgtext+0avgdata 978980maxresident)k
0inputs+0outputs (0major+245091minor)pagefaults 0swaps


(This is on my desktop with a nice SSD.) I just timed it, and it also takes 10s from typing code . until the yellow bar goes away. It might be misleading that the yellow bar doesn't come on until a few seconds after the server starts up. I believe it starts showing after we've read the oleans for all the imports. (The server sends the lines to highlight, so this is not something we can easily fix in the vscode extension itself.)

#### Floris van Doorn (Mar 06 2020 at 20:37):

Ah, ok. If it's already busy importing (or at least reading) files before the yellow lines show up, then this behavior makes sense. Thanks for checking on this :thumbs_up:

#### Kevin Buzzard (Mar 08 2020 at 17:53):

Something which has been bugging me for about a week or so with VS Code: I often want to see the definition of term. I tend to move my cursor onto the term, and then right-click -> go to definition. Recently, if the term is relatively near the top of the screen and has a large docstring, then the docstring has started appearing directly under the cursor, stopping me from being able to right-click! I think by default the hover-window or whatever it's called (the transient thing) appears safely above the term, but if the term is near the top of the VS Code window then instead of appearing below it, it appears on top of it. Did something change or are my reflexes just getting slower?

Last updated: May 13 2021 at 18:26 UTC