Zulip Chat Archive

Stream: lean4

Topic: VSCode error message


Kenny Lau (Jan 05 2021 at 15:47):

How do I view the error messages on VSCode?

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

Edward Ayers (Jan 05 2021 at 15:50):

Following your intructions at 'How to install Lean 4'

Kenny Lau (Jan 05 2021 at 15:51):

oh, that works

Kenny Lau (Jan 05 2021 at 15:51):

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

Edward Ayers (Jan 05 2021 at 15:51):

It's back to basics for a while I guess

Edward Ayers (Jan 05 2021 at 15:52):

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


Last updated: Dec 20 2023 at 11:08 UTC