neovim (error message/processing message)

Stream: general

[Antoine Chambert-Loir]

I have two questions about lean.nvim in neovim.

1. After a recent update, I get the error message

lean.setup { lsp = { ... } } is deprecated, use call vim.lsp.config('leanls', { ... }) directly in
stead.
Feature will be removed in lean.nvim v2025.12.1

which I didn't manage to address.

2. When I run LeanRefreshFileDependencies, the infoview window prints a plain Processing File without any indication of what it's doing. I have seen that vscode gives more information.
   Would it be possible to have it too? Moreover, that info line is only visible if the cursor is on the first line of the file.

[Julian Berman]

This should fix 1. https://github.com/AntoineChambert-Loir/nvim/pull/2

[Julian Berman]

Can you maybe tell me a bit more about 2 -- if I open A.lean and B.lean in VSCode and A depends on B, and I modify B, I see the imports out of date message and then if I restart file in VSCode I don't seem to see any more detail while that's happening.

[Julian Berman]

(As for it only appearing on the first line -- this is coming very soon, I already have a change locally to dim the infoview when imports are out of date, which I'll push as soon as I get some time to write docs and an automated test.)

[Kevin Buzzard]

In VS Code if you modify a file and then click refresh dependencies on a second file quite a long way further down the heirarchy then you can see which file is being built and how many more need to be built before your refreshed file comes alive again. I would send a gif but I've got two VS Code's open and am ploughing through the diffs between two 876M trace dumps so am a bit reluctant to touch anything...

[Julian Berman]

Interesting, thanks! That helps, let me see if I can reproduce.

[Antoine Chambert-Loir]

I should have been more specific, and Kevin pointed out exactly what I had in mind.

[Christian Merten]

I don't know if Antoine is already implying that, but let me point out that I used to see more information when refreshing a file. Since updating a few days ago, I only see Processing file.

[Julian Berman]

I just pushed a commit which I think should give us the same information as what you see in VSCode (https://github.com/Julian/lean.nvim/commit/1db3db3a5fb2494f7bdd56f2650acf9156d08305) -- if you (both) update, can you let me know whether you see what you're looking for now?

[Antoine Chambert-Loir]

Something gets printed but is almost immediately erased. Here is a video.
Enregistrement de l’écran 2026-01-18 à 23.34.04.mov

[Julian Berman]

Hrm, weird. I'll have a closer look here again.

[Christian Merten]

For me it fixed it, I am now seeing the old output. My guess would be that in @Antoine Chambert-Loir's example the reloading simply finishes too quickly.

[Julian Berman]

That or my other hypothesis is that Antoine's example has a separate sorry diagnostic, so that's the other thing I want to double check. But thanks for confirming for yours!

[Christian Merten]

Related to this: I used to see much more diagnostic information in the actual editor (similar to the VS Code error lens plugin). Since the update, I only see this in the infoview. How can I restore the old behaviour?

[Julian Berman]

Perhaps you're referring to Neovim changing its own default in 0.11 for virtual_text -- some detail here: https://neovim.io/doc/user/news-0.11.html#_diagnostics you can turn it back on again with the line that it shows there.

[Christian Merten]

Yes, that fixed it. Thank you for the quick fixes and pointers!

[Antoine Chambert-Loir]

I tried the new version on a more complicated file, and this looks very good! Thank you!

[Julian Berman]

Ah very good ok, glad to hear that "things were too fast" was part of the issue in the end :). Thanks for reporting.

[Kevin Buzzard]

I tried to create a video of the phenomenon but, because of the module system, I edited Mathlib.Init and then some random leaf file recompiled instantly :-)