Remove the blue sqiggly underline in vscode for #eval, etc

Stream: lean4

[Nehal Patel]

image.png
Is there a way to have vscode not put a blue quiggly line under #eval, #check, etc? thanks

[Aaron Liu]

the VSCode has a hard limit of 500 squiggles per file, so if have more then 500 squiggles higher up in the file then it will not generate any more squiggles (unfortunately this gets rid of other squiggles too, not just in #eval, #check, etc.)

[Julian Berman]

The squiggles are part of VSCode indicating there is an INFO level diagnostic on that line. Do you really want to make all such indications go away (and I guess you have VSCode's error lens thingy enabled there?) If so I'm sure there's a setting to configure the style of that line, if only by making it be #000000 and blend with the background

[Snir Broshi]

Indeed, you can add this to your VSCode's settings.json:

"workbench.colorCustomizations": {
  "editorInfo.foreground": "#00000000"
}

See #general > error lens in lean4

[Nehal Patel]

Amazing — Thank you!