search

leanprover / vscode-lean

Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language.
Apache License 2.0
116 stars 49 forks source link

Make incomplete proofs more prominent #337

Open DanielFabian opened 1 year ago

DanielFabian commented 1 year ago

I've been working through mathematics in lean and I've found on the same page multiple incomplete proofs that I just didn't notice.

As it stands it puts a red squiggly under the by for a the tactics block.

It's pretty small and somewhat easy to miss.

How hard would it be to add something more prominent like the yellow squiggly when a proof uses sorry?

Maybe it's yellow when it uses sorry and red if it does not type check?

What are the thoughts on this.

PatrickMassot commented 1 year ago

I fully agree, and this is an issue for teaching especially. My workaround is to use the Error Lens VSCode extension, but this shouldn't be required.

Kha commented 1 year ago

We already have the progress indicator, projecting errors and other diagnostics onto that as well seems like a natural solution to me. Not sure if this should be changed in the server, as the client already has all relevant data for doing so.