weird vscode troubles?

Stream: general

[Gabriel Ebner]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Gabriel Ebner]

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]

Yes, it also happens to me currently.

[Bryan Gin-ge Chen]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

I think this should fix it. Sorry about this!

[Gabriel Ebner]

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

[Scott Morrison]

Yep, that fixed it.

[Gabriel Ebner]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

It just says lean.

[Kevin Buzzard]

Try deleting it and see if it helps :-)

[Gabriel Ebner]

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]

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]

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?