Zulip Chat Archive
Stream: general
Topic: blue squiggly lines
Stavros (Sep 04 2022 at 19:17):
hello,
does anyone know how i can get rid of the blue squiggly lines underlying LEAN code in VS code:
many thanks!
Stavros
Eric Rodriguez (Sep 04 2022 at 19:18):
these are to highlight that these lines have output - I'm not sure if they are disableable.
Bryan Gin-ge Chen (Sep 04 2022 at 19:21):
The blue squiggly lines are expected; they indicate that the Lean server is returning output to you at your #eval statements.
Apparently it's possible to set the style of them to transparent by playing with your settings (I haven't tried this myself): https://stackoverflow.com/a/48610661
Stavros (Sep 04 2022 at 19:30):
i see... unfortunately they also seem to have the side effect of adding squiggly lines to all comments that follow?
for instance, in my code above, comment "-- subtraction" and everything below is underlined, whereas "-- addition" and everything above is not.
this seems like a bug, and is annoying. does anyone have a fix?
thanks again!
Kevin Buzzard (Sep 04 2022 at 20:06):
I think this is a recent regression, at least for me
Patrick Massot (Sep 04 2022 at 20:31):
I think this bug was fixed in July. Did it come back? Which version of lean are you using?
Patrick Massot (Sep 04 2022 at 20:32):
I cannot reproduce this on a recent Lean but it was indeed extremely annoying in July.
Stavros (Sep 04 2022 at 20:59):
i am using LEAN 3 language support for VS Code, v0.16.54.
Name: lean
Id: jroesch.lean
Description: Lean 3 language support for VS Code
Version: 0.16.54
Publisher: leanprover
VS Marketplace Link: https://marketplace.visualstudio.com/items?itemName=jroesch.lean
when i click on "install another version" it shows me that this is the latest version ("1 wk ago"):
image.png
i am also using VS Code:
Version: 1.71.0 (user setup)
Commit: 784b0177c56c607789f9638da7b6bf3230d47a8c
Date: 2022-09-01T07:36:10.600Z
Electron: 19.0.12
Chromium: 102.0.5005.167
Node.js: 16.14.2
V8: 10.2.154.15-electron.0
OS: Windows_NT x64 10.0.19043
Sandboxed: No
Patrick Massot (Sep 04 2022 at 20:59):
This isn't what I'm asking
Patrick Massot (Sep 04 2022 at 20:59):
I'm asking which version of Lean, not which version of the VSCode extension
Patrick Massot (Sep 04 2022 at 21:00):
What does #eval lean.version says in that file?
Stavros (Sep 04 2022 at 21:05):
it says
(3, (10, 0))
btw, going back to version 0.16.43 (8 months ago) fixes the problem.
Patrick Massot (Sep 04 2022 at 21:05):
This bug happens when you combine a recent VSCode extension with an old Lean.
Patrick Massot (Sep 04 2022 at 21:06):
So indeed you can downgrade the VSCode extension. But a much better solution is to update Lean.
Stavros (Sep 04 2022 at 21:06):
you mean upgrade to LEAN 4 ?
Patrick Massot (Sep 04 2022 at 21:07):
No. Upgrade Lean 3.
Patrick Massot (Sep 04 2022 at 21:07):
Your version of Lean 3 is from 02 May 2020, this really ancient.
Patrick Massot (Sep 04 2022 at 21:07):
How did you end up with such an outdated Lean?
Patrick Massot (Sep 04 2022 at 21:09):
You are 38 releases behind present.
Stavros (Sep 04 2022 at 21:09):
i will look into updating my LEAN 3, but a student of mine who just installed LEAN 3 a few days ago seems to have the same problem. i will ask him what version he has.
will get back, many thanks!
Patrick Massot (Sep 04 2022 at 21:09):
Did you start using Lean recently?
Patrick Massot (Sep 04 2022 at 21:10):
If yes then you did something really wrong to install Lean or start your project.
Stavros (Sep 04 2022 at 21:10):
no, i've been using it since 2020 and teaching several classes with it
Patrick Massot (Sep 04 2022 at 21:11):
Ok, that makes sense. So indeed the issue is that we have no way to tell VSCode not to update the extension when people use old versions of Lean. This would require having several versions of the extension, one for each project.
Patrick Massot (Sep 04 2022 at 21:12):
Do you use mathlib in your code? If not then updating Lean shouldn't be too painful. Otherwise it will be quite a journey, and if you were happy with your code then pinning the VSCode extension to an old one is probably the best idea.
Stavros (Sep 04 2022 at 21:14):
ok, got it, many thanks!
Patrick Massot (Sep 04 2022 at 21:17):
@Gabriel Ebner do you think it would be possible for the extension to display a warning and advice when it detects an incompatible version of Lean? There aren't too many cases but the one described in this case is really bad, especially for teaching (it hit us at the worse time for the summer school at ICERM and it was really really nasty).
Chris Lovett (Sep 12 2022 at 19:21):
I see the same thing on not so old version of lean3, I was on version 3.44 and when I upgraded to 3.48 the squiggles are correct. It seems like the problem was first fixed in 3.45. Perhaps this commit was the actual fix? But personally I also find all the blue squiggles distracting at best and would love to find a way to hide them automatically...
Patrick Massot (Sep 12 2022 at 19:42):
Yes, that's the fix
Chris Lovett (Sep 12 2022 at 20:47):
I found a way to remove blue squiggles entirely, replacing them with an ellipsis you can hover over instead, which also has the nice side effect of removing them from the VS Code "Problems list" in the output window. See https://github.com/leanprover/lean4/issues/1590
Last updated: Dec 20 2023 at 11:08 UTC