Question about blue squiggly underline

[xpe]

Is the squiggly line under #eval to be expected? I am pretty sure these are generated by Zed diagnostics. Perhaps this mechanism is how this extension shows outputs from the lean LSP?

Environment

> lean --version
Lean (version 4.26.0, arm64-apple-darwin24.6.0, commit d8204c9fd894f91bbb2cdfec5912ec8196fd8562, Release)

> elan --version
elan 4.1.2 (58e8d545e 2025-05-26)

> zed --version
Zed 0.217.3 – /Applications/Zed.app

> sw_vers
ProductName:            macOS
ProductVersion:         15.7.3
BuildVersion:           24G419

[xpe]

Hmmm. VS Code with the Lean4 extension looks very similar.

Semantically, this makes no sense to me. There is no problem here.

[xpe]

This has to do with the Lean LSP, not this extension, best I can tell, but it does affect Zed users downstream... so I'm trying to make this nicer, especially for new users. My first impression here is "yuck", to be open, but I'm trying very hard to see many angles on this.

So I read this in my research leanprover/lean4#1590 (comment) :

The user does see "information" vs "hint" quite clearly, as you've observed: "information" shows up with the info icon in the Problems view. They are eye catching and bring your attention to them from anywhere in the project, which is exactly the intended behavior for something that is the equivalent of a write to stdout. "Hint" can only be seen when you happen to be looking in the area (there is no global list of them AFAIK) and plays a role more similar to code lens or other local information gathering.

That is all to say that I agree with Patrick: lean is using the correct mechanism to signal the output of output-producing operations in the IDE. If you want to make the blue squiggles go away, stop writing #eval and #check.

After chewing on this, my current take is: these squiggles are confusing and problematic. Literally "problematic" because they show up in the "Problems" pane in VS Code. In Zed, they are Diagnostics -- both of which indicate, more or less, "you should see this and fix it".

I feel like better ways are available, because I'm pretty sure LSP have other mechanisms besides DiagnosticSeverity.information to convey information back to the host editor.

Claude Opus 4.5 directly captures my take on the matter:

The Lean extension's choice to use info-level diagnostics optimizes for visibility (you see immediately that #eval is special) at the cost of visual noise and semantic mismatch (squiggles suggest problems).

[owlx56]

By this way, Zed can show #eval as lens to the right of the code(Inline diagnostics):

VS Code also can do it by Error Lens:

Since Zed doesn't have a Problems panel, the squiggly underline is the main visual noise issue.

Looking at Zed's source code, there's an internal underline_diagnostic method in the LspAdapter trait that allows disabling the underline for specific diagnostics while preserving the diagnostic itself — meaning inline diagnostics would still display the output.

However, this method is not currently exposed in the zed_extension_api, so extensions cannot customize this behavior.

It would be great if Zed could either:

1. Expose underline_diagnostic in the extension API, or
2. Add a setting to disable underlines for specific diagnostic severities (e.g., Information)

According to Gemini, Zed renders DiagnosticSeverity.hint and DiagnosticSeverity.information with the same underline color, but differentiates them in inline diagnostics and scrollbar markers. Therefore, switching to DiagnosticSeverity.hint will not help.

That is all to say that I agree with Patrick: lean is using the correct mechanism to signal the output of output-producing operations in the IDE. If you want to make the blue squiggles go away, stop writing #eval and #check.

As it says, #eval and #check are development/debugging tools and typically do not appear in production Lean 4 project code.

[xpe]

Thanks for your reply. I can see that when writing a Zed extension, no good deed goes unpunished.

As it says, #eval and #check are development/debugging tools and typically do not appear in production Lean 4 project code.

This is a bit funny to me, because I would guess many Lean projects exist in an ongoing state of development and debugging!

Forgive my talking-out-loud here... It is notable that almost all of the screenshots and (few) video tutorials have the blue squiggles. It almost looks like a kind of Stockholm syndrome to me.

I've been reading more of the LSP protocol specs and looking at various language usage to figure out the intended and actual semantics. I'm not completely convinced at this point, but I'm seeing more indications that #eval and #print statements don't belong as "Diagnostics" and instead make more sense as code lenses or inlay hints.

If you have a moment to weigh in ... What do you think are the most compelling logical arguments for using:

• Diagnostics (DiagnosticSeverity.information)
• code lenses
• inlay hints
• something else?

[owlx56]

This is a bit funny to me, because I would guess many Lean projects exist in an ongoing state of development and debugging!

There is always a gap between theory and reality.

Personally speaking, inlay hints would be the ideal solution. This approach would not only avoid underlines but also allow developers to conveniently view the results. It seems that code lenses are more frequently used for interactive scenarios. However, I doubt whether the Zed extension API can achieve this. Or you can try to convince the Lean 4 developers.