Zulip Chat Archive

Stream: maths

Topic: VSCode not showing errors


Bhavik Mehta (Jun 13 2020 at 15:13):

VS code isn't showing red underlines for errors for me, even though the problems bar at the bottom does and I'm getting lean errors on the right

Bhavik Mehta (Jun 13 2020 at 15:13):

Restarting lean doesn't fix it

Bhavik Mehta (Jun 13 2020 at 15:13):

Oh it's back now... how confusing!

Bryan Gin-ge Chen (Jun 13 2020 at 15:15):

Very odd. If you can figure out how to reproduce this, please create an issue at the vscode-lean repo. (Also, I'm not sure this thread should be in #maths)

Bhavik Mehta (Jun 13 2020 at 15:17):

Will do! (Sorry, my mistake - meant to put it in #new members and must have missed somehow!)

Gabriel Ebner (Jun 13 2020 at 15:18):

Did you use the git extension to revert a change, etc.?

Bhavik Mehta (Jun 13 2020 at 15:18):

Nope

Gabriel Ebner (Jun 13 2020 at 15:19):

I have also run into this issue. Most often it happens when I revert a change. Sometimes it helps to just close the current file and open it again.


Last updated: Dec 20 2023 at 11:08 UTC