v4.18.0 - inlay hints

Stream: general

[Jason Rute]

I just saw on live.lean-lang.org that auto implicit variables are automatically shown in grey! This is amazing. I’ve been asking for something like this for years. (IntelliJ has a feature like this for Scala implicits, which are more related to type classes, but I thought it would be good for Lean implicit variables too!)

[Patrick Massot]

Yes, this is the inlay hint feature at work!

[Shreyas Srinivas]

There's a small bug in this feature. When I click on the autoimplicit inlay to add the variable explicitly, I get a second copy of the inlay as in the screenshot below:

Screenshot from 2025-03-04 14-51-35.png

[Shreyas Srinivas]

CC : @Marc Huisinga

[Marc Huisinga]

Is this in the web editor?

[Marc Huisinga]

I can't reproduce the issue in VS Code.

[Shreyas Srinivas]

Yeah web editor

[Bhavik Mehta]

Can reproduce: https://live.lean-lang.org/#codez=KYDwhgtgDgNsAEBvAzvALvAXPQjcAF8tcsBeeZAewCdKBPIA

[Rémy Degenne]

If I open that link, wait for the grey {α} to appear, then insert a line break before example, then after a second or two the {α} moves and I see exampl {α}e

[Jireh Loreaux]

Iterating keeps moving {α} one character to the left.

[Patrick Massot]

@Jon Eugster If inlay hints are broken in Monaco, maybe there is some option to deactivate them?

[Damiano Testa]

It looks like the inlay hints do not use the "current" edit-state of the file, but the filemap at the time of last saving.

[Jireh Loreaux]

This makes me want to turn auto-implicit on in Mathlib again (although I never wanted to turn it off :laughing:)

[Patrick Massot]

Yes, this will allow us to get the best of both options.

[Eric Wieser]

We still lose out when reviewing on github, where inlay hints aren't a thing

[Jon Eugster]

Patrick Massot said:

Jon Eugster If inlay hints are broken in Monaco, maybe there is some option to deactivate them?

I'm afraid I currently don't know what the issue is. I can't reproduce it in lean4monaco where everything seems to work fine, so must be something particular to lean4web. Maybe about how the editor content is handled in React...?

Damiano Testa said:

It looks like the inlay hints do not use the "current" edit-state of the file, but the filemap at the time of last saving.

what do you mean by this observation?

[Marc Huisinga]

@Jon Eugster I think we figured out what the issue is. It likely has to do with the way that the Live setup works.

[Damiano Testa]

What I meant, is that it looks like the position where the inlay is displayed is the same as it was before you started editing the file. Subsequent edits do not alter the position, it just keeps being displayed at the same String.pos as in the original setup.

[Marc Huisinga]

Inlay hints should work correctly again on https://live.lean-lang.org.

[Patrick Massot]

Eric Wieser said:

We still lose out when reviewing on github, where inlay hints aren't a thing

I really don’t think this is enough motivation. I was already not convinced to give up auto-implicit before inlay hints, but here the argument becomes really really weak.

[Yaël Dillies]

Auto-implicits don't enforce that similar lemmas in sections use the same variable names

[Patrick Massot]

Yes, that’s indeed one more argument in favor of auto-implicit: we can choose variable names more freely.

[Eric Wieser]

Do inlay hints have neovim / emacs support? (I know this matters much less for beginners than vscode)

[Aaron Liu]

Marc Huisinga said:

Inlay hints should work correctly again on https://live.lean-lang.org.

The inlay seems to be fixed, but not the insertion (double click to insert)

[Henrik Böving]

Eric Wieser said:

Do inlay hints have neovim / emacs support? (I know this matters much less for beginners than vscode)

Yes they are supported in neovim, I know emacs has the appropriate options and infrastructure on its side though I haven't seen for myself that it works so only 99% ^^

[Marc Huisinga]

Aaron Liu said:

Marc Huisinga said:

Inlay hints should work correctly again on https://live.lean-lang.org.

The inlay seems to be fixed, but not the insertion (double click to insert)

Do you have an MWE?

[Jon Eugster]

Aaron Liu said:

The inlay seems to be fixed, but not the insertion (double click to insert)

Seems to work fine for me on the example above

[Marc Huisinga]

Eric Wieser said:

Do inlay hints have neovim / emacs support? (I know this matters much less for beginners than vscode)

@Julian Berman helped test inlay hints in NeoVim before the release. AFAICT the Emacs plugin is practically unmaintained at this point and has been broken in several ways for a long time.

[Eric Paul]

Here's a fairly unimportant issue but one that I think would be nice for hovering on the inlay hints:

At the moment, I can hover over an inlay hint for an implicit parameter and it says, for example, α : Sort u_1. But when there are multiple implicit parameters, if after hovering on one, I move my cursor to the other, it does not update this information. Or even with just a single implicit parameter, if I go from hovering over the inlay hint generally to actually on that parameter, it does not update to its information.

(I've only tested this in the web editor)

[Aaron Liu]

Marc Huisinga said:

Aaron Liu said:

Marc Huisinga said:

Inlay hints should work correctly again on https://live.lean-lang.org.

The inlay seems to be fixed, but not the insertion (double click to insert)

Do you have an MWE?

Lean 4 Web - Google Chrome 2025-03-04 15-53-12.mp4

[Bhavik Mehta]

Yup I can get that to happen too now

[Marc Huisinga]

Aaron Liu said:

Marc Huisinga said:

Aaron Liu said:

Marc Huisinga said:

Inlay hints should work correctly again on https://live.lean-lang.org.

The inlay seems to be fixed, but not the insertion (double click to insert)

Do you have an MWE?

Lean 4 Web - Google Chrome 2025-03-04 15-53-12.mp4

Thanks, I can reproduce this. The issue appears to occur when attempting to apply the inlay hint during the edit delay. I'll look into it.

[Marc Huisinga]

Eric Paul said:

Here's a fairly unimportant issue but one that I think would be nice for hovering on the inlay hints:

At the moment, I can hover over an inlay hint for an implicit parameter and it says, for example, α : Sort u_1. But when there are multiple implicit parameters, if after hovering on one, I move my cursor to the other, it does not update this information. Or even with just a single implicit parameter, if I go from hovering over the inlay hint generally to actually on that parameter, it does not update to its information.

(I've only tested this in the web editor)

This is a bug in VS Code as well. Perhaps we should just display all auto-implicits and their types in the same hover to work around it.

[Marc Huisinga]

The insertion issue appears to be yet another VS Code / Monaco bug. I'll see if we can somehow work around it.

[Jon Eugster]

Btw, for lean4web it's useful if you test wether things work as expected in you local VSCode and then if it's a bug which is only appearing in lean4web, append it here: lean4web#55

I'll try to fix all these then at some point, but it's useful if Marc can first fix anything that's not web-related.

[Marc Huisinga]

PR to fix the inlay hint insertion issue: lean4#7343
PR to combine auto-implicit inlay hint tooltips into one to work around buggy VS Code inlay hint hover behavior: lean4#7344