Zulip Chat Archive

Stream: lean4

Topic: VSCode error message


view this post on Zulip Kenny Lau (Jan 05 2021 at 15:47):

How do I view the error messages on VSCode?

view this post on Zulip Edward Ayers (Jan 05 2021 at 15:49):

I can see the errors in the 'problems' pane. I am using the vscode extension mhuisi.lean4

view this post on Zulip Edward Ayers (Jan 05 2021 at 15:50):

Following your intructions at 'How to install Lean 4'

view this post on Zulip Kenny Lau (Jan 05 2021 at 15:51):

oh, that works

view this post on Zulip Kenny Lau (Jan 05 2021 at 15:51):

I was just used to the "All Messages" window that exists for Lean 3

view this post on Zulip Edward Ayers (Jan 05 2021 at 15:51):

It's back to basics for a while I guess

view this post on Zulip Edward Ayers (Jan 05 2021 at 15:52):

You can also whack F8 and it will show the error message inline


Last updated: May 18 2021 at 23:14 UTC