Zulip Chat Archive

Stream: maths

Topic: VSCode not showing errors


view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Jun 13 2020 at 15:13):

Restarting lean doesn't fix it

view this post on Zulip Bhavik Mehta (Jun 13 2020 at 15:13):

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

view this post on Zulip 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)

view this post on Zulip 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!)

view this post on Zulip Gabriel Ebner (Jun 13 2020 at 15:18):

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

view this post on Zulip Bhavik Mehta (Jun 13 2020 at 15:18):

Nope

view this post on Zulip 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: May 14 2021 at 18:28 UTC