inlayHint

Stream: Emacs

[Yury G. Kudryashov]

After an upgrade to 4.18.0-rc1, I'm getting this warning:

Warning (lsp-mode): Unknown request method: workspace/inlayHint/refresh

Did something change in the Lean lsp server implementation?

[Patrick Massot]

Yes, Marc worked a lot on inlay hints.

[Patrick Massot]

This mean some extra text displayed by the editor which is not in your source code.

[Patrick Massot]

https://github.com/leanprover/lean4/pull/7112

[Patrick Massot]

https://github.com/leanprover/lean4/pull/6768 has some screenshot

[Patrick Massot]

The very light gray stuff in
image.png
is not part of the file, it’s added by the editor.

[Patrick Massot]

those are auto-implicit types.

[Yury G. Kudryashov]

Thank you! I'll see if Emacs lsp supports them. For now, I'll just ignore the warning.

[Yury G. Kudryashov]

@Mekeor Melire Do you know anything about this?

[Mauricio Collares]

(setq lsp-inlay-hint-enable t)
(lsp-inlay-hints-mode)

[Yury G. Kudryashov]

I tried this, and I'm still getting the warnings.

[Mauricio Collares]

What's your lsp-mode package version? I can see the inlay hints here.

[Yury G. Kudryashov]

9.0.1

[Mauricio Collares]

Right, I see the same thing as well when opening Mathlib/Control/Random.lean. lsp-mode contains this line:

,@(when lsp-inlay-hint-enable '((inlayHint . ((refreshSupport . :json-false)))))

which indicates the server shouldn't be sending refresh requests in the first place (and inlay hints work without them). cc @Marc Huisinga

[Marc Huisinga]

Feel free to open a bug report about this in the Lean 4 repository. Note that without support for refresh requests, inlay hints cannot ever become a usable feature in any editor that lacks them.
Currently, we don't really implement any support for client capabilities at all; either the client supports the features that are provided by the Lean language server with its various extensions and LSP spec violations that are necessary for interactive theorem proving, or it will be broken in various ways and (at best) only function correctly in some cases by accident.

In general, my recommendation would be to switch to a plugin that is actually being maintained (like the NeoVim plugin) and hasn't been in a half-broken and unmaintained state for years. Alternatively, someone needs to step up to properly maintain the Emacs plugin and bring it into a mostly feature-complete and working state, after which I'll be happy to coordinate changes to the language server with the maintainer before a release, as we now do with NeoVim.

[Mauricio Collares]

Thanks for the information! I think it's fair to say no one will switch from Emacs to vim to get inlay hints, but I will file an issue in the lsp-mode repository now that I know that support for refresh requests is essential.

[Mauricio Collares]

Posted a comment on a preexisting issue (https://github.com/emacs-lsp/lsp-mode/issues/4230), but that was filed for the semgrep LSP. I will file a separate issue if I don't see activity after a few days.

[David Renshaw]

I opened an issue: lean4#7488

[David Renshaw]

in a half-broken and unmaintained state for years

lean4-mode had been working well for me, until this warning started showing up.

[Berber]

i'm kind of sad that emacs lean4-mode is in such a bad state. i am also just sad that working with lean is almost only possible with vs code and nvim. i am happy that there is at least one other editor than vs code.

[Julian Berman]

As just an interested outsider I think Marc made it sound like above that all that's really needed is some more ownership over pushing the emacs plugin forward, no? I think @Yury G. Kudryashov expressed similar sentiments before that he feels he's not quite an expert enough in emacs to own maintenance (apologies if I'm misremembering). It looks like there's 4 current open PRs, if it's helpful I'm happy to review some of them even myself if they're stuff I had to understand for the nvim plugin, though of course I'm not an emacs expert by any means, but it seems to me like a decent step is someone saying they want to own helping to review the open PRs and perhaps then that person or one or more people getting commit bit on the repo (or otherwise it living somewhere else if leanprover-community is less comfortable with giving that out).

[Julian Berman]

(None of which is to say that if it worked fine before and it's easy enough to do so that just disabling this warning might be a good short term thing -- though I think it sounded like the LSP doesn't really respect client capabilities at all at the minute so who knows how easy that is. Well. Marc is a who :)

[David Renshaw]

The above discussion makes it sound like this particular issue (lack of support for inlay refresh) is with upstream lsp-mode, not with lean4-mode.

[Berber]

indeed, i also understand the problem as being with lsp-mode, not with lean4-mode.

however, the fact that the last commit has been 3 months ago, and that its development seems scattered (with good efforts that i support, like making it work with eglot), does not look good.

[Kevin Buzzard]

My impression is that the community would welcome people who would like to make the Lean-in-emacs experience better. Whilst the majority of people here use VS Code, several power users are using nvim and certainly there have been power users using emacs in the past (and the existence of this channel is another indication that people are interested). Lean is rapidly-changing software and my understanding of the above discussion is that it is only recently that things got derailed a bit with recent changes to core Lean.

[Yury G. Kudryashov]

Indeed, I don't have much time for Emacs lean4-mode. I'll do my best to go over the open PRs this weekend.

[Yury G. Kudryashov]

AFAIR, at least one of the open PRs is a large refactor. I plan to cherry-pick some parts of it to the current HEAD, then decide what to do with non-bc changes.

[Joseph Myers]

I'm working around this warning with

(setq warning-minimum-level :error)

(though that potentially disables other warnings as well).

[Yury G. Kudryashov]

Pressing Enter adds this to custom-set-variables:

'(warning-suppress-types '((lsp-mode)))

[Notification Bot]

6 messages were moved from this topic to #Emacs > Dev: Inlay Hint Refresh Request by Mekeor Melire.

[Mekeor Melire]

(Sorry for the noise, I had bad luck renaming this topic in Zulip. Further discussion will take place in Dev: Inlay Hint Refresh Request topic.)