lean.nvim

Stream: general

[Julian Berman]

Will mention a status update on the past few days of neovim support via lean.nvim in case it attracts anyone else who's following along :)

@Gabriel Ebner helped tidy up the infoview with some syntax highlighting, added support for showing diagnostics in it and made a more straightforward implementation of abbreviation insertion support, all of which are great.

We also fixed a couple of annoying basic bugs, though there are still a few to fix. At the minute I dare say things are quite usable to start.

@Rishikesh Vaishnav is working on per-window or per-tab infoviews which will make things much easier to work with with multiple splits and tabs. Rish let's maybe move our DMs here, in case it's interesting to anyone else (and if not they'll mute :P)

[Julian Berman]

Hopefully we'll also soon have a way to run lean 3 and lean 4 buffers side-by-side.

[Rish Vaishnav]

Hello folks! I am a graduate student from California who has been studying Lean for a few months but am relatively new to Zulip. Good to meet you all!

Per-tab/per-window infoviews are mostly ready (see this PR), there just are a few error messages not affecting functionality that I'm trying to work out, and we may want to add a few extra features. We've also got some design decisions to make on whether to make the lean vim filetype default to Lean 3 or Lean 4. It's currently dependent on a PR to nvim-lspconfig that adds Lean 4 as a new language server, so you'll have to install that fork if you want to try it out.

[Patrick Massot]

I'd love to use Lean in vim (although this will probably never be a serious option because of widgets). I'm super grateful that some people invest time in trying to make this happen. But I must say the README is daunting. The installation seem to require a lot of manual dependency installation and configuration, and it's not clear what is optional and what is required. Certainly the vim nightmare of having dozens of competing plugin managers doesn't help. Could you record some screencast showing the current status of this project? That would greatly help people deciding whether it's worth spending one hour installing it.

[Patrick Massot]

I should also write I think part of the mess comes from the Lean 3/Lean 4 dichotomy. It would probably help a lot to have separate instructions for Lean 3 and Lean 4.

[Julian Berman]

Yes that's good feedback thanks. I've been meaning to add a short demo, will do so, and make it a bit clearer what's necessary for what.

[Rish Vaishnav]

@Patrick Massot I was looking into how to support “true” http infoviews in neovim as well... I believe websockets are the technology we need to use? Which is available via the lua.http module. This could enable widgets. And for the very commonly used non-graphical widgets, it should be possible to port those directly for use in the terminal. Would be happy to look into this in the future

[Rish Vaishnav]

Made filetype lean refer to Lean 4 and lean3 refer to Lean 3, since we seem to agree that it is the right time for this. Adjusted nvim-lspconfig accordingly. Let me know if there are any objections.

[Rish Vaishnav]

@Gabriel Ebner It may be wise to also put a warning against using lean.vim if using neovim, and direct them to lean.nvim (in the lean.vim README)

[Rish Vaishnav]

Have fixed all of the bugs/error messages relating to the new infoview functionality I could find, NOTE that I've changed the config option lsp4 to lsp so that if we eventually stop supporting Lean 3 it won't be necessary to change that. Added to README descriptions of mappings for new infoview stuff.

TODO:

• Manually test abbreviations and completion from compe (may have been broken in lean3 by filetype rename)
• Manually test Treesitter
• Fix existing testing framework to work with the new infoview code
• README updating

[Julian Berman]

Nice, thanks! I think also things are getting big for one PR, so I'm going to try tearing off a piece and merging it independently if I can find some self-contained bits.

[Patrick Massot]

Rish Vaishnav said:

Patrick Massot I was looking into how to support “true” html infoviews in neovim as well... I believe websockets is the technology we need to use? Which is available via the lua-http library. This could enable widgets. And for the very commonly used non-graphical widgets, it should be possible to port those directly for use in the terminal. Would be happy to look into this in the future

I think you have it backward. There is no communication issue. I don't think there is any websockets involved, the Lean server simply sends widget information the same way it sends everything. But then all widgets are graphical. Displaying them is the issue. To be very specific, I'm not talking about toys such as the Hanoi towers widgets here, I'm talking about what you can see in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.22unfold.22.20a.20proposition/near/240804412 for instance. The big thing is being able to put your mouse on some expression in the info view and see how Lean parses them thanks to the interactive highlighting, and then copy or jump to definition.

[Daniel Fabian]

Also, @Julian Berman a screenshot or two of the final outcome often speaks more than a thousand words ;-)

[Rish Vaishnav]

Yeah, was considering adding a gif to the README of a demo using this, though we’ll probably have to update that once we implement pinnable/pausable infoview messages (at which point it would seem more competitive with VSCode)

[Ryan Lahfa]

As I prefer NeoVim and I do a lot of Lean 4 these days, I can be a beta tester if you want :)

[Rish Vaishnav]

That's awesome, all you have to do is install the forks of lean.nvim and nvim-lspconfig (replacing any existing installations). Here are zips of the minimal test packages I've been using: test_lean4.zip and test_lean.zip.

[Rish Vaishnav]

^ (also make sure you do NOT have lean.vim installed)

[Rish Vaishnav]

Alright, fixed the testing infra (though the automated github tests will fail until the nvim-lspconfig PR is merged), fixed a (hopefully last) edge case error message, and added some more details on the new functionality to the README.

This should be ready for a "final review" before merge @Julian Berman @Gabriel Ebner. And @Gabriel Ebner do you have any more comments on nvim-lspconfig? If it looks good to you then I'll go ahead and make the PR to upstream.

[Julian Berman]

Nice, well done. It's usually a bit easier to see what changes are being proposed in a PR -- I think the lspconfig change is probably correct at this point but it's slightly nontrivial to test because it has a circular dependency on the other change.

[Patrick Massot]

Rish Vaishnav said:

Gabriel Ebner It may be wise to also put a warning against using lean.vim if using neovim, and direct them to lean.nvim (in the lean.vim README)

The README of lean.nvim explicitly says one first needs to install lean.vim. This confirms people probably need to wait until the situation stabilizes.

[Julian Berman]

I think what we should possibly do, assuming we've agreed to call lean4 lean and Lean 3 lean3, is to make that filetype change immediately (in the lean.vim repo), which unblocks the change in the lspconfig repo.

[Julian Berman]

Yes Patrick give it a few days :)

[Patrick Massot]

Ok great. Thanks again for all your efforts!

[Julian Berman]

@Rish Vaishnav in general if we can it's much easier to review changes one small bit at a time rather than all bundled together with other ones, and also a bit easier if you work on a branch, rather than on the main branch, because then you can merge in upstream changes a bit easier -- but I'm trying not to bother much with that now, we can certainly work with what you have, it's great, will just take a bit to incrementally merge it.

[Rish Vaishnav]

Yeah my bad... I am a "baby" open source developer so definitely let me know if there are any best practices I'm not following!

[Julian Berman]

Yes I figured, you're doing great don't worry :) you did the important bit which is writing something nice. The rest is easy stuff.

[Julian Berman]

But yeah now we have basically the lspconfig change blocked on changing the lean filetypes, and then merging to lean.nvim blocked on the lspconfig change

[Julian Berman]

so we can do that in the lean.nvim repo or the lean.vim one (changing the filetype name) but I kind of would like to try to do it in the lean.vim repo assuming Gabriel is ok merging it -- there's a small chance we can make things still work together, so until that falls apart I kind of have hopes we'll be able to push through...

[Julian Berman]

@Rish Vaishnav am I being clear enough? Basically we have to introduce the new filetype names, so let's do that first, then you can send the lspconfig PR and it will work immediately, and then we can decide whether we really need to merge the two?

[Rish Vaishnav]

Hmm not 100% following, for lean.nvim I've already used filetype lean3 for Lean 3 and lean for Lean 4. We shouldn't need to change lean.vim (the new README says that you should not have lean.vim installed if using lean.nvim)

[Rish Vaishnav]

Oh I see, you're saying if they're using lean.vim instead of lean.nvim, then we need to add detection for the lean3 filetype in lean.vim, right?

[Julian Berman]

Right now what we have is that the PR to lean.nvim can't be merged because it depends on changes to lspconfig, but the converse is also true! lspconfig's PR can't be merged either because the only existing setup doesn't really use that filetype, not until I hit the merge button on your PR

[Julian Berman]

So things of course will work at the end of the day when everything's merged, but along the way, stuff will break

[Rish Vaishnav]

Gotcha. Does Github does not have some tool for synchronized merging?

[Julian Berman]

It doesn't, and in theory it wouldn't really be too big of an issue, it's not like we have 1000 users, we have essentially the 3 of us :P -- but I need to review the rest of the PR more carefully so I understand all the changes, so it's really me not being sure I can hit the merge button immediately

[Rish Vaishnav]

Yes totally understandable. Let me know if you have any questions, no rush at all!

[Rish Vaishnav]

Ok sorry but just pushed another small fix slightly refactoring close_win_wrapper (can't believe I missed this... :P)

[Rish Vaishnav]

Added a number of comments to the source (should hopefully make your review a bit easier)

[Rish Vaishnav]

2021-06-06-162302_1918x1079_scrot.png

This a bit much? :scream:

[Rish Vaishnav]

2021-06-06-162856_1917x1079_scrot.png

(after :LeanInfoPerTab) Ah that's better...

[Rish Vaishnav]

2021-06-06-165122_1916x1079_scrot.png

Or maybe, if you do things in the right order with :LeanInfoPerWin...

[Rish Vaishnav]

One more (small) thing I noticed - if you mess around with the infoview before the Language server has given diagnostics for your line, some ugly error messages about failed hover/plainGoal callbacks can be thrown. Again, doesn't "break" anything, but would be nice to fix, probably using something similar to what was done with wait_for_line_diagnostics() in the tester code. Though I will put this off to a future PR.

[Rish Vaishnav]

And also would be nice to include a "processing file..." message if it is waiting, similar to what is done in VSCode

[Julian Berman]

Yes definitely we should keep track of any known issues! But you may notice I'm trying to whittle down your branch little by little. So definitely in a second PR, or a future one :)

[Julian Berman]

My next whittling will be we already depend on lspconfig as a hard dep, so rather than vendoring the module from it with the path stuff, we should just be able to require it, right?

[Julian Berman]

If you have spare moments maybe give that a shot, since the US is about to wake up and I'm about to go on 6 hours of lovely Zoom calling...

[Rish Vaishnav]

Hmm currently I believe it is usable without nvim-lspconfig if they specifically set enable = false in lsp3 and lsp4, though it should be okay to require it since it would seem very rare to use this plugin without it

[Rish Vaishnav]

This should make it possible to remove all of that copied code in util.lua as well

[Gabriel Ebner]

Rish Vaishnav said:

This should be ready for a "final review" before merge Julian Berman Gabriel Ebner. And Gabriel Ebner do you have any more comments on nvim-lspconfig? If it looks good to you then I'll go ahead and make the PR to upstream.

The lspconfig stuff looks good to me, at least Lean-wise.

[Rish Vaishnav]

Cool, I'll make that PR once we've "finalized" things on our side so that we can make sure the merges happen at somewhat the same time

[Julian Berman]

No no make the PR immediately, that'll actually help!

[Julian Berman]

It'll save you from having to do what we just discussed I think.

[Rish Vaishnav]

Oh I see, alright will do

[Rish Vaishnav]

It is open: https://github.com/neovim/nvim-lspconfig/pull/958

[Rish Vaishnav]

Yeah, my bad in including unrelated fixes (e.g. buffer-local keymappings) in my PR rather than creating a new PR for them, will be more careful about this in the future. Looking at my other commits, everything else should be self-contained (though I really should have made simultaneous support and per-window/per-tab infoviews two separate PRs)

[Rish Vaishnav]

Also feel free to remove to mode-toggling mappings by the way... I agree that it should be pretty rare to use, so the :LeanInfoPerTab and :LeanInfoPerWin commands should be enough. I just got a bit too excited there once I got this working lol

[Julian Berman]

All good, don't worry, yeah it's 100x easier to review 10 small PRs that do one thing each than 1 big one essentially, so in general the smaller you can make them the better. And yeah think I'll kill those two commands until someone asks for them.

[Julian Berman]

The excitement is good though :P it'll keep you motivated to help, which I could use all I can get.

[Rish Vaishnav]

Yeah also for the :LeanInfoPerTab and :LeanInfoPerWin commands feel free to remove them as well... Though I already personally find them very useful as I frequently switch between my desktop RPi (large screen) and connecting to it via SSH over my laptop (small screen), and dynamically being able to change that makes it possible for me not to have to modify init.vim/init.lua and restart neovim - so I think it's worth mentioning in the README how to set those commands up in the lsp/lsp3 configs

[Rish Vaishnav]

One more thing to put on the roadmap: individually configurable NESW infoviews - I'd imagine, for example when viewing Lean 3 files and Lean 4 files side by side, it would be pretty convenient to have the infoview on the bottom of each source window rather than always on the right. Shouldn't be too much trouble to implement

[Gabriel Ebner]

Rish Vaishnav said:

One more thing to put on the roadmap: individually configurable NESW infoviews - I'd imagine, for example when viewing Lean 3 files and Lean 4 files side by side, it would be pretty convenient to have the infoview on the bottom of each source window rather than always on the right. Shouldn't be too much trouble to implement

This is also useful for portrait screens.

[Rish Vaishnav]

Trying out the new term goals - any idea what's causing exit-code 82 with leanpkg print-paths on the latest nightly (06/09)?

https://asciinema.org/a/2UsJIWjPAFA1ZM4waDx0LpWG0

[Gabriel Ebner]

This is an interesting error, and I can't reproduce it. You're on arm, right?

[Rish Vaishnav]

Yep. I’m going to try some of the previous nightlies and see if I can find where it first show up

[Sebastian Ullrich]

I would bet on https://github.com/leanprover/lean4/pull/495 :)

[Sebastian Ullrich]

No idea either though

[Rish Vaishnav]

Thanks. Don't have the knowledge yet to solve this, so swallowing my pride for now and moving to an x86 machine :grimacing:

[Rish Vaishnav]

Update: the next feature I'm going to implement is pinnable/pausable infoview messages, starting from my infoview_persistence_refactor branch. But before that, I'm going to focus for a bit on adding complete automated testing for per-window/per-tab infoviews to make things easier down the road.

[Julian Berman]

That sounds great, definitely please do send small, single-purpose PRs for that as you go. But more tests would be awesome.

[Rish Vaishnav]

@Julian Berman To save you some time, we can abandon the current PR # 35 and I can work on introducing incremental PRs for the new functionality (along with ones for new unit tests). But if you think you've "almost got it" with # 35, we can go ahead with that. Let me know what you prefer.

[Julian Berman]

@Rish Vaishnav if you don't hold it against me that'd be 100% helpful

[Julian Berman]

I am almost at the point where I can cross off another piece of functionalitiy, but after that would still have a bit of work for each of the remaining bits, so yeah if you're OK with that it'd deeeefinitely help.

[Rish Vaishnav]

Yes no problem at all - figuring out how to best separate things is half the fun anyways!

[Rish Vaishnav]

@Gabriel Ebner FYI: We've just internalized all of the components from lean.vim into lean.nvim - not sure what the plan for lean.vim is from here, whether to archive or support in parallel. IMO probably best to support in parallel at least until neovim 0.5.0 is officially released, but let me know your thoughts on this.

[Gabriel Ebner]

I'll leave lean.vim as it is for now, though maybe we should make the link to lean.nvim more prominent. Future changes to the syntax files will go to lean.nvim.

[Julian Berman]

There's now a short demo in the README: https://github.com/Julian/lean.nvim/#leannvim

There still is not a Patrick-proof (i.e. "just tell me to run one command and then everything works without reading 8 paragraphs") section, and Lean 3 functionality lags a bit behind Lean 4. Both of those are things I'll address in the next week or so, but the demo video hopefully gives an initial idea of where things are. Comments are of course welcome.

[Johan Commelin]

Great, that demo video looks really promising!!

[Rish Vaishnav]

@Julian Berman the language servers seem to be broken in CI, even for commits before the most recent merge. Could recent changes to lean-language-server be responsible? Do the yml files need to be updated in some way? Looking into it…

[Rish Vaishnav]

Locally, after updating lean-language-server, I get:

[local] lean.nvim $ lean-language-server --stdio
/usr/local/bin/lean-language-server: line 1: use strict: command not found
/usr/local/bin/lean-language-server: line 2: syntax error near unexpected token `exports,'
/usr/local/bin/lean-language-server: line 2: `Object.defineProperty(exports, "__esModule", { value: true });'

[Julian Berman]

Sorry, should have mentioned that somewhere you'd see -- it's related to me breaking that somehow, but I don't know how, I didn't touch anywhere near that, so I can only assume something changed in tsc's behavior maybe or something, I have to investigate (and had to jump on calls). https://github.com/leanprover/lean-client-js/pull/21#issuecomment-867688593

[Rish Vaishnav]

Alright no prob, I'll look into it as well

[Gabriel Ebner]

I've pushed a fix now.

[Gabriel Ebner]

The whole lean-client-js project hasn't been touched for years. It seems impossible to upgrade everything to the latest typescript version, but upgrading lean-language-server worked just fine and fixed the bug.

[Rish Vaishnav]

Awesome, looks like that fixed it. Thank you!

[Julian Berman]

Thanks to Rish and Gabriel, lean.nvim just merged support for... widgets :) -- both for lean 3 and 4.

If you were waiting for support for them to decide whether neovim was worth a shot, now's your chance. Let us know what you think. We're still merging a few tweaks to how things look (and documenting the mappings), but the core functionality is indeed there now.

[Johan Commelin]

Wow, that's really cool!

[Johan Commelin]

How do I test this?

[Patrick Massot]

I can't even imagine how it could look like :open_mouth:

[Patrick Massot]

Did you already update the documentation?

[Julian Berman]

I'll post a recording a bit later after the tweaks are in -- and no, still working on tweaking the docs, so this is an early sneak peak (but hey who can resist such things). For now if you have the plugin installed -- howto is here, let me know if anything is unclear -- the mappings you'll use are here -- but more docs to come later tonight if you're less adventurous (or have less time).

[Patrick Massot]

I can definitely wait. Thank you so much for all this!

[Julian Berman]

In this case I didn't do much myself, just the messenger trying to rile up more feedback :), but indeed the others did quite a nice job.

[Julian Berman]

Here's a brief screen recording of what it looks like at the minute -- https://user-images.githubusercontent.com/329822/136033121-4656e399-b422-4404-9e6c-526dffe91419.mov

[Johan Commelin]

That looks very exciting!

[Johan Commelin]

If installing this is reasonably easy, I am very interested in trying this out.

[Julian Berman]

I believe at this point it should be, and of course am happy to help if not (either by improving docs or otherwise) -- have you got the plugin installed? Or if not, can I help somehow there? What step are you at?

[Johan Commelin]

I'm at step 0.

[Johan Commelin]

Can I install the plugin using usual methods?

[Julian Berman]

Cool :)

[Julian Berman]

Yes -- any plugin manager should work, we include instructions for vim-plug specifically here: https://github.com/Julian/lean.nvim/#installation

[Julian Berman]

@Rish Vaishnav also deserves another shout out for the (massively cool) effort on getting the above to work.

[Rish Vaishnav]

Thanks :blush: Though there is certainly still a lot more cool stuff I plan to add very soon!!!

[Johan Commelin]

@Julian Berman Plug 'andrewradev/switch.vim' " For Lean switch support
What does that do?

[Johan Commelin]

aah, it's some generic plugin for syntax transformations?

[Johan Commelin]

Yet another thing to try out

[Julian Berman]

@Johan Commelin Yes :) in my opinion it's literally the most useful under-known vim plugin

[Julian Berman]

Amongst the few of us using lean.nvim however, I suspect only I've used the lean support I wrote

[Julian Berman]

And since I know so little lean, it undoubtedly could use improvement in what it switches between

[Julian Berman]

But what it does right now is e.g. if you have library_search under the cursor and hit switch, it'll change that to suggest, and if you hit it again to hint I think

[Julian Berman]

Or if you have tt under the cursor you get ff

[Johan Commelin]

simp -> squeeze_simp??

[Julian Berman]

The full set of switches are here: https://github.com/Julian/lean.nvim/blob/main/ftplugin/lean/switch.vim#L8-L35 and as I say I fully expected someone who knows more lean to at some point come along and suggest better versions of that

[Julian Berman]

yep though actually I think I made it use your simp?, but when I saw you say squeeze_simp was still a bit better at things I made a mental note to go back to squeeze_simp which I may not have pushed done

[Julian Berman]

Uh sorry I linked you the lean 4 version

[Julian Berman]

The lean 3 one (which has tactic switches) is here: https://github.com/Julian/lean.nvim/blob/27817399adcf871075337cb2b7d1e773e7e5c55e/ftplugin/lean3/switch.vim

[Alex J. Best]

Any tips for following nested widgets? The only way I managed to go more than one level deep is with :set mouse=a as ctrl-w w seems to fail me after one widget

[Julian Berman]

Hit Tab

[Alex J. Best]

Hm, it doesn't seem to do anything for me unfortunately

[Julian Berman]

I added that an hour or two ago

[Julian Berman]

So update if you haven't since then perhaps

[Alex J. Best]

Perfect, thank you all for this :smile:

[Patrick Massot]

Installing the suggested packages results in an endless stream of errors like: E5108: Error executing lua ...sot/.config/nvim/bundle/nvim-compe/lua/compe/context.lua:20: attempt to index field 'b' (a nil value)

[Julian Berman]

@Patrick Massot can you share what version of neovim you're on? Via e.g. nvim --version.

[Patrick Massot]

and Error executing vim.schedule lua callback: ...sot/.config/nvim/bundle/plenary.nvim/lua/plenary/job.lua:480: attempt to call field 'wait' (a nil value)

[Patrick Massot]

NVIM v0.5.0-353-g3051342f9
Build type: RelWithDebInfo
LuaJIT 2.1.0-beta3
Compilation: /usr/bin/gcc-5 -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=1 -O2 -g -Og -g -Wall -Wextra -pedantic -Wno-unused-parameter -Wstrict-prototypes -std=gnu99 -Wshadow -Wconversion -Wmissing-prototypes -Wvla -fstack-protector-strong -fdiagnostics-color=auto -DINCLUDE_GENERATED_DECLARATIONS -D_GNU_SOURCE -DNVIM_MSGPACK_HAS_FLOAT32 -DNVIM_UNIBI_HAS_VAR_FROM -DMIN_LOG_LEVEL=3 -I/home/travis/build/neovim/bot-ci/build/neovim/build/config -I/home/travis/build/neovim/bot-ci/build/neovim/src -I/home/travis/build/neovim/bot-ci/build/neovim/.deps/usr/include -I/usr/include -I/home/travis/build/neovim/bot-ci/build/neovim/build/src/nvim/auto -I/home/travis/build/neovim/bot-ci/build/neovim/build/include
Compilé par travis@travis-job-403476e6-991c-4366-b1c7-4e5a12a1aed5

Features: +acl +iconv +tui

[Patrick Massot]

My vim is now completely unusable, even for non lean files

[Julian Berman]

Hm, odd, sorry -- I suppose 2 things to try if you don't mind, one is can you give a shot at neovim 0.5.1? You can get a quick download of it here https://github.com/neovim/neovim/releases/tag/v0.5.1 if you're comfortable trying that, though it's weird because the first error message is basically saying :lua print(vim.wait) doesn't work (so if you can try that and tell me if that works that may help too

[Julian Berman]

But I know Gabriel was successfully using 0.5.0 up until like 2 days ago

[Patrick Massot]

Maybe I misunderstand the instructions. For instance I'm not sure where I'm meant to write

-- You may want to reference the nvim-lspconfig documentation, found at:
-- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
-- The below is just a simple initial set of mappings.
local function on_attach(client, bufnr) {
    local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end
    local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end
    buf_set_keymap('n', 'gd', '<Cmd>lua vim.lsp.buf.definition()<CR>', {noremap = true})
    buf_set_keymap('n', 'K', '<Cmd>lua vim.lsp.buf.hover()<CR>', {noremap = true})
    buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc')
}

[Julian Berman]

One sec, I'll give you a full gist

[Patrick Massot]

:lua print(vim.wait) answers nil

[Patrick Massot]

Note that I never used any lua for anything

[Julian Berman]

Hm, yeah that shouldn't matter, for neovim it's part of neovim -- you're on debian I guess?

[Julian Berman]

If you type :version inside neovim do you get something similar to that output?

[Patrick Massot]

With the newer nvim I get a new error message E5112: Error while creating lua chunk: /home/pmassot/.config/nvim/plugin/lean.lua:4: unexpected symbol near '{'

[Patrick Massot]

line 4 is local function on_attach(client, bufnr) {

[Patrick Massot]

:version
NVIM v0.5.1
Build type: RelWithDebInfo
LuaJIT 2.1.0-beta3

[Julian Berman]

Oh. And that line is telling me that indeed I put invalid lua in the README so apologies.. One second I'm on a call but I'll give you the right thing

[Patrick Massot]

There is no hurry at all. I'll take care of my son for a while.

[Julian Berman]

Put this in ~/.config/nvim/plugin/lean.lua: https://gist.github.com/Julian/5ddb85a86f4295491546832b25fc2011

(And let me know if that at least makes the errors go away)

[Patrick Massot]

I can now use vim normally!

[Patrick Massot]

Let me try some Lean then

[Patrick Massot]

I see the info view! :octopus:

[Julian Berman]

Hooray! Yeah feel free to ask anything else if you start playing around. What I just gave you doesn't do everything you may want (out of vim) -- lean.nvim is somewhat intentionally less opinionated (or simple?) than the vscode plugin so there's more room to customize things (or use plugins in the neovim ecosystem), but if you don't do so already yourself obviously ask and happy to help (especially if it's missing functionality we should add). So yeah in short tear us apart :D

[Patrick Massot]

This is so amazing that I'm laughing with joy in front of my computer

[Adam Topaz]

Uh oh... should I be concerned that I will need to switch back to vim now?

[Julian Berman]

Well that certainly makes my day. Again credit to the other folks though, I'm just the guy who was stubborn enough to ignore you when you said Lean doesn't have a vim story :D

[Julian Berman]

But @Gabriel Ebner and @Rish Vaishnav have both contributed a ton I would have never been able to do, so it was a true team effort.

[Patrick Massot]

How to you see where errors are? What about the orange bars?

[Gabriel Ebner]

What about the orange bars?

Fixed. They used to work in Lean 3 as well, but from what I can tell this was broken after merging the widgets branch.

[Gabriel Ebner]

Patrick Massot said:

How to you see where errors are?

You might need to set the colors manually (if your colorscheme doesn't support it yet):

hi LspReferenceRead cterm=bold ctermbg=red guibg=LightYellow
hi LspReferenceText cterm=bold ctermbg=red guibg=LightYellow
hi LspReferenceWrite cterm=bold ctermbg=red guibg=LightYellow
hi LspDiagnosticsDefaultError cterm=bold ctermfg=Red
hi LspDiagnosticsDefaultWarning cterm=bold ctermfg=Yellow
hi LspDiagnosticsDefaultInformation ctermfg=Blue
hi LspDiagnosticsUnderlineError gui=undercurl
hi LspDiagnosticsUnderlineWarning gui=undercurl
hi LspDiagnosticsUnderlineInformation gui=undercurl
hi LspDiagnosticsUnderlineHint gui=undercurl
hi link SpecialChar Character

You might also need to enable the squiggles manually (not sure if this is the default or not):

:lua <<EOF
vim.lsp.handlers["textDocument/publishDiagnostics"] = vim.lsp.with(
  vim.lsp.diagnostic.on_publish_diagnostics, {
    underline = true,
    virtual_text = { spacing = 4 },
    update_in_insert = true,
  })
EOF

[Patrick Massot]

I can confirm the orange "bars" are there. However they make the left margin randomly jump (as do thet #check and #print commands) which is really really not nice. Is there any way to avoid that?

[Patrick Massot]

Maybe we could permanently reserve horizontal space for them?

[Patrick Massot]

I'm not sure what you call red squiggles. I think I don't see them. I pasted you lua code at the end of my plugin/lean.lua

[Patrick Massot]

By the way, in case we still have a couple of VScode users, I recently found the "Error lens" extension which makes errors much easier to spot.

[Julian Berman]

You can permanently reserve space using... I think :set signcolumn=yes (or vim.opt.signcolumn = "yes" from your lua file)

[Julian Berman]

The default is "auto".

[Julian Berman]

Also beyond what Gabriel shared you probably want some navigation to move between errors (at least I like that a lot)

[Julian Berman]

This is what I use (the first and last line of this, though perhaps the whole thing is of interest): https://github.com/Julian/dotfiles/blob/main/.config/nvim/plugin/lsp.lua#L21-L25

[Julian Berman]

So when I hit <space>n it goes to the next lean line with an error on it.

[Julian Berman]

And <space>N goes to the previous one.

[Julian Berman]

If you want to copy paste those lines just note you'll need to copy paste these too: https://github.com/Julian/dotfiles/blob/main/.config/nvim/plugin/lsp.lua#L4-L12

[Patrick Massot]

Julian, can you show what "red squiggles" are meant to look like?

[Julian Berman]

I have them turned off, ha, but yeah gimme a sec

[Julian Berman]

They're meant to look quite similar to VSCode where the actual text has a curly line underneath it in your lean file

[Julian Berman]

Are you in terminal neovim or graphical?

[Patrick Massot]

That's what I thought. I don't see them

[Patrick Massot]

I'm in a terminal

[Julian Berman]

This is what it should look like, albeit this is Lean 4: Screen-Shot-2021-10-05-at-16.12.13.png

[Julian Berman]

That's in a terminal (I use terminal neovim too)

[Patrick Massot]

I don't have this :sad:

[Julian Berman]

I think there's 2 things that might be preventing you from seeing them -- one is I think Lean 3 support for us still doesn't have them, but Gabriel correct me if I'm wrong

[Julian Berman]

I think there there's an open issue: https://github.com/Julian/lean.nvim/issues/97

[Patrick Massot]

I'm talking only about Lean 3

[Julian Berman]

But we need to fix it in Lean 3's server

[Julian Berman]

Yeah so I think you won't see them

[Patrick Massot]

Ok, that's not a big deal

[Julian Berman]

(The other one is if your $TERM is misset, but yeah I think for Lean 3 they don't work AFAIK -- as I say I usually leave them off personally, I find them a bit noisy)

[Patrick Massot]

How do you click the "Try this" links?

[Patrick Massot]

Oops, it's in the doc

[Julian Berman]

Support for try this is a bit wonky, I wrote it very early on -- but right now you can hit <LocalLeader>t (from the Lean source file) to replace the first one

[Patrick Massot]

It doesn't replace the correct thing

[Julian Berman]

Yeah, sometimes the parsing is wrong though so if it starts to annoy you (as it often annoys me), complain :) and I'll try to make time to make it better.

[Julian Berman]

Right, sorry :/

[Patrick Massot]

I had a squeeze_simp at this and it kept the at this (which became duplicated)

[Julian Berman]

in those cases I do the hacky thing, I just go into the infoview window, yank the right thing, and replace, and then curse at the bad parsing code

[Julian Berman]

(The vscode extension has some heuristics which essentially are what's needed to port to Lua)

[Patrick Massot]

Do you sometimes see Error executing vim.schedule lua callback: ...t_nvimHd0Pv1/usr/share/nvim/runtime/lua/vim/lsp/util.lua:1052: Failed to switch to buffer 26 when trying to jump to definition?

[Julian Berman]

I haven't seen that error personally -- how often does it happen? I take it not every time?

[Patrick Massot]

I'm currently in a state where it happens every time

[Patrick Massot]

restarting vim fixed it

[Julian Berman]

OK -- https://github.com/neovim/neovim/pull/12262 possibly looks like the most relevant issue

[Julian Berman]

But if it happens again I guess we can see what to do about it

[Sebastien Gouezel]

Patrick Massot said:

By the way, in case we still have a couple of VScode users, I recently found the "Error lens" extension which makes errors much easier to spot.

Very nice, thanks for mentioning this!

[Patrick Massot]

But now you should switch to vim

[Sebastien Gouezel]

You know that I'm on windows, right? How could you imagine I would switch to vim? :-)

[Patrick Massot]

It's never too late to redeem

[Sebastien Gouezel]

But I already redeemed, removing my double boot Ubuntu/Windows and switching back fulltime to Windows.

[Yakov Pechersky]

Ah, but there is WSL to bring you back to linux

[Johan Commelin]

@Julian Berman @Gabriel Ebner @Rish Vaishnav Thank you so much for all your efforts! This seems to be working very nicely.

[Johan Commelin]

My next job will be to figure out how to do LSP stuff. (E.g., gd doesn't do go-to-definition for me, atm.)

[Johan Commelin]

But that should be orthogonal to the lean plugin, right?

[Gabriel Ebner]

I think you need to set up your own mappings:

nnoremap gD <Cmd>lua vim.lsp.buf.declaration()<CR>
nnoremap gd <Cmd>lua vim.lsp.buf.definition()<CR>
nnoremap K <Cmd>lua vim.lsp.buf.hover()<CR>
nnoremap <leader>K <cmd>lua vim.lsp.diagnostic.show_line_diagnostics{show_header = false}<CR>
nnoremap gi <cmd>lua vim.lsp.buf.implementation()<CR>
nnoremap <C-k> <cmd>lua vim.lsp.buf.signature_help()<CR>
nnoremap <space>wa <cmd>lua vim.lsp.buf.add_workspace_folder()<CR>
nnoremap <space>wr <cmd>lua vim.lsp.buf.remove_workspace_folder()<CR>
nnoremap <space>wl <cmd>lua print(vim.inspect(vim.lsp.buf.list_workspace_folders()))<CR>
nnoremap <space>D <cmd>lua vim.lsp.buf.type_definition()<CR>
nnoremap <space>rn <cmd>lua vim.lsp.buf.rename()<CR>
nnoremap <space>ca <cmd>lua vim.lsp.buf.code_action()<CR>
nnoremap gr <cmd>lua vim.lsp.buf.references()<CR>
nnoremap <space>e <cmd>lua vim.lsp.diagnostic.show_line_diagnostics()<CR>
nnoremap [d <cmd>lua vim.lsp.diagnostic.goto_prev()<CR>
nnoremap ]d <cmd>lua vim.lsp.diagnostic.goto_next()<CR>
nnoremap <space>q <cmd>lua vim.lsp.diagnostic.set_loclist()<CR>
nnoremap <space>f <cmd>lua vim.lsp.buf.formatting()<CR>

[Patrick Massot]

I should have taken notes yesterday but I think it's not too late. When I'll be back home I'll try to precisely write down everything I did to make it work.

[Johan Commelin]

Thanks, I'll also play around some more.

[Julian Berman]

@Patrick Massot that would be super helpful of course. Feel free to stick them in the wiki perhaps too, which right now only has one page: https://github.com/Julian/lean.nvim/wiki/Configuring-&-Extending

[Johan Commelin]

What is the idiomatic way to close the hover popups?

[Rish Vaishnav]

<c-w>-c should work for now, though we plan to add a mapping for this

[Johan Commelin]

:q also worked, but it seemed a bit barbaric

[Rish Vaishnav]

Also note that this won’t work well (and neither will :q) if you try it two or more times in a row in nested tooltips, since it could plop you in any window at that point. I’ve been using the experimental hop.nvim integration recently so just noticed this myself.

So yeah a mapping to properly exit tooltips is certainly much needed…

[Rish Vaishnav]

In the meantime perhaps your best bet for lean 3 is probably just to use the “x” button

[Rish Vaishnav]

@Johan Commelin Just pushed, Shift-Tab should now do it for ya

[Julian Berman]

Oh. I was going to make Shift+Tab move backwards through tooltips.

[Rish Vaishnav]

Yeah I think that's what this does? It doesn't actually close it, just moves you to its parent.

[Julian Berman]

Aha, ok lemme give it a shot myself then, cool.

[Patrick Massot]

My notes about what I did yesterday:

nvim

Install a recent nvim by going to https://github.com/neovim/neovim/releases
download nvim.appimage (version 0.5.1) put it somewhere where my shell can
find it and make it executable.

node Lean server

Install Node + npm and the node package lean-language-server

I use https://github.com/nvm-sh/nvm to manage node version so I could simply run

npm install -g lean-language-server

vim plugins

I use https://github.com/tpope/vim-pathogen to manage my vim packages so
I went to $HOME/.config/nvim/bundle/ and ran

• git clone https://github.com/hrsh7th/nvim-compe.git
• git clone https://github.com/nvim-lua/plenary.nvim.git
• git clone https://github.com/neovim/nvim-lspconfig.git
• git clone https://github.com/Julian/lean.nvim.git

Configuration files

$HOME/.config/nvim/plugin/, create a file lean.lua containing

vim.opt.completeopt = { 'menuone', 'noselect' }

require'compe'.setup{
  autocomplete = false,
  source = {
    nvim_lsp = { priority = 99 },
    nvim_lua = { priority = 99 },
    path = { priority = 99 },
  }
}

-- You may want to reference the nvim-lspconfig documentation, found at:
-- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
-- The below is just a simple initial set of mappings.
local function on_attach(_, bufnr)
    local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end
    local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end
    local function cmd(mode, key, cmd)
    vim.api.nvim_buf_set_keymap(
      bufnr,
      mode,
      key,
      '<cmd>lua ' .. cmd .. '<CR>',
      {noremap = true}
    )
      end
    buf_set_keymap('n', 'gd', '<Cmd>lua vim.lsp.buf.definition()<CR>', {noremap = true})
    buf_set_keymap('n', 'K', '<Cmd>lua vim.lsp.buf.hover()<CR>', {noremap = true})
    buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc')

    cmd('n', '<leader>n', 'vim.lsp.diagnostic.goto_next{popup_opts = {show_header = false}}')
    cmd('n', '<leader>q', 'vim.lsp.diagnostic.set_loclist()')
    cmd('n', '<leader>r', 'vim.lsp.buf.rename()')
    cmd('n', '<leader>K', 'vim.lsp.diagnostic.show_line_diagnostics{show_header = false}')
    cmd('n', '<leader>N', 'vim.lsp.diagnostic.goto_prev{popup_opts = {show_header = false}}')
end

require('lean').setup{
    abbreviations = { builtin = true },
    lsp = { on_attach = on_attach },
    lsp3 = { on_attach = on_attach },
    mappings = true,
}

vim.lsp.handlers["textDocument/publishDiagnostics"] = vim.lsp.with(
  vim.lsp.diagnostic.on_publish_diagnostics, {
    underline = true,
    virtual_text = { spacing = 4 },
    update_in_insert = true,
  })

in $HOME/.config/nvim/after/ftplugin/, create lean3.vim containing

hi LspReferenceRead cterm=bold ctermbg=red guibg=LightYellow
hi LspReferenceText cterm=bold ctermbg=red guibg=LightYellow
hi LspReferenceWrite cterm=bold ctermbg=red guibg=LightYellow
hi LspDiagnosticsDefaultError cterm=bold ctermfg=Red
hi LspDiagnosticsDefaultWarning cterm=bold ctermfg=Yellow
hi LspDiagnosticsDefaultInformation ctermfg=Blue
hi LspDiagnosticsUnderlineError gui=undercurl
hi LspDiagnosticsUnderlineWarning gui=undercurl
hi LspDiagnosticsUnderlineInformation gui=undercurl
hi LspDiagnosticsUnderlineHint gui=undercurl
hi link SpecialChar Character

set signcolumn=yes

[Patrick Massot]

Julian, feel free to steal any of this for your documentation (or tell me I messed up).

[Patrick Massot]

Patrick Massot said:

Do you sometimes see Error executing vim.schedule lua callback: ...t_nvimHd0Pv1/usr/share/nvim/runtime/lua/vim/lsp/util.lua:1052: Failed to switch to buffer 26 when trying to jump to definition?

I found a way to reproduce with 100% failure: ask to lint a file and then try to go to definition:
bug_gd.gif

[Patrick Massot]

It would be nice to have markdown syntax highlighting in comments

[Patrick Massot]

How do you restart the lean server when it goes crazy?

[Patrick Massot]

And when it dies I see (node:581156) UnhandledPromiseRejectionWarning: server is not alive but don't get the option to restart it

[Patrick Massot]

The linting trick is far from being the only way to trigger the jump to bug, it happens really really often

[Julian Berman]

Thanks Patrick. At first glance definitely nothing messed up in it!

Patrick Massot said:

How do you restart the lean server when it goes crazy?

:LspRestart should work I believe. (or sometimes :e to just re-edit the current file).

Patrick Massot said:

It would be nice to have markdown syntax highlighting in comments

We had this and disabled it, I forgot why -- maybe just while we were decommisioning the old lean.vim plugin. I'll have to remind myself.

Patrick Massot said:

The linting trick is far from being the only way to trigger the jump to bug, it happens really really often

Does that lint trick work in any file? I notice the one you're showing is some local changes right? When I try that on my machine in the version from the mathlib repo I can't reproduce :( even if I switch to using 0.5.0 (normally I use nightly), but we can try staring at the code to see what's happening, I don't have ideas yet.

[Patrick Massot]

Yes, I was obviously editing a file. I'll try on master

[Patrick Massot]

Yes, it works on master

[Patrick Massot]

I mean the bug is there on master

[Julian Berman]

OK, that's "good" in some sense, though I can't reproduce here on that file, it works fine on my machine -- let me see what to do about debugging, unless someone else either can reproduce or has an idea.

[Patrick Massot]

:version
NVIM v0.5.1
Build type: RelWithDebInfo
LuaJIT 2.1.0-beta3
Compilation: /usr/bin/gcc-11 -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=1 -DNVIM_TS_HAS_SET_MATCH_LIMIT -O2 -g -Og -g -Wall -Wextra -pedantic -Wno-unused-parameter -Wstrict-prototypes -std=gnu99 -Wshadow -Wconversion -
Wmissing-prototypes -Wimplicit-fallthrough -Wvla -fstack-protector-strong -fno-common -fdiagnostics-color=always -DINCLUDE_GENERATED_DECLARATIONS -D_GNU_SOURCE -DNVIM_MSGPACK_HAS_FLOAT32 -DNVIM_UNIBI_HAS_VAR_FRO
M -DMIN_LOG_LEVEL=3 -I/home/runner/work/neovim/neovim/build/config -I/home/runner/work/neovim/neovim/src -I/home/runner/work/neovim/neovim/.deps/usr/include -I/usr/include -I/home/runner/work/neovim/neovim/build
/src/nvim/auto -I/home/runner/work/neovim/neovim/build/include
Compilé par runner@fv-az87-829

Features: +acl +iconv +tui

[Julian Berman]

(Also reenabling markdown syntax seems to make neovim segfault ugh. So that probably is the reason why we disabled it. I doubt we looked at why that's happening in too much detail though.)

[Gabriel Ebner]

It would be nice to have markdown syntax highlighting in comments
We had this and disabled it, I forgot why -- maybe just while we were decommisioning the old lean.vim plugin. I'll have to remind myself.

I removed it intentionally. We got lots of highlighting errors where the markdown syntax extended beyond the end of the comment. My plan is to copy a small and hopefully safe set of highlighting rules from the markdown syntax file. I just haven't gotten around to it yet.
(We have to do the same thing in the vscode extension. If we use the default vscode markdown highlighting, then some markdown highlighting extends beyond the end of the comment, even more than it does now. So we have a custom copy of the markdown syntax in the vscode extension where half of the rules are disabled.)

[Julian Berman]

Ah.. fair enough, sounds good.

[Julian Berman]

Patrick given I don't have a better idea for the minute but found another vaguely similar bug report, can you perhaps confirm whether you still see the issue on nightly? You can find an appimage of it at the bottom of the page here: https://github.com/neovim/neovim/actions/runs/1310512839

[Patrick Massot]

At least the lint trick no longer triggers the bug!

[Julian Berman]

OK yeah I'm somewhat suspicious it's an 0.5 race condition... perhaps that will hold you off at least for a few days using the nightly and seeing whether you can get it to happen there too.

[Patrick Massot]

I don't mind using the nightly, I put it in place of the 0.5.1 version that I downloaded yesterday

[Julian Berman]

Great!

[Anne Baanen]

This is really cool! I'd like to make one bug report though: when tab-expanding backslash abbreviations the cursor doesn't go to the end of a sequence of bytes. For example: \ + < + TAB results in my cursor ending up in the middle of the ⟨, and continuing to type produces garbage like 鿢ꡡ (that is <e2><9f>a<a8>, apparently)

[Anne Baanen]

However, the issue is not a big deal to me and I'll probably switch (back) from to soon :D

[Julian Berman]

First, hooray! Thanks, glad you're enjoying. The bug report is unfortunately known, I tried to fix it and failed (even though I kind of partially fixed it) -- https://github.com/Julian/lean.nvim/issues/89

[Julian Berman]

I can try to give it another shot sometime soon but I'm still half-underwater with non-lean-related work so I don't know it'll be "immediately". But I know the cause, it's annoying differences in unicode-using APIs and screen-character using APIs.

[Julian Berman]

The other workaround by the way is to not hit tab -- which my fingers really hate so it doesn't really work for me, but if you manage to just keep typing and not manually expand the expansion and let it autoexpand, your cursor position should be OK.

[Julian Berman]

Patrick by the way I put your notes with only small modifications here: https://github.com/Julian/lean.nvim/wiki/Getting-Started and we probably can use that as a place to put some more improvement suggestions.

[Anders Christiansen Sørby]

I'm trying to set up lean.nvim using nix home-manager. It is not added to nixpkgs yet which means I need to set it up myself.

[Julian Berman]

I don't use home-manager, though I know others do -- but if you either need a change to the repo to support that setup or have done so yourself and can contribute it it'd definitely be welcome.

[Julian Berman]

GitHub copilot support for neovim landed an early version today -- https://github.com/github/copilot.vim -- I didn't bother personally signing up for Copilot yet, but if anyone else did, do let me know if you try it out with lean.nvim (the two wouldn't really interact I suspect, so behavior should be roughly the same as using Copilot in VSCode)

[Julian Berman]

There's also tabnine support here -- https://github.com/tzachar/cmp-tabnine which I also have not yet tried with Lean, but should also work the same as in VSCode.

[Antoine Chambert-Loir]

I followed what @Patrick Massot indicated,
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lean.2Envim/near/256457660, with the following variations.

nvim. I use https://brew.sh/ on MacOS, hence just add to type brew install nvim.

npm. I

brew install npm
npm install -g lean-language-server

[Julian Berman]

brew install lua shouldn't be necessary

[Julian Berman]

I put a version of Patrick's notes here: https://github.com/Julian/lean.nvim/wiki/Getting-Started -- but let me modify it for macOS as well quickly done

[Julian Berman]

Can you have a look at that perhaps and tell me if what's there helps you get started? Or if not please do feel free to modify anything there (or keep putting it here and I'll do so!)

[Julian Berman]

I can see perhaps @Antoine Chambert-Loir that you may be having issues because you may have put those things in ~/.vim instead of ~/.config/nvim which is where neovim files generally go, but not sure if that was a typo perhaps

[Antoine Chambert-Loir]

Thanks @Julian Berman for looking it up. Everything was in ~/.nvim except for pathogen.vim which was in ~/.vim/autoload, but I pushed it in ~/.nvim. In any case, I still have the following error messages:

Erreur détectée en traitant /Users/chambert/.config/nvim/plugin/lean.lua :
E5113: Error while calling lua chunk: /Users/chambert/.config/nvim/plugin/lean.lua:3: module 'compe' not found:
        no field package.preload['compe']
        no file './compe.lua'
        no file '/usr/local/Cellar/luajit-openresty/2.1-20210510/share/luajit-2.1.0-beta3/compe.lua'
        no file '/usr/local/share/lua/5.1/compe.lua'
        no file '/usr/local/share/lua/5.1/compe/init.lua'
        no file '/usr/local/Cellar/luajit-openresty/2.1-20210510/share/lua/5.1/compe.lua'
        no file '/usr/local/Cellar/luajit-openresty/2.1-20210510/share/lua/5.1/compe/init.lua'
        no file './compe.so'
        no file '/usr/local/lib/lua/5.1/compe.so'
        no file '/usr/local/Cellar/luajit-openresty/2.1-20210510/lib/lua/5.1/compe.so'
        no file '/usr/local/lib/lua/5.1/loadall.so'

I woud guess that pathogen is not loded…

[Julian Berman]

Possibly -- Make sure you mean ~/.config/nvim again, not ~/.nvim?

[Julian Berman]

:scriptnames will tell you whether pathogen loaded compe

[Julian Berman]

and if you don't mind editorializing, I would personally not really recommend you use pathogen

[Julian Berman]

Tim Pope is a genius, and pathogen is great -- but if you're just starting I don't see why you'd want to use it, plug is way easier to use

[Julian Berman]

@Antoine Chambert-Loir (Headed out for a bit but yeah let me know if that still doesn't fix it, I do want to make sure this is as easy and clear as possible!)

[Ryan Lahfa]

FWIW: https://github.com/NixOS/nixpkgs/pull/143923 :)

[Anders Christiansen Sørby]

I've tried a basic setup for a nix flake build, but got some errors: https://github.com/Julian/lean.nvim/issues/192

[Ryan Lahfa]

Anders Christiansen Sørby said:

I've tried a basic setup for a nix flake build, but got some errors: https://github.com/Julian/lean.nvim/issues/192

As @Patrick Stevens noticed, some dependencies are minimal for this plugin: https://github.com/NixOS/nixpkgs/pull/144282

[Rish Vaishnav]

recording-2021-11-16_09.33.42.mp4

Introducing: state diffs! This makes it a bit easier to see what changes from one state to the next. Specifically, you can place down a "diff pin" that is diff'ed against the current state, and we also have an "auto diff pin" mode (which I'm using here) to make the diff pin automatically trail the cursor so that if you're precise enough about your motions it will immediately show you the diff from the previous tactic.

This just uses vim's built-in text-based diff functionality, so it can get messy (as you saw near the end there). I expect we'd eventually have something more precise for Lean 4. And as always you can take this as a call for beta testers, let us know if you find any bugs!

[Rish Vaishnav]

@Julian Berman @Gabriel Ebner Figured I should let you know that I don't think I'll be reviewing or working much on the plugin for at least the next few weeks (unless I think of a hot new feature that helps me a lot with Lean 3) since I need to focus on getting some first formalizations into mathlib for my Master's thesis project (planning to formalize Judea Pearl's results connecting probability and graph theory). So feel free to take over for now and @ me if you're hopelessly lost on any of my code haha... And also happy new year!!

[Julian Berman]

Happy New Year! Yeah I figured you were deep in thesis land given you're usually responding with solutions before I finish figuring out what a problem is :D -- good luck, sounds good.

[Julian Berman]

So far not lost! Getting my bearings.

[Julian Berman]

(I guess a good sign of that is I haven't brutally broken anything in my mashing yet, at least to the best of what I can tell. Hopefully not chopping things up too bad.)

[Matthew Ballard]

First, I :heart: this plugin. Thanks for making it.

Should I notice performance differences between the language server in nvim and vs code?

[Julian Berman]

Glad to hear it! I'm not aware of any specific ones but if you have one in front of you do share and we can look into it

[Julian Berman]

Thanks to @Bhavik Mehta 's whims and my newfound unemployment insomnia, we now have tactic highlighting. How precisely it looks will depend on your color scheme, but e.g. mine looks like:

Screen-Shot-2022-03-14-at-06.46.59.png

Feedback of course welcome.

If you want precisely what I see, you want this colorscheme with this override for tactics color.

[Eric Rodriguez]

that looks absolutely gorgeous!

[Yaël Dillies]

Could it be a different color from other classes of keywords, namely declaration keywords and begin end/by?

[Julian Berman]

Sorry, which ones from which ones Yaël -- make begin/end by different from with? Or something else?

[Julian Berman]

Going to drop support for neovim 0.5.1, which is really old, no longer supported upstream, and is randomly failing some test. I assume no one is using this (including not you anymore @Gabriel Ebner ?) but if that's not the case let me know.

[Gabriel Ebner]

It has been some time since 0.6 was released, so this is fine with me.

[Bartosz Piotrowski]

Hi, many thanks to Julian et al. for this wonderful plugin! I have a question: is it possible to switch off the infoview updates in the insert mode? I tried to achieve this by removing a line containing CursorMovedI in lua/lean/infoview.lua by somehow it didn't make any difference...

[Julian Berman]

Thanks for the kind words. At the minute there isn't one, though it should be easy to add, happy to do so -- would you mind elaborating on why you want to do it (not that it sounds like a bad idea at all, just want to make sure I understand the motivation in case there's something else we should add.). I know personally I find it really annoying sometimes that the infoview clears and shows "processing" while I'm typing, and would prefer it leave the last update so I can stare at it. Is that the reason?

[Bartosz Piotrowski]

Yes, this is the reason! Sometimes when I start writing a next tactic with arguments from the context and the context suddenly disappears from the screen, I have trouble remembering the names of the hypothesis I need. Then I need to remove what I wrote and start again (or move the cursor back, but this not always restores the previous state). Apart from that, I find this a bit distracting when the infoview changes with each keystroke. I believe some people like this immediate feedback but for me personally it would be much better to update only after I finish inserting a full command.

[Julian Berman]

Understood -- OK. Let me think a small bit, I think the behavior I personally want is slightly different from "don't update at all until you exit insert mode", it's more like "don't show errors until I stop typing for a bit, and never clear the infoview, just keep showing the last thing that was there until a new thing is ready"

[Julian Berman]

But this is definitely a reasonable request, and probably we can add something that lets both of us have what we want :)

[Alex J. Best]

In the vscode extension there is a button to pin the infoview to a fixed cursor location, does that exist in nvim yet?

[Julian Berman]

Yes, we have pins (though honestly I still want to tweak how they work, which will require some discussing).

[Julian Berman]

You can place one with <localleader>x.

[Julian Berman]

Feedback of course welcome on them.

[Matthew Ballard]

Julian Berman said:

That's the wrong place (lsp/_util), but sorry that the docs don't make this example clear. Right now you do this by:

require('lean').setup{
  -- whatever other options you set
  lsp3 = {
    cmd = { 'lean-language-server', '--stdio', '--', '-M', '4096', '-T', '3000000' },
    -- on_attach = on_attach or whatever else you set here
  },
}

Is still the correct way to pass memory configuration to language server?

[Julian Berman]

Yep, it should be, and Tsvi was kind enough to add it here as an explicit copyable example -- is it working for you?

[Matthew Ballard]

Hmm. Let me try again and report back. Hopefully, it is user error.

[Julian Berman]

Success? Or failure?

[Julian Berman]

It slightly annoys me when I need to tweak this myself, I kind of wish we had a separate memory = whatever; timeout = whatever table and then assembled the CLI on user behalf like vscode-lean does, but I think Gabriel had a comment somewhere on doing so that I'll have to dig up.

[Matthew Ballard]

Ambiguous. I managed to crash the language server with the same memory/timeout settings that worked for vs code but I didn't investigate further. But before that performance seemed comparable.

[Julian Berman]

It's essentially just keeping parity with the recent VSCode PR thanks to Eric, but we've now got symbol searches in Lean 3 via the same code:

screen.gif

(This already works out of the box in Lean 4)

[Matthew Ballard]

Is there an easy way to search for/replace unicode? Generally I would have thought there was a plugin to search/replace based on a selection.

[Julian Berman]

I haven't had a ton of time for lean the past two months given my new job (though hopefully things are calming a bit) -- which is to say expanding abbreviations in cmd mode is a feature that should be reasonably easy to implement but I haven't gotten time to do so yet

[Julian Berman]

In the interim the easiest thing is to use a register or copy paste :/

[Julian Berman]

(:h i_^R for the former if you need it)

[Matthew Ballard]

Thanks. No rush :smile:

[Julian Berman]

OK, I made expanding abbreviations work at least in the cmdline window (even though it doesn't still with /). But the former means there's at least an easy way to search now. :h q/ if you've never used it before, but basically type q/ and you get a normal mode window you can type searches into, and which'll expand unicode abbreviations (as long as you enter it from a lean buffer). Feedback of course welcome. See the screencast if that's not enough info:

abbrev.gif

[Julian Berman]

A minor UX tweak which anyone using lean.nvim may have opinions on -- I'd like to make the cursor in the infoview window be on the (first) goal line by default, rather than at the top. The main reason is that for short infoviews the goal is often off to the bottom (and invisible without scrolling) which I find annoying, and especially so for vertical displays where the infoview can be short.

https://github.com/Julian/lean.nvim/pull/279/files is the PR if you care to try it out, or otherwise if you have an opinion on the behavior (especially if you don't like the proposed change) feel free to share.

[Matthew Ballard]

+1 for me. It’s easy to jump to the top of a buffer if needed.

[Alex J. Best]

This sounds like a good change to me, I'm often annoyed by this in vscode too and have wondered if putting the goal at the top and ordering the hypotheses below it in order of last modified would be a better UX than the present default. Though I can see how this is confusing from a proof calculus perspective

[Alex J. Best]

Unfortunately changing the list order using pure CSS results in a broken widget display, so I never tried this order seriously for a long time, it can be very helpful though on long proofs though

[Patrick Massot]

In VScode you can control this using widgets. See https://github.com/leanprover-community/sphere-eversion/commit/81f98837feab576e17053cc97623b404c019b9db

[Alex J. Best]

Nice! And I just checked that it does work in nvim also :smile: which one would hope given that thats the idea of widgets after all, but its good to be sure.

[Alex J. Best]

Can we add a (deduplicated version of) this to mathlib? E.g. As a tactic file that isn't allowed to be imported within mathlib (like omega), but people could import while working if they like. I think enough people would find it useful.

[Jireh Loreaux]

Is it possible to add as something accessible with set_option?

[Julian Berman]

I've added a small section to the README on enabling semantic highlighting in Lean 4 (even though support upstream is via a plugin rather than built-in to neovim for a bit longer).

If you want to try it feel free to follow the instructions, and ask if you run into trouble (or edit the wiki, which is always welcome).

[Julian Berman]

Two minor lean.nvim tweaks -- I just attempted to copy the inaccessible hypothesis highlighting from VSCode, so now one should see something like:

Screenshot-2023-07-04-at-17.03.52.png

If you don't like that, or want to tweak the colors, leanInfoInaccessibleHyp is the hilight group you want to touch (it's linked to Comment by default).

And secondly there's now a simple switch for sorry <-> exact? in Lean 4 (as usual if anyone has suggestions for better switches, or for things in general, feel free to share).

[Calvin Lee]

Is anybody else experiencing freezes in lean.nvim?
not sure why it's happening to me, but it's fairly common after a few backward movement commands, from what i can tell.
I just haven't had time to track it down and wasn't sure if it was just me
(neovim completely shuts down, and won't respond to ^C or ^Z, and instead i have to SIGKILL it... it's really a huge pain working with lean like this)

[Julian Berman]

I have done some number of Lean hours greater than epsilon this week, which is more than the previous few months -- and have not experienced any, though in the past I recall sporadic times

[Julian Berman]

The usual advice I'd give is "try a newer version and hope it works better"

[Julian Berman]

(Newer version of nvim)

[Julian Berman]

Also check that you don't have any orphaned Lean processes in the background just in case

[Calvin Lee]

I'm using the stable arch release of nvim (currently 0.9.1)
maybe i'll try nightly

[Julian Berman]

Obviously if you can manage to reproduce anything please share.

[Julian Berman]

Next time it happens you can possibly also try stracing the process to see what the heck it's doing though if it won't respond to ^C there's a decent chance it won't attach either I guess

[Matthew Ballard]

lean.nvim#289 I still get this but have been too lazy to debug properly. If you find anything more out, I would love to hear. My guess is an extension conflict.

[Julian Berman]

I now have a stack trace of this happening, but I don't see anything particularly useful (yet?). But my guess is something lower level in nvim that's broken, if anything the trace is saying it's perhaps stuck firing autocmds... Hrm.

[D. J. Bernstein]

I see each typed character in nvim spinning up a new Lean thread (evident in system load monitoring). The time for the thread to finish depends very much on how complicated the currently edited proof is: long formulas with ambiguous types, search tactics, defeq challenges, etc. Spinning up enough uncompleted threads will quickly freeze nvim. Presumably some limited resource is being exhausted within nvim or Lean. A simple workaround is to put /-- above the proof being edited (so each thread finishes quickly), and then remove the /-- after editing to feed the proof to Lean.

[Matthew Ballard]

I have this happening without editing the files. Often just moving quickly through the document is enough to trigger it for me.

[Julian Berman]

I'll have a look at the code we're using to backoff sending infoview state requests, which presumably are the ones involved in either case, we fire them obviously anytime the cursor moves to get the new infoview state. I think we do have some sort of existing backoff there, but maybe outstanding requests aren't being cancelled, or something.

(Thanks for the tip both of you.)

[Wojciech Nawrocki]

Note also that the LSP server merges several subsequent keystrokes into one edit that then gets processed by a single task, as long as the keystrokes happen in quick succession. The expected typing speed is configurable via the 'edit delay' option (passed through here in vsc-lean4). I'm not sure if lean.nvim exposes this, but it could help.

[Julian Berman]

The expected typing speed is configurable via the 'edit delay' option (passed through here in vsc-lean4).

I added a note for how you tweak this with lean.nvim here and have tweaked the value locally just to play around with it.

[Matthew Ballard]

Much thanks for looking into this. I have had freezes ~10-20/day recently. I’ll test drive a higher delay today. Is 200 ms the default currently?

[Julian Berman]

I'm somewhat skeptical it'll help honestly, though I'm trying to cause another freeze, and yeah sorry for the disruption, still no idea what's happening :/

[Julian Berman]

The default is 200ms yeah. I dropped mine locally to 50ms (which definitely feels snappy :D) but in the past 10 minutes of randomly scrolling through and opening files I haven't managed to get something to freeze.

[Matthew Ballard]

I’ll definitely be able to tell by the end of day if there is an effect

[Matthew Ballard]

Not a single freeze at 50 ms today. Certainly possible it is a fluke but very, very encouraging.

[Calvin Lee]

just had my first freeze since changing to 50ms
it's still present but a lot rarer

[Matthew Ballard]

This is my sense also. I may try to drop it further.

[Julian Berman]

Hrm, fascinating, ok yes let me know if lower is even better, though it'd still be quite confusing why VSCode doesn't run into issues, as I think its default is left at 200.

[Wojciech Nawrocki]

This is a bit surprising, lowering the delay will use more compute on the Lean side as your code is elaborated more often. But it sounds like the freezes are entirely on the nvim side rather than due to system overload. Perhaps nvim LSP expects notifications from the server to come more often than they actually do when the delay is higher.

[Matthew Ballard]

I was thinking that it is overloading nvim in some way when all the lsp updates get sent at once. If so, I would also think that something similar would have been observed.

[Julian Berman]

I have a lead on how to figure out what is freezing on the neovim side (it's nothing terribly intelligent, it's mostly "sprinkle prints in the few places we might be blocking the event loop forever to see which one is the one we actually are in when things freeze"), but I probably won't get to poking at it for another few days, so I'm quite glad regardless that this improves things for now

[Gihan Marasingha]

I've just installed the plugin, following the instructions in the Getting Started Wiki. It's great!

One question:

When I do <Leader>n, I get the error message:

E5108: Error executing lua: /Users/xxx/.config/nvim/plugin/lean.lua:50: attempt to call field 'goto_next' (a nil value)
stack traceback:
    /Users/xxx/.config/nvim/plugin/lean.lua:50: in function </Users/xxx/.config/nvim/plugin/lean.lua:50>

<Leader>n should "jump to the next Lean line with a diagnostic message". I assume (perhaps incorrectly) that #check commands produce diagnostic messages. Here is my MNWE:

#check Nat.mul_assoc
#check Nat.add_assoc

What am I doing wrong?

Setup: Lean 4 on an M2 MacBook.

[Julian Berman]

#check indeed produces a diagnostic message, so it's probably not you that's done something wrong! Let's see...

[Julian Berman]

Ah the issue is that newer nvim renamed where that function lives.

[Julian Berman]

@Gihan Marasingha I've just updated the section with the new names, can you try that again and let me know if it works for you

[Gihan Marasingha]

@Julian Berman Thanks. That fixes things!

[Gihan Marasingha]

The sorry.fill function doesn't work for Lean 4. Of course, one simple alternative is to remove the comma from "{ sorry },"

However, a cleaner style in Lean 4 is to use indentation for subgoals. I've written an alternative Lua function that seems to do the right thing. If that functionality is desirable, please let me know and I'll make a PR.

[Gihan Marasingha]

The problem with my proposed function is that it ruins the Lean 3 behaviour.

[Julian Berman]

A PR would be great, though even better I think might be moving this functionality to Lean using the new code actions framework (which means it wouldn't just work in lean.nvim)

[Julian Berman]

(If it did stay in lean.nvim then casing on the filetype should handle the lean 3 vs 4 bit -- but yeah I suspect doing this as a code action is the right upgrade really)

[Gihan Marasingha]

OK, for the moment, I've just done the simpler PR by modifying sorry.fill. The code checks vim.bo.filetype and takes appropriate action.

[Julian Berman]

TL;DR lean.nvim has a new README demo. Give feedback if you see anything missing or you'd like to see.

This morning someone posted a thing[1] to HN that I've wished existed for years. Given it exists, of course the first thing to do is use it to re-write a new (Lean 4) demo for lean.nvim. You can find that in the README, or here below as a GIF:

demo.gif

[1]: VHS, a tool for writing "scripts" for video recordings of demos / usages of programs, which can be used to automatically regenerate screen recordings when you modify the script. Hooray! lean.nvim's demo script now lives in the repo.

[Scott Morrison]

Wow, VHS is nice. :mind_blown: Now we just need it for VSCode. :-)

[Julian Berman]

Isn't it?

@Scott Morrison google says maybe https://github.com/microsoft/codetour is a thing?!

[Scott Morrison]

Interesting, thanks. Maybe one day I'll have time to try it. :-)

[Henrik Böving]

Julian Berman said:

Henrik Böving said:

Just to make sure I'm not going to duplicate work: has someone here already started implementing this as a neovim telescope plugin?

I have not yet though I certainly intended to both for Loogle and Moogle.

Hm, well I guess I was gonna try either way because I've never written a nvim plugin before, I'm sure it will end up being quality software :tm:

[Julian Berman]

Well, I'm happy to help! Or see it be part of lean.nvim, or whatever is helpful.

[Henrik Böving]

image.png
High tech feature :tm:

@Julian Berman do you want me to PR this to lean.nvim or should it be a separate plugin?

[Julian Berman]

Woohoo, well done. I'd love it in lean.nvim itself, seems like people like Loogle a lot (justifiably probably though I haven't gotten a chance to use it myself). But yeah let's stick it in!

[Henrik Böving]

Okay I'll put that on my TODO list for tomorrow

[Julian Berman]

As require'lean.loogle' probably, enablable/disablable via config, and probably on by default assuming there's no real dependencies in what you have

[Julian Berman]

I want to heart your comment but Android Zulip keeps jumping around when I try to click the emoji so consider this a heart.

[Henrik Böving]

Julian Berman said:

As require'lean.loogle' probably, enablable/disablable via config, and probably on by default assuming there's no real dependencies in what you have

It needs plenary and telescope so it would add one dependency.

[Julian Berman]

Plenary is already a dep

[Julian Berman]

For telescope yeah fair basically it should be enabled if the user has telescope and not otherwise

[Julian Berman]

But that's very minor to tweak if need be

[Julian Berman]

It may also be the case that your code might be able to use vim.ui.select

[Julian Berman]

But I'll point that out on PR if so (and then it doesn't even depend on telescope!) unless you feel like looking at what that is if you don't already know

[Notification Bot]

13 messages were moved here from #general > Call for help: Loogle in VS Code by Julian Berman.

[Joachim Breitner]

I want to heart your comment but Android Zulip keeps jumping around when I try to click the emoji so consider this a heart.

https://github.com/zulip/zulip/issues/11448. I’m also less emphatic on the phone than I’d like to be.

[Joachim Breitner]

@Henrik Böving , could you add a nice User-agent to the request, possibly even with version information? It will be informative to see with which tools people use the loogle api.

[Henrik Böving]

Joachim Breitner said:

Henrik Böving , could you add a nice User-agent to the request, possibly even with version information? It will be informative to see with which tools people use the loogle api.

:salute:

[Henrik Böving]

Merged, it reports with a User-Agent of "lean.nvim" for now.

[Julian Berman]

Hello.

I have pushed a "fork" of Mathlib4 which essentially swaps the VSCode GitPod out for .. neovim of course. It lives here: https://github.com/Julian/neomathlib (implementation note: all it does is modify the .docker/gitpod/Dockerfilefrom the mathlib4 repo).

If you configure GitPod to clone your dotfiles, as I just did, then you end up with a surprisingly easily working environment with mathlib cache populated etc.. I guess that's what all the VSCode people have been raving about :). In slightly further detail -- pick "Terminal" as your environment (it's one of the options), then pick that repo as your workspace, then clone your dotfiles, and be sure you have lean.nvim as one of your plugins.

There's nothing new here that's lean.nvim-specific other than "it's in a browser", but It looks like:

Screen-Recording-2023-11-26-at-4.03.09-PM.gif

If anyone finds this particularly useful I can automate updating Mathlib4 from the upstream repository so it stays permanently up to date -- and of course if anyone has ideas for how to make running this even more straightforward to use do let me know. I considered installing lean.nvim globally so it just works when you start it -- but the truth is you anyhow then need some personal settings, so it doesn't seem like it saves much. But willing to put some more thought in there if someone finds it useful.

[Calvin Lee]

Julian Berman said:

I have pushed a "fork" of Mathlib4 which essentially swaps the VSCode GitPod out for .. neovim of course. It lives here: https://github.com/Julian/neomathlib (implementation note: all it does is modify the .docker/gitpod/Dockerfilefrom the mathlib4 repo).

Is there any reason this has to be a fork and can't be upstreamed? it seems reasonable to include both neovim and vscode configuration in the mathlib4 gitpod

[Francisco Giordano]

How do people deal with Unicode delimiter pairs when editing Lean in Vim?

For example, if you're in front of the text exact Nat.le_trans ‹i ≤ _› ‹_ ≤ j›, how would you go about changing the content within the angle brackets, given that they are the french angle brackets and ci< won't work. The same goes for ⟨,⟩. I haven't found myself using other kinds of delimiters yet.

@Julian Berman have you thought about adding something in lean.nvim to help with this somehow?

I use wellle/targets.vim and it is possible to extend the settings to deal with these delimiters. I don't think there are any built-in settings that can configure this. Also not sure it would make sense to add targets.vim as a dependency of lean.nvim.

[Julian Berman]

Francisco Giordano said:

How do people deal with Unicode delimiter pairs when editing Lean in Vim?

For example, if you're in front of the text exact Nat.le_trans ‹i ≤ _› ‹_ ≤ j›, how would you go about changing the content within the angle brackets, given that they are the french angle brackets and ci< won't work. The same goes for ⟨,⟩. I haven't found myself using other kinds of delimiters yet.

Julian Berman have you thought about adding something in lean.nvim to help with this somehow?

I use wellle/targets.vim and it is possible to extend the settings to deal with these delimiters. I don't think there are any built-in settings that can configure this. Also not sure it would make sense to add targets.vim as a dependency of lean.nvim.

We already set matchpairs for the structure literals -- I just added the assumption ones, whatever they're called.

I use vim-matchup so for me that means I can use ci% to change between either of those -- I suspect targets.vim will have some equivalent text object because yeah, it's just a builtin vim option. But if not let me know and I can look into it.

[Julian Berman]

Calvin Lee said:

Julian Berman said:

I have pushed a "fork" of Mathlib4 which essentially swaps the VSCode GitPod out for .. neovim of course. It lives here: https://github.com/Julian/neomathlib (implementation note: all it does is modify the .docker/gitpod/Dockerfilefrom the mathlib4 repo).

Is there any reason this has to be a fork and can't be upstreamed? it seems reasonable to include both neovim and vscode configuration in the mathlib4 gitpod

That's a question for @maintainers I guess, or perhaps @Eric Wieser specifically who I think added the VSCode gitpod support -- certainly if you (and hopefully others) use it and want it it makes asking easier :D -- I also considered this but was hoping someone else would be the one to propose it.

Mathlib folks are you ok with me merging that in and sending a PR (i.e. installing neovim too in the gitpod setup)?

[Patrick Massot]

Does it make it any harder to use VSCode in gitpod? Or would this be completely transparent to VSCode users?

[Julian Berman]

It's completely transparent.

[Francisco Giordano]

Julian Berman said:

I suspect targets.vim will have some equivalent text object because yeah, it's just a builtin vim option. But if not let me know and I can look into it.

% works because it's default in vim. Though it might make sense to add ‹:› as a pair too.

I suppose for better integration with the other features of targets.vim I can just set it up in my config.

[Julian Berman]

I'm talking about the text object (which in matchup is set to i%) not just the navigation which is %

[Julian Berman]

Looks like targets.vim doesn't respect that setting -- https://github.com/wellle/targets.vim/issues/130 and https://github.com/wellle/targets.vim/issues/169 -- I'd probably try to copy the code there to your config

[Julian Berman]

(It should really respect that setting, but however many years later that seems still open which is never a good sign)

[Julian Berman]

(PR for Gitpod: https://github.com/leanprover-community/mathlib4/pull/9024 )

[Matthew Ballard]

Delegated

[Julian Berman]

I haven't bothered setting up an autocmd to only run this in the Mathlib repo, but for anyone who works on Mathlib and might find it useful, https://github.com/Julian/dotfiles/commit/a3091b44a123931630c0241e1f836e7f4dd8e89b is how you run the Mathlib4 style checker using nvim-lint to catch style mistakes as you edit. I'll add it to the wiki whenever I get to doing the aforementioned autocmd'ing.

[Patrick Massot]

Inspired by recent discussion on the emacs mode, I’d like to give lean.nvim another try. But the first thing I wanted to do doesn’t seem to work. I’d like to resize the info view but Ctrl-w = doesn’t seem to do anything. @Julian Berman

[Chris Henson]

Same here. Though resizing just the infoview with Ctrl-w >, etc. works fine.

[Patrick Massot]

Also do you have an example config for semantic syntax highlighting? The default one is really not usable at all (or else there is something wrong with my config).

[Julian Berman]

Nice! Your suggestions obviously are super welcome. For that one -- you want your infoview equal width obviously? We set winfixwidth so that infoview contents don't jump around as you open and close windows -- if you do want to use ^W=, you can first turn that off. I can add that as a config option to make that directly supported

[Julian Berman]

In the immediate meantime you can use lua vim.wo[require('lean.infoview').get_current_infoview().window].winfixwidth = false and then ^W= should work again

[Patrick Massot]

Indeed this fixes the issue.

[Julian Berman]

Patrick Massot said:

Also do you have an example config for semantic syntax highlighting? The default one is really not usable at all (or else there is something wrong with my config).

I only set one thing in mine it looks like -- https://github.com/Julian/dotfiles/blob/3fd4b990155547676c97a995191ef6b66bfa1286/.config/nvim/after/syntax/lean.lua#L1-L8 -- but it will depend on your theme. Try what I use for a moment, see if it's more correct -- I'm using kanagawa -- https://github.com/Julian/dotfiles/blob/3fd4b990155547676c97a995191ef6b66bfa1286/.config/nvim/lua/plugins/init.lua#L3-L12

[Julian Berman]

Patrick Massot said:

Indeed this fixes the issue.

OK, cool, I'll add an option in a bit which causes lean.nvim to not set that option, and presumably also you'd like the width/height to not be set at all so it starts off equal size? If so I'll just make it do that too.

[Patrick Massot]

The starting size question is really tricky because it depends a lot on your screen size.

[Julian Berman]

Right, there's an open issue to do this with percentages

[Chris Henson]

@Julian Berman While you're here, is there a simple way to have the infoview automatically close when you close all of the buffers with .lean files?

[Patrick Massot]

The syntax highlighting is still very weird, I will try your theme.

[Julian Berman]

Chris Henson said:

Julian Berman While you're here, is there a simple way to have the infoview automatically close when you close all of the buffers with .lean files?

the "robust way" we haven't implemented yet because it's more complicated than it sounds -- but there's a simple way which will work that you can use which another contributor wrote out, one sec.

[Julian Berman]

@Chris Henson try this by @Francisco Giordano : https://github.com/Julian/lean.nvim/issues/43#issuecomment-1850633100 and please let me/us know if it works (well or otherwise)

[Julian Berman]

I am hoping to have some more time for Lean in the next few weeks (part of my secret plan to merge it in part with my day job) -- but nag-driven-development is also very effective, so if you or anyone run into issues do complain.

[Chris Henson]

Julian Berman said:

Chris Henson try this by Francisco Giordano : https://github.com/Julian/lean.nvim/issues/43#issuecomment-1850633100 and please let me/us know if it works (well or otherwise)

On first try it seems to work as expected, thank you! Your work on this plugin is much appreciated.

[Patrick Massot]

I can confirm that changing to your theme gives more meaningful colors.

[Julian Berman]

Great! Obviously the one I use I don't think is the only one that will work -- what you'd be looking for is some reasonably modern theme, because neovim 0.9 changed the name of highlight groups a bit, so the theme has to keep up

[Julian Berman]

But before this I used to use edge and that worked fine too I think.

[Julian Berman]

(if you want details on how to manually change colors we should obviously document that too...)

[Patrick Massot]

But it is also very dull and looses nice other things like thinner vertical lines separating buffers or removing the stupid tildes at the end of a buffer.

[Patrick Massot]

I was using onedark

[Julian Berman]

that shouldn't be related, it's funny if a theme is messing with the latter at least

[Julian Berman]

those are normal settings, which I guess the theme is changing on your behalf

[Julian Berman]

I don't remember what the tilde one is called, it's the first thing everyone turns off, let's see...

[Patrick Massot]

Weird, it seems to be gone now.

[Julian Berman]

OK cool -- are you roughly in working shape then?

[Patrick Massot]

Yes it seems ok now. Thanks a lot for your help!

[Patrick Massot]

Let me now try to edit code…

[Patrick Massot]

Before I tried editing code for real I went to get some coffee. When I came back to my office I immediately noticed the CPU fan noise. It turns out nvim was using 100% of a CPU…

[Julian Berman]

Was it compiling mathlib? Or doing nothing?

[Patrick Massot]

Doing nothing

[Julian Berman]

Strange. Only thing I'd say is make sure you're up to date, and if it happens again we can maybe strace to see what the heck it's doing.

[Julian Berman]

Ah wait sorry, we still haven't addressed https://github.com/Julian/lean.nvim/issues/289, which I forgot about -- after tweaking a lean setting I don't think any of us have encountered that in awhile, but we didn't change the default

[Julian Berman]

I still think it probably sounds like a lean bug but I am not good enough at figuring out how to isolate it.

[Julian Berman]

Anyways Patrick, try adding this: https://github.com/Julian/dotfiles/blob/main/.config/nvim/lua/plugins/lsp.lua#L245

[Julian Berman]

(disabling editDelay)

[Julian Berman]

If that makes it go away maybe I'll make it the default, this has been an issue for ages so may as well make it work out of the box

[Matthew Ballard]

I have been living happily for a long time now with this as my setting

[Julian Berman]

Ok, much as it makes me uncomfortable to change lean behavior, I trust your vote, will tweak it later

[Patrick Massot]

Ok I added the option, we’ll see whether this happens again.

[Patrick Massot]

Julian, the video in the README is very frustrating because it shows many things you can do but then nothing in this README explain how to do them.

[Patrick Massot]

For instance I don’t how to jump to definition. The obvious gd works in the info view but not in the main buffer.

[Julian Berman]

A bit of that is because don't terribly want to document "normal" neovim things -- which I recognize makes it hard to get started if you don't already use "normal" neovim heavily, but your question basically applies to any language -- I am probably happy to answer how to do things if you have specific ones

[Julian Berman]

For gd, that question is related to https://github.com/neovim/neovim/issues/24252 -- which don't bother reading -- but basically it is still being worked on upstream whether default mappings will automatically be made for LSP things! Only K is automatically mapped right now

[Julian Berman]

So in short, if you want a set of good mappings, here's what I use: https://github.com/Julian/dotfiles/blob/3fd4b990155547676c97a995191ef6b66bfa1286/.config/nvim/lua/plugins/lsp.lua#L18-L92

[Yury G. Kudryashov]

You can point to the documentation page of lsp for neovim which lists useful functions to bind.

[Yury G. Kudryashov]

I mean, in the docs for lean.nvim.

[Yury G. Kudryashov]

And to your config file as an example.

[Julian Berman]

In particular the line that makes gd work is this one: https://github.com/Julian/dotfiles/blob/3fd4b990155547676c97a995191ef6b66bfa1286/.config/nvim/lua/plugins/lsp.lua#L25 which is equivalent to vim.keymap.set('n', 'gd', vim.lsp.buf.definition, { buffer = 0 })

[Julian Berman]

Yury G. Kudryashov said:

And to your config file as an example.

we do both of these already! It's not enough clearly though

[Julian Berman]

https://github.com/Julian/lean.nvim?tab=readme-ov-file#configuration--usage and/or https://github.com/Julian/lean.nvim/wiki/Getting-Started-From-the-Ground-Up in particular points you to the neovim docs, including a suggested setup

[Julian Berman]

But I sympathize that it's hard to know that that's where you need to look if you don't know why something doesn't work

[Julian Berman]

(All again to say if you have specific suggestions I'm all for helping)

[Julian Berman]

Patrick let me know if you have other examples and I can try to either answer or document or both

[Patrick Massot]

Thanks. Part of the issue is that I recently tried to modernize my vim. In particular I try to use lua configuration files and there are many things I don’t understand. In particular I already have a line that tries to bind this but it doesn’t seem to work.

[Julian Berman]

Your dotfiles aren't public by chance are they? Make sure you're doing the mapping inside of the function that you pass to lsp = { on_attach = THISFUNCTION } }

[Patrick Massot]

They are almost entirely the files from kickstart.vim

[Julian Berman]

Ah that's good, I want to show an example using kickstart.vim but haven't had the time to look at it

[Patrick Massot]

Actually on this computer I tried the variant https://github.com/dam9000/kickstart-modular.nvim

[Patrick Massot]

In particular I have the lines https://github.com/dam9000/kickstart-modular.nvim/blob/master/lua/lsp-setup.lua#L23-L25

[Patrick Massot]

But still no bindings

[Julian Berman]

Are you passing that function to lean.nvim?

[Patrick Massot]

I can call the lsp function from command mode so this is definitely a binding issue.

[Patrick Massot]

Julian Berman said:

Are you passing that function to lean.nvim?

I don’t know how to do that, so probably no.

[Patrick Massot]

I really know nothing about this lua world. I’ve been using vim for 20 years but not in this modern way.

[Julian Berman]

Here's the short explanation

[Julian Berman]

These lines in the example: https://github.com/dam9000/kickstart-modular.nvim/blob/master/lua/lsp-setup.lua#L71-L95 are trying to tell you "enable whatever languages you use"

[Julian Berman]

But lean.nvim -- much like the rust plugin -- handle calling that on your behalf already

[Julian Berman]

You essentially need to keep a reference to that on_attach function, and then pass it to lean.nvim when you call its setup

[Julian Berman]

The cheap and easy way for right now is instead of local on_attach, do _G.on_attach = function() ....

[Julian Berman]

and now you have a global function called _G.on_attach -- then when you call require('lean').setup{ ... }, now you use _G.on_attach as your on_attach function

[Julian Berman]

Does that make any sense, or do you want me to try to write it out a bit more specifically? If you paste how (or if) you're currently calling lean.setup{} that also might help.

[Patrick Massot]

I cannot get it to work. I think I will put my config on GitHub. It will be convenient to share it among my computers anyway.

[Patrick Massot]

I dumped everything on https://github.com/PatrickMassot/neovim_config. It features the whole kickstart repo which is maybe not very smart.

[Patrick Massot]

I need to go anyway, but I’ll try again tonight.

[Patrick Massot]

It feels a lot more promising than last time I tried.

[Patrick Massot]

One thing I can already say is that having the infoview as an ordinary buffer is a bit annoying. It makes it more complicated to quit (I need a :qa when I really mean :q) and it messes up :bp.

[Julian Berman]

I have limited time tonight but will take a quick look now to see if I can just give you some hint.

[Julian Berman]

One thing I can already say is that having the infoview as an ordinary buffer is a bit annoying. It makes it more complicated to quit (I need a :qa when I really mean :q) and it messes up :bp.

The :q thing is obviously related to the discussion above -- you can use the same autocommand to have the infoview quit

[Julian Berman]

(Which means then you won't need :qa)

[Julian Berman]

:bp I would simply recommend you never use honestly

[Julian Berman]

Even if it's a bit of retraining muscles.

[Julian Berman]

But the modern way is to use a fuzzy finder

[Julian Berman]

(Telescope being the one that all the kids are excited about these last 5 years, so you may as well use it)

[Julian Berman]

OK I got a few minutes to look -- you have it almost right but there is some issue with what order files are loading in, which is common.

You can fix this in a crude way with:

diff --git a/lua/lazy-plugins.lua b/lua/lazy-plugins.lua
index 5049773..6fe4300 100644
--- a/lua/lazy-plugins.lua
+++ b/lua/lazy-plugins.lua
@@ -215,7 +215,10 @@ require('lazy').setup({
     -- see details below for full configuration options
     opts = {
       lsp = {
-        on_attach = _G.on_attach,
+        on_attach = function(client, bufnr)
+          require('lsp-setup')
+          on_attach(client, bufnr)
+        end,
         init_options = { editDelay = 0 },
       },
       mappings = true,

which seems to make things work here -- this which-key plugin which I've heard of but don't use kind of makes it a bit annoying to diagnose because it is messing with gd itself, but whatever -- I think just that change above will unblock you for now. Honestly I'm a bit disappointed at how slow this setup is that they start you with :/ but ok whatever, it has some decent plugins they're setting you up with at least.

If the above doesn't help I can send a PR tomorrow.

[Patrick Massot]

It works, thanks!

[Patrick Massot]

(including the autocommand to close the infoview).

[Julian Berman]

Great! I put in the default for editDelay = 0, so that now should be automatic. I will probably not do the width thing immediately, I want to think it through a bit, because I don't remember why everything works as it does with our window management (but I will do something at some point and let you know). Keep feedback coming.

[Chris Henson]

@Julian Berman Is there a way to configure the infoview to advance manually instead of based on the current cursor position?

[Julian Berman]

Do you mean you want to pause updates to it, or to force it to update itself, or to have it show the state at a different cursor location, or choice D :)?

[Julian Berman]

Or you mean you want it to not automatically update and only update when you tell it to?

[Chris Henson]

Julian Berman said:

Or you mean you want it to not automatically update and only update when you tell it to?

This is what I meant. Only move the infoview to the current cursor position when you tell it to.

[Julian Berman]

Got it - you're aware of pins right? Just to be sure you're not doing this for that reason?

[Julian Berman]

(i.e. because you want to watch what's happening at some other location)

[Chris Henson]

I don't think I am, what are pins?

[Chris Henson]

Oh I see a description in the docs, let me try it out and see how it works.

[Chris Henson]

I see. Not what I meant, but the pins feature is very nice! I am curious how often/how you use the diff pins, they seem interesting.

I still would sometimes prefer advancing the infoview manually. It is just an issue of preference, sometimes the constantly changing infoview is a bit hard on the eyes for my taste. I realize I can mostly get what I want with pausing/unpausing the infoview.

[Julian Berman]

No I was going to say exactly that (that I sometimes get annoyed at how spasmy the infoview is)

[Julian Berman]

I'll fix that at some point, I've wanted to do it in a general way but I still haven't managed to do that, so I'll do the hacky one at some point, just so that it doesn't continuously flash back and forth and clear itself

[Julian Berman]

Anyways, the answer for pausing is lua require'lean.infoview'.pin_toggle_pause()

[Julian Berman]

Which is really confusingly named, I thought I'd renamed that by now but guess not.

[Julian Berman]

I don't think we bind a key to that by default but you can of course.

[Julian Berman]

oh we do, it's <localleader>p

[Chris Henson]

Yeah I tried that, it works well for me. I'm curious, if I bind calling that twice (to unpause and pause again) will it wait for things to run in-between, or potentially interrupt Lean?

[Julian Berman]

Are you doing that to implement the "refresh the infoview now" bit?

[Julian Berman]

We should expose some function to do that if we don't already clearly.

[Julian Berman]

But that should be fine

[Chris Henson]

Yeah pretty much. Maybe not a robust way, but I think I might try it for a bit. Thanks again for the help! (Which in this case was a good reminder to read the docs haha)

[Patrick Massot]

Julian Berman said:

In the immediate meantime you can use lua vim.wo[require('lean.infoview').get_current_infoview().window].winfixwidth = false and then ^W= should work again

What would be the syntax to put that in a config file? Currently the first thing I do whenever I open a Lean file is to search this is my command history.

[Patrick Massot]

The Hoskinson center bought me a giant screen for my office and it is very frustrating to have a super narrow infoview window.

[Julian Berman]

Create a file called ~/.config/nvim/after/plugin/leaninfo.lua and put:

vim.opt_local.winfixwidth = false
vim.opt_local.winfixheight = false

in it

[Julian Berman]

You can also consider upping the width and height setting in your Lean setup settings, if all you want is a wider one and you don't specifically care about ^W= in particular (let me know if you need syntax for that)

[Julian Berman]

(And yeah we should definitely pick some width relative to your screen width -- I use a portrait monitor and my infoview is then on top not the side so this doesn't bother me otherwise probably I'd have fixed it already. I can try to get to it at some point.)

[Patrick Massot]

Oh that’s simple. I was afraid because of the require('lean.infoview').get_current_infoview().window bit.

[Patrick Massot]

Doesn’t seem to work.

[Julian Berman]

I am afraid something is messing with the way "normal" neovim works in that setup again :/ -- I'll have to look at the layout again.

[Julian Berman]

Oh no, it's me who's a dum dum doing too many things at once.

[Julian Berman]

@Patrick Massot ~/.config/nvim/after/ftplugin/leaninfo.lua not plugin

[Patrick Massot]

It works!

[Julian Berman]

Great. Hopefully you see what that does.

[Patrick Massot]

Sure

[Patrick Massot]

And is there a way to avoid typing the ^w= at startup?

[Julian Berman]

Add vim.cmd.wincmd('=') to the bottom of that file is a cheap way

[Patrick Massot]

Thanks, that’s a much better starting point.

[Patrick Massot]

The README says there is some interactive widgets support but I don’t see anything. What is the current status? Even before displaying a widget, can you select things in the infoview?

[Julian Berman]

Yeah, move to the infoview window and press enter to "click" , and tab to move into the popup

[Julian Berman]

Can gove more details tomorrow

[Patrick Massot]

This is not what I am talking about. I ask about the analogue of VSCode shift click.

[Kevin Buzzard]

Yet more proof that nobody other than Patrick knows about this shift click thing :-)

[Kevin Buzzard]

Maybe there should be a blog post about it? Although with this worrying development of Patrick switching from VS Code, maybe the fact that you can shift click on things will soon be lost in time...

[Marc Huisinga]

We'll document these more obscure VS Code features in a reasonable place in the future so that they are not lost to time and forgotten :-)
For InfoView features specifically, we still have to look into whether implementing our own context menu for the InfoView is possible.

[Julian Berman]

Patrick yeah I don't know that I know what shift-click does, or when it does anything -- I just tried typing some random goal and shift clicking and I don't see things happening, can you share some example and tell me what it should do?

[Julian Berman]

Marc Huisinga said:

We'll document these more obscure VS Code features in a reasonable place in the future so that they are not lost to time and forgotten :-)
For InfoView features specifically, we still have to look into whether implementing our own context menu for the InfoView is possible.

Yeah such a list would definitely help me have more parity with VSCode features.

[Marc Huisinga]

Julian Berman said:

Patrick yeah I don't know that I know what shift-click does, or when it does anything -- I just tried typing some random goal and shift clicking and I don't see things happening, can you share some example and tell me what it should do?

See https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.24/LIPIcs.ITP.2023.24.pdf (section 3.2). Many widgets trigger only in a specific selection context.

[Julian Berman]

Aha. I see the mechanics from there, thanks. Is there some widget in Mathlib I can use to test that out? Ideally one that doesn't target HTML output?

[Patrick Massot]

This is the fundamental component of almost any widget whose purpose is not to draw a nice picture you can show in talks but never use for real.

[Patrick Massot]

It is used by the conv? or calc widgets for instance.

[Kevin Buzzard]

Yeah I've used it for calc. It's still a little-known feature though!

[Julian Berman]

Patrick Massot said:

It is used by the conv? or calc widgets for instance.

Got it, OK, I suspect it's probably not too difficult to get working but I don't have time to look today, and probably it needs a small bit of thought for what the UI should be in nvim to replace shift+click. I guess some text objects to add regions to the ones you're selecting, and then some way to clear them, kind of like how the quickhl plugin works. But have to try to use the widgets to see. Maybe later in the week.

[Francisco Giordano]

suffices by doesn't update the infoview properly. is this a lean.nvim issue?

example:

example (h : p ∧ q) : q ∧ p := by
  have hp : p := h.left
  suffices hq : q by
    -- cursor here
    exact (And.intro hq hp)
  exact And.right h

putting the cursor in the line after by doesn't add hq as a hypothesis. it does immediately after by though

[Damiano Testa]

This has been brought up also for VSCode, not just for lean.nvim.

[Julian Berman]

Julian Berman said:

Patrick Massot said:

It is used by the conv? or calc widgets for instance.

Got it, OK, I suspect it's probably not too difficult to get working but I don't have time to look today, and probably it needs a small bit of thought for what the UI should be in nvim to replace shift+click. I guess some text objects to add regions to the ones you're selecting, and then some way to clear them, kind of like how the quickhl plugin works. But have to try to use the widgets to see. Maybe later in the week.

I looked at this briefly this afternoon and I still don't quite see how it works in VSCode. I see which RPC method is used to get the available widgets, and added support for it to neovim, but I still don't see where the data on what is selected actually gets sent rather than just collected. Will see about having another look when I get some more spare cycles.

[Patrick Massot]

I’m sure @Gabriel Ebner or @Wojciech Nawrocki can easily answer this question.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

still don't see where the data on what is selected actually gets sent rather than just collected

I'm not entirely clear on what you mean by 'sent' and 'collected'; in general, the selection (more or less an array of the selected terms) is passed as a prop to the main function of the JS code of each widget that is currently being displayed. Widgets can then choose to do whatever they want with it. A widget written with mk_rpc_widget%, such as the conv one, will proceed to call the RPC method that was used to define said widget with the new selection data and then display the HTML reply.

[Julian Berman]

Aha I was afraid of that. So the actual data gets passed across the JavaScript boundary (to the thing that VSCode execs from getWidgetSource) rather than back to the server?

[Julian Berman]

If so that makes this nearly impossible to implement, or at least means it's time to head back to investigating embedding a JS engine :/

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yep, the ability to run JS is pretty fundamental to some more sophisticated widgets. That said, any widgets implemented with mk_rpc_widget% will send the data right back to the server (here is the logic) which you could theoretically reimplement in vim. Though it would be relying on an implementation detail that may change at any point :/

[Julian Berman]

Yeah I mean I certainly expected to run into this if I tried to integrate with "fancy widget that renders a rubik's cube and lets you move it", but less so for this where it seems like JS doesn't need to be involved at all

[Julian Berman]

Will have to put this on the back burner, I'm sure any of 1) try out a JS engine and/or shadow DOM in the background, 2) proceed down that implementation detail path or 3) try to special case the specific JS source code for mk_rpc_widget% is an avenue forward but it's not a "hour and then it's working" one. Will give it another shot though at some point. Thanks for the info.

[mars0i]

This is a long thread! Is the idea that all lean.nvim questions and discussion should goes here? I've been posting about lean.nvim in "new members", because I'm just figuring things out with my Lean config.

[Julian Berman]

I think either way is fine -- I occasionally stick small announcements in this one mostly so that people who don't care about nvim can have muted this thread, but yeah I don't think it's a problem if you create new ones.

[Julian Berman]

Random plugin tip which I just discovered myself last week. aznhe21/actions-preview.nvim is nice, it will show you previews of what a code action will do before you apply it (via telescope). Here for instance is what it shows for some simple simp try this replacement:

output.gif

[Matthew Ballard]

With the update to lake in v4.8.0-rc1, I am getting some papercuts.

For example, when jumping into a new file, I will still get a Building ... message which amusingly changes when moving the cursor. If I try to active the language server before it finishes, nvim freezes.

[Patrick Massot]

I also noticed weird behavior

[Henrik Böving]

The building is not lean.nvim but lake

[Matthew Ballard]

So people are seeing this in VS Code also? I didn't notice any messages like that

[Patrick Massot]

I did not try in VSCode yet.

[Henrik Böving]

I don't know if they are seeing it in vscode but if you run lake build on the command line afte changing one file you will see that it spits out many build lines. This is a known lake regression, it is also known how this happens.

[Matthew Ballard]

Oh

[Henrik Böving]

Note that lake is not actually building, it merely prints too early that it is bulding

[Henrik Böving]

Only to then notice that in fact, there is nothing to build

[Matthew Ballard]

I also miss the cascading build output but that is off topic

[Julian Berman]

I don't have any real time to dig into anything today but if there's consensus something needs looking into I'll try to have a look once things settle down a bit.

[Matthew Ballard]

It sounds like we wait for changes to lake for now

[Anne Baanen]

This is probably just user error, but I'm noticing that importing a file with a lot of trace output (e.g. set_option trace.profiler true) causes nvim to take up a huge amount of cpu power before the server can start building the file itself. I don't particularly care about the trace output of files I'm importing, so is there any way to hide this information and not have it slow down my nvim so much?

[Julian Berman]

That sounds like the sort of thing that shouldn't differ (fingers crossed) between nvim and VSCode (in the sense that I can't think of anything we'd particularly be doing for trace output different from any other retrieved state) -- can you check if you see similar behavior in VSCode perhaps?

[Julian Berman]

If the answer is no I can do some profiling to see what's up.

[Matthew Ballard]

Is this because lake is now more verbose on loading things in general?

[Anne Baanen]

Just tested this on VS Code and it doesn't seem (particularly) slow. I also didn't see any trace output in the infoview, only the [1305/1306] Compiling Mathlib.Whatever.Filemessages.

[Julian Berman]

Huh. Interesting. Does VSCode not show trace output at all? Or put it somewhere else?

[Julian Berman]

I can try to have a look but not before Sunday most likely.

[Patrick Massot]

I also saw vim being completely frozen while lake is working, which never happened to me with VSCode.

[Matthew Ballard]

Things seem much better (and prettier!) with v4.8.0-rc2

[Julian Berman]

Are the freezes fixed?

[Matthew Ballard]

One data point but yes. I think the output from lake was overwhelming the buffer.

[Julian Berman]

Interesting, OK, I wonder / worry whether the latter is some other (albeit less pressing) issue then.

[Julian Berman]

Have you ever looked at any gigantic traces and noticed similar issues?

[Matthew Ballard]

Maybe in the past. Those truncate the unfolding now so it’s less often you see a giant dump.

[Matthew Ballard]

It appears that vim.lsp.client has had its fields rearranged. get_language_id moved out from under config and up to the same level directly under client. https://github.com/Julian/lean.nvim/pull/336

Not sure how the tests are broken...

[Julian Berman]

There's some other change in 0.10 that I haven't had a chance to look into... from what I saw in the half hour I gave it previously, it's something only broken in the tests, not in real life. So, the best kind of broken.

[Julian Berman]

We also seem to have no test for restart_file obviously which is how we don't notice that change, but that should hopefully be easy to add. I merged your PR for now, thanks for noticing!

[Anne Baanen]

The build logs appear a lot faster indeed, that's very good! The trace output seems to be as slow as ever unfortunately. :(

[Anne Baanen]

I forgot to say last time: In case it matters, I'm using nvim-qt under X11 on Arch Linux.

[Julian Berman]

Anne can you give me some simple-ish thing which reproduces the slowness for you, I can at least see if nvim profiling says anything useful

[Anne Baanen]

Looks like putting a set_option trace.profiler true above any expensive file in Mathlib (i.e. one of the top files listed here ordered by "value"), then importing it from a test file would work.

[Anne Baanen]

Actually doing it with the most expensive file, Mathlib.RingTheory.Kaehler, takes a minute or so on my machine before it starts the actual trace output, so presumably you might want to try out a medium-slow file first.

[Anne Baanen]

So explicit repro steps;

• Open a file in Mathlib (e.g. Mathlib.RingTheory.Kaehler)
• Add a line to the top set_option trace.profiler true
• Don't close the buffer or run lake build
• Make a new file test.lean with the contents:

import Mathlib.RingTheory.Kaehler

#eval "... trace output done!"

• See that vim displays the trace output on the import line extremely slowly.

[Matthew Ballard]

It don't see any trace output now but it is quite slow.

[Matthew Ballard]

It seems very slow without the tracing though

[Julian Berman]

I too see no trace output in test.lean. I happened to pick Mathlib.Analysis.Calculus.ContDiff.Defs -- on my machine here simply opening that file and waiting for it to finish processing / have the yellow bars disappear takes ~38.5 seconds (timed by hand) -- but that time is the same trying it a few times both in VSCode and neovim, so that's.. "good" at least.

[Julian Berman]

Next will try again with set_option trace.profiler and just see how long it takes, and assuming you're right that it's much slower in neovim will try to see if I can tell why.

[Julian Berman]

I hope this message affects precisely no one, but I have just removed Lean 3 support from lean.nvim to shed some lines of conditional code. There is a lean3 git tag on the last commit containing Lean 3 support, should any future time traveller need Lean 3.
lean.nvim's test suite passes, and a few minutes of manual playing seems to reveal nothing horridly broken, so I believe I've done the surgery correctly, but feel free to raise issues if anything seems amiss.

[Shanghe Chen]

Hi is there some specific logic in the implementation of semantic highlight of lean.nvim? Here Marc says there is some subtlety

when the client requests the semantic tokens for the full file, we instead only provide it with the semantic tokens up to the current point of elaboration. Unfortunately, now the client thinks that it knows all the semantic tokens, so it will not request the semantic tokens again for a while.
To make the client re-request the semantic tokens, we send a workspace/semanticTokens/refresh server to client request every couple of seconds so that the client re-requests the set of semantic tokens for the current point of elaboration in the file.

but checking the codebase of lean.nvim I saw no handle for this.

[Julian Berman]

I'm not intimately familiar with that part of LSP but from what Marc mentioned it doesn't sound like lean.nvim would have to do anything special to benefit from that

[Julian Berman]

(I assume you're asking because you were working on another editor, right? Not because you're seeing highlighting issues?)

[Julian Berman]

But yeah if it's a server-to-client request I'd assume that neovim's normal LSP handlers are attached to it and will handle re-running the highlighting, so there's nothing specific to lean.nvim that would need to fire.

[Julian Berman]

I happen to be looking into something unrelated at the minute, but just because I see it in the debug logs, it does indeed seem like everything works fine there, I see:

[DEBUG][2024-07-17 16:35:20] .../vim/lsp/rpc.lua:408    "rpc.receive"   {  id = 0,  jsonrpc = "2.0",  method = "workspace/semanticTokens/refresh"}
[TRACE][2024-07-17 16:35:20] ...m/lsp/client.lua:1017   "server_request"        "workspace/semanticTokens/refresh"      nil
[TRACE][2024-07-17 16:35:20] ...m/lsp/client.lua:1020   "server_request: found handler for"     "workspace/semanticTokens/refresh"
[TRACE][2024-07-17 16:35:20] ...lsp/handlers.lua:711    "default_handler"       "workspace/semanticTokens/refresh"      {  ctx = '{\n  client_id = 1,\n  method = "workspace/semanticTokens/refresh"\n}'}

which looks like it's neovim just handling things.

[Shanghe Chen]

Yeah thanks for the helpful information! The client I am using seems not handling this but the hightlight seems not bad though.

[Patrick Massot]

In the VSCode extension, when you see a unicode character in a Lean file, the tooltip explains how to type it using the abbreviation mechanism. Is there anything similar in lean.nvim?

[Chris Henson]

Patrick Massot said:

In the VSCode extension, when you see a unicode character in a Lean file, the tooltip explains how to type it using the abbreviation mechanism. Is there anything similar in lean.nvim?

<LocalLeader>\\ shows how to type the symbol under the cursor

[Patrick Massot]

Thanks, but it doesn’t seem to work here. Are you sure this isn’t a mapping you configured?

[Patrick Massot]

Sorry, it does work

[Patrick Massot]

I was doing something wrong.

[Patrick Massot]

It a really strange mapping but I can remap it.

[Austin Letson]

How do you view the type of a visual selection in lean.nvim? I am looking for essentially the behavior of selecting text and hovering in vscode.

[Julian Berman]

Does the selection bit actually do anything "special" in VSCode? I'd doubt it but I could be wrong.

[Julian Berman]

Specifically I think it will still just show you the hover for whatever your cursor ends up hovering over, regardless of what's visually selected

[Julian Berman]

In which case the answer is vim.lsp.buf.hover() -- you could add a visual mode mapping for that if you use visual mode a lot (though if you're OK with me saying so I'd avoid it for vim reasons generally, it's usually better to use a motion)

[Julian Berman]

Specifically, you'd add vim.keymap.set('v', 'K', vim.lsp.buf.hover) somewhere in your LspAttach or generally in your nvim setup.

[Chris Henson]

Julian Berman said:

Specifically I think it will still just show you the hover for whatever your cursor ends up hovering over, regardless of what's visually selected

I think this is correct. I could easily see the hover for certain whitespace leading to the misconception that the selection matters.

[Austin Letson]

Chris Henson said:

Julian Berman said:

Specifically I think it will still just show you the hover for whatever your cursor ends up hovering over, regardless of what's visually selected

I think this is correct. I could easily see the hover for certain whitespace leading to the misconception that the selection matters.

Ah, yes. I believe this is right. I was mistaken about the selection mattering.

[Austin Letson]

Julian Berman said:

In which case the answer is vim.lsp.buf.hover() -- you could add a visual mode mapping for that if you use visual mode a lot (though if you're OK with me saying so I'd avoid it for vim reasons generally, it's usually better to use a motion)

Got it. I have this mapped and use it in normal mode but was in visual mode because I mistakenly thought it would matter. However, I am always open to vim tips of any sort and will think twice next time I use visual mode.

[Chris Henson]

Unrelated question. Is there any easy way to enable just the lean.nvim Unicode abbreviations for other file extensions?

[Julian Berman]

Not right now but it has been requested in the past. It honestly wouldn't be hard to make it work, all the abbreviation code lives in one file. I honestly can't promise to make any time to do it, but certainly would accept a PR, or you're certainly welcome to open an issue (or comment on the one I closed because no one had asked for it in awhile and I'll reopen it) and I may get to it on a rainy day.

[Chris Henson]

Julian Berman said:

Not right now but it has been requested in the past. It honestly wouldn't be hard to make it work, all the abbreviation code lives in one file. I honestly can't promise to make any time to do it, but certainly would accept a PR, or you're certainly welcome to open an issue (or comment on the one I closed because no one had asked for it in awhile and I'll reopen it) and I may get to it on a rainy day.

Assuming I can figure it out, I'd be willing to make a PR. Does it sound reasonable to add an option to abbreviations of what patterns should be included for the autocommand?

[Julian Berman]

Chris Henson said:

Does it sound reasonable to add an option to abbreviations of what patterns should be included for the autocommand?

I think that sounds like a decent idea yeah -- though perhaps another route is we could have a require('lean.abbreviations').attach() or whatever we name it, and that function call is something you (anyone) could run in a ftplugin file which would attach/enable the autocmds for expanding abbreviations (so you'd put require(...).attach() in ~/.config/nvim/after/ftplugin/julia.lua, say). And then the existing Lean enablement is just an automatic call to that function for Lean.

[Chris Henson]

For anyone else interested in this feature of lean.nvim abbreviations in other file types, my PR to allow this was just merged. Adding something like require('lean.abbreviations').enable('*.txt', {}) is the syntax. Thanks for being friendly to new contributors @Julian Berman!

[Patrick Massot]

Since we are discussing lean.nvim, something that I really miss from VSCode and shouldn’t be too hard is the ability to see how much of the current Lean file has been processed and how far the processing frontier is from my cursor. In VSCode this is shown in the tiny column at the right of a file.

[Julian Berman]

Would you be happy with just a numeric representation?

[Patrick Massot]

Yes, having the information in the status line would already be very helpful.

[Patrick Massot]

Also, I am still using the code from https://github.com/Julian/lean.nvim/issues/43#issuecomment-1850633100 to close the infoview, but it now triggers a deprecation warning in my config. I tried to fix it. I managed to remove the warning but it also removed the functionality…

[Julian Berman]

(back in a few minutes but can you share the deprecation warning -- I assume it's one about get_option which should be easy to fix, I can post a fixed version to the issue)

[Patrick Massot]

The deprecated bit is vim.api.nvim_buf_get_option

[Julian Berman]

I hadn't seen Stephen's comment at the bottom there, but just modifying the comment you linked:

      local group = vim.api.nvim_create_augroup('LeanAutoOpenClose', {})

      vim.api.nvim_create_autocmd('BufWinEnter', {
        group = group,
        pattern = {'*.lean'},
        callback = function ()
          require('lean.infoview').open()
        end
      })

      vim.api.nvim_create_autocmd({'BufWinLeave', 'QuitPre'}, {
        group = group,
        pattern = {'*.lean'},
        callback = function()
          local infoview = require('lean.infoview').get_current_infoview()
          if infoview then
            local tab_wins = vim.api.nvim_tabpage_list_wins(0)
            local lean_wins = vim.tbl_filter(function (w)
              local buf = vim.api.nvim_win_get_buf(w)
              return vim.bo[buf].filetype == 'lean'
            end, tab_wins)
            if #lean_wins <= 1 then
              infoview:close()
            end
          end
        end
      })

should both remove the deprecation warning and preserve the functionality from what I see quickly here (vim.bo[bufnr].foo is the replacement for vim.api.nvim_buf_get_option(bufnr, 'foo') essentially). Let me know if that works.

[Patrick Massot]

It seems to work, thanks!

[Patrick Massot]

Having this done by the extension without further tweaking would still be nice if you have time for it.

[Julian Berman]

I agree, it's on the shortlist to do so I'll work on it next most likely.

[Patrick Massot]

And indeed I didn’t see Stephen’s comment that should probably be taken into account.

[Julian Berman]

How do I make Lean spend a bunch of time processing in the middle of some file?

[Julian Berman]

Just to delay long enough to ensure I'm telling you the right thing for your processing question

[Julian Berman]

Will sleeping make it process...

[Julian Berman]

Yes it seems so, never mind.

[Julian Berman]

I've pushed a basic version of what's needed for your processing percentage Patrick, you can update and try it out via e.g. :lua vim.notify(("%.f%% Processed"):format(require'lean.progress'.percentage())).

[Julian Berman]

Let me know if that does what you expect -- how exactly to add it to your status bar depends a bit on which/whether you use a status bar plugin.

[Patrick Massot]

This is already very nice. It still misses the information about how far from the cursor is the processing (the visual indication in VSCode is really efficient for that, a text indication seems harder to get concise enough).

[Patrick Massot]

I use nvim-lualine/lualine.nvim but I think this is simply the default from kickstart, so I wouldn’t mind changing if this makes things easier.

[Julian Berman]

I have to look at VSCode to see what it does a bit more carefully to know what the exact right UX seems like but it sounds like adding a sign column indication in neovim might be a nice way to do the cursor bit.

[Julian Berman]

Patrick Massot said:

I use nvim-lualine/lualine.nvim but I think this is simply the default from kickstart, so I wouldn’t mind changing if this makes things easier.

I honestly am not a heavy status line user, but I just switched to lualine a few minutes ago to see -- here's an example how you use that function with lualine https://github.com/Julian/dotfiles/commit/b4b16c1d687cede64782cce7f0f951ca9197a972
Note that the refresh rate is not immediate -- I'm not sure what the idiom is for this, doing it on user behalf would seem impolite, as refreshing the statusline slows down other important stuff (actually.. doing stuff). You can increase it obviously yourself if you do want more granular counting though.

[Julian Berman]

(n.b. I'm a little confused that lualine's docs don't say how to add components per filetype other than via that extension mechanism, which is kind of janky and seems to replace the entire status bar. That's a seemingly funny omission to me, but I may just be missing something obvious. I've probably exhausted the amount of time for the moment on playing with it but perhaps it's worth a bug/doc request report on the repo at some point.)

[Julian Berman]

One note on the "cursor frontier" bit which occurred to me while looking at lean.nvim's progress code -- something is going to need to change once Lean does not process files sequentially anymore -- what do you want to see in this case Patrick? (I suppose VSCode will have the same question if it doesn't already choose some behavior there)

[Julian Berman]

Do you want to see the distance to the closest progress block? The furthest? Or is VSCode happy there because you can see the "distribution" of where your orange bars are quickly?

[Patrick Massot]

In Lean 3 we could very clearly see the parallel processing, and this was rather cool (but not really useful).

[Julian Berman]

OK, thanks to Patrick and Eric on the last community call, I've just pushed a first version of showing remaining goal states for apply? and other trythis widgets. I have not tested it heavily, and the UX can still be improved, but having the info available immediately seems better than not. If you notice any errors or have improvement suggestions, please let me know. Ultimately I think doing a telescope previewer for this seems like the right next step. Here's what you should see:

Screenshot-2024-08-11-at-12.05.17.png

[Julian Berman]

(Note that selecting a suggestion still goes via vim.lsp.buf.code_action() or your preferred code action plugin.)

[Julian Berman]

Productive day -- I've also just pushed a satellite.nvim extension for showing document-wide progress information.

Patrick this hopefully gives you what you want for cursor info. Here's what it looks like, though the gif export I used has somewhat choppy framerate:

Screen-Recording-2024-08-11-at-17.07.40.gif

What you should see is a right sidebar which shows, top to bottom, progress information for the document -- this should look familiar, it's similar to what we had already, but now what you see represents the entire document, rather than just the visible lines.
It shows where your cursor is, what fraction of the document is visible (both of those are builtin satellite features) and then orange bar overlays for what section of the document is being processed by Lean (that's new/lean.nvim's doing clearly.) In the GIF the cursor position is the (tiny) blue box in the right bar, and the visible document portion is a slightly lighter background color -- again this is a bit hard to see in the recording, but locally it should be visible.

If you install satellite.nvim, e.g. by adding

{
  'lewis6991/satellite.nvim',
  event = 'BufReadPost'
}

to your lazy.nvim setup, everything should just immediately work. I've made this disable our existing progress bars if present, because the information is a bit redundant, but if you don't want this, nothing should have changed for you. Feedback again welcome.

[Patrick Massot]

Thank you very much Julian! It looks great!

[Patrick Massot]

I’ll try right now.

[Patrick Massot]

It seems to work great!

[Patrick Massot]

The apply? thing is a great start but clearly we need that telescope list with the refine invocations and the new goals are preview.

[Julian Berman]

Great! Yes you'll have it (soon hopefully) don't worry :)

[DSB]

Hello everyone. I had lean.vim working fine with my neovim config (I use lunarvim). But out of nowhere, it stopped working. I've tried updating Lean, and now I get the following error whenever I try to modify a .lean file within neovim:

Error executing lua callback: ...arvim/site/pack/lazy/opt/lean.nvim/lua/lean/infoview.lua:1088: attempt to call field 'iter' (a nil value) stack traceback: ...arvim/site/pack/lazy/opt/lean.nvim/lua/lean/infoview.lua:1088: in function <...arvim/site/pack/lazy/opt/lean.nvim/lua/lean/infoview.lua:1087>

Any ideas on what might be going on? Btw, I'm using a Mac.

[Julian Berman]

You're on neovim 0.9

[Julian Berman]

Presuming you installed it via homebrew, update.

[DSB]

Like a charm! Thanks @Julian Berman !

[mars0i]

Can anyone suggest some neovim/vim colorschemes that work well with Lean on a white background?

Or, in this code

def myfn (arg : Nat) := arg + 1

does anyone know what the neovim/vim syntax category is for arg on both the left and right? The syntax categories are coming from the Julian/lean.nvim plugin in file "lean.nvim/syntax/lean.nvim.

I can see the syntax categories in that file, and see what colors they're mapped to by running

:so $VIMRUNTIME/syntax/hitest.vim

but none of my experiments changes the color of the arg variable or anything in that position. (It's a light gray--nearly invisible on a white background.)

[Julian Berman]

does anyone know what the neovim/vim syntax category is for arg on both the left and right?

You can see this with :Inspect -- put your cursor where you're curious and run that command -- there can be 2 different sections in the output -- the top will show you if lean is sending back "Semantic Token" information for where you are, and the bottom is what we use when there's no semantic token info which is the syntax file you saw.

[mars0i]

Thanks @Julian Berman! I didn't know about that--it's incredibly useful.

I'm still stuck, though. :Inspect with the cursor on arg says that it's a leanEncl, but changing the color of leanEncl only changes the color of Nat. :Inspect also says, at that location,

@lsp.type.variable.lean links to @variable priority: 125

I'm not sure what to do with that.

(lean.nvim includes this line syn keyword leanCommand variable, but I assume that just means that what Lean considers a variable should be colored using the leanCommand category, but the color of arg doesn't change when I change the color of leanCommand, though a lot of other things change color, as I would expect).

[Julian Berman]

(I'll look more closely in a bit after clearing off a few other things from my yak stack)

Just to explain the last line though -- syn keyword leanCommand variable this specifically affects how the word variable itself is colored

[mars0i]

Oh, interesting.
Thanks!

[Julian Berman]

Sorry, I should learn to read messages instead of just skimming them too. On @lsp.type.variable.lean -- don't be scared by the @ signs.

[Julian Berman]

leanEncl is saying (slightly obtusely) "you're on top of an enclosed thing". @lsp.type.variable.lean is telling you "you're also on top of a syntax element whose name is @lsp.type.variable.lean", and it's telling you that the way nvim knows to color that is that "color it the same way as we color @variable" -- again don't be afraid of the @ sign it's just a thing internal neovim highlight groups prepend for namespacing.

[Julian Berman]

So what I would try there is you can change the color of one or both @lsp.type.variable.lean (if you just want to affect Lean) or @variable if you want to change how nvim colors variables across all your programming languages.

[Julian Berman]

If you want concrete reccs, I only use light backgrounds ~2% of the time -- I use https://github.com/rebelot/kanagawa.nvim which I don't think I've had any major complaints with (on either light or dark). gruvbox I suspect should work fine, as would https://github.com/folke/tokyonight.nvim, or any of the "even somewhat popular" neovim color schemes -- but if you're using one and it still doesn't have enough contrast feel free to share which one you use.

[Julian Berman]

Possibly more generally we should color variables inside binders differently than variables externally, or at least make it easy to do that -- but I think it's the Lean server that should really do that and I'm not sure if they want feature requests on semantic highlighting at this point.

[mars0i]

@Julian Berman, thank you so much! I had no idea that I could directly apply the hi command to those @-names. That worked. What a relief. (I kind of accidentally upgraded neovim from 0.9.x to 0.10.1, and that changed the syntax coloring so that some of the terms were nearly unreadable--no idea why--and didn't really want to go back to 0.9.x. On another computer I'm still on 0.9.5, and the coloring is fine.)

I'll try out those syntax files, too. Thank you.

[mars0i]

I'm trying to figure out how to make the Infoview window default to opening as a horizontal window below the first source code window. I saw this on the main page for lean.vim:

-- Set infoview windows' starting dimensions.
-- Windows are opened horizontally or vertically depending on spacing.
width = 50,
height = 20,

I've experimented with those settings by adding e.g. this

 \ infoview = { width = 100, height = 10 },

to lua require('lean').setup{ ... } in my startup file. I get a width change, but the Infoview window is still on the right. I looked around in the wiki as well. What does "depending on spacing" indicate? Thanks!

[Julian Berman]

Are you trying to make it always be horizontal?

Here's the precise logic at the minute: https://github.com/Julian/lean.nvim/blob/main/lua/lean/infoview.lua#L117
Basically it's vertical if there's more vertical space than horizontal with some constant factor.

It's been previously requested to have more control over the dimensions and direction but nothing else exists yet there -- you cane though add things to your ftplugin files to move it wherever you want after lean.nvim opens the window as a workaround.

[mars0i]

Well, yeah, I want to start with it horizontal. I might make it vertical during editing in some contexts. OK--thanks. I'll play around with that.

[mars0i]

It wasn't working for me, but I figured it out. The horizontal Infoview appears when I start nvim in a narrow terminal window, but I normally run nvim in a GUI wrapper, goneovim. The Infoview was ending up on the right no matter how narrow and tall the goneovim window was. The problem seems to be that the goneovim window dimension-setting happens too late, and lean.nvim was unaware of the window dimensions. I've identified a workaround, though, and I'll play around with my configuration. Thank you @Julian Berman!

[Alexander Dunlap]

Is there a way to get lean.nvim to wrap the hints that show up in the main window? They are getting cut off at the end of the screen for me -- e.g. here I would like to see the rest of the phrase "declaration use". New user here, thanks for the help.
image.png

[Patrick Massot]

I don’t know the answer to this question, but do you know that you can see the message in a floating window using vim.diagnostic.open_float?

[Patrick Massot]

For instance you can put somewhere in your config vim.keymap.set('n', '<leader>e', vim.diagnostic.open_float, { desc = 'Open floating diagnostic message' })

[Julian Berman]

That's the usual answer to this question yeah (use a float). If you want this to happen automatically, I'll just note you can also add an autocommand which automatically opens the float if you don't move your cursor for a second. E.g. by adding:

vim.api.nvim_create_autocmd({ 'CursorHold', 'CursorHoldI' }, {
  buffer = 0,
  callback = function()
    vim.diagnostic.open_float { header = '' }
  end
})

to your init.lua (to do it for all languages -- in that case don't add the buffer = 0) or ~/.config/nvim/after/ftplugin/lean.lua (to do it just for Lean).

And the "magic terminology" to know is that neovim calls that "virtual text".

[Julian Berman]

mars0i said:

It wasn't working for me, but I figured it out. The horizontal Infoview appears when I start nvim in a narrow terminal window, but I normally run nvim in a GUI wrapper, goneovim. The Infoview was ending up on the right no matter how narrow and tall the goneovim window was. The problem seems to be that the goneovim window dimension-setting happens too late, and lean.nvim was unaware of the window dimensions. I've identified a workaround, though, and I'll play around with my configuration. Thank you Julian Berman!

That sounds suspicious. Sounds maybe like a goneovim bug but not sure without trying, I haven't used a GUI neovim in a very long while, but if you do a small bit of diagnosing, probably happy to see you file an issue (even on lean.nvim) to see if we should do some workaround maybe.

[Alexander Dunlap]

thanks a lot!

[Julian Berman]

(Please complain if you have general feedback! Especially about things I should be adding to the still-in-progress Manual which I promise to put some more work into the next week or two.)

[mars0i]

Julian Berman said:

That sounds suspicious. Sounds maybe like a goneovim bug but not sure without trying, I haven't used a GUI neovim in a very long while, but if you do a small bit of diagnosing, probably happy to see you file an issue (even on lean.nvim) to see if we should do some workaround maybe.

Probably a goneovim code design decision rather than a bug per se. The window size gets set by goneovim according to its settings.toml file, which is loaded after the regular nvim config files. So to get goneovim to set the window size, I run set columns=N and set lines=M from goneovim's settings.toml. Running set columns=N and set lines=M before that point is overridden when goneovim configures its window. lean.nvim, I would guess, runs before that point, so it doesn't know that goneovim is going to change the window size.

The workaround is just to also set the columns and lines in my nvim startup file (.vim/vimrc in my case). Then lean.nvim knows what the window size is supposed to be, and later goneovim will set the window to the same size in response to seeing the set columns/lines when settings.toml is read.

[mars0i]

I could run everything in vimrc directly from goneovim's settings.toml, I guess, but I prefer to run most of my configuration from a single file that is shared by various configurations of nvim and vim.

[Julian Berman]

It seems like the two logos were asking for it to happen, so lean.nvim has a logo now:

image.png

You'll find it in the README.

[Henrik Böving]

Stickers when!

[mars0i]

You can get Lean t-shirts on the web (e.g. Redbubble). Now I want a lean.nvim shirt.

[mars0i]

I ran PlugUpdate (vim.plugged's update comment) and got a new version of lean.nvim. It's possible that I also made other changes to my configuration, but I don't think so. Is it possible that the latest version of lean.nvim is causing the following? (If not, I'm not sure what I did.)

E325: ATTENTION
Error detected while processing BufReadPost Autocommands for "*":
Error executing lua callback: ...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:24: Error executing lua: ...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:25: BufReadPost Autocommands for ""..FileType Autocommands for ""..function <SNR>1_LoadFTPlugin[19]..script /Users/mabrams/.vim/plugged/lean.nvim/ftplugin/lean/lean.lua: Vim(runtime):E5113: Error while calling lua chunk: ...rs/mabrams/.vim/plugged/lean.nvim/ftplugin/lean/lean.lua:26: attempt to call field 'iter' (a nil value)
stack traceback:
...rs/mabrams/.vim/plugged/lean.nvim/ftplugin/lean/lean.lua:26: in main chunk
[C]: in function 'nvim_cmd'
...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:25: in function <...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:24>
[C]: in function 'nvim_buf_call'
...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:24: in function <...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:10>
stack traceback:
[C]: in function 'nvim_cmd'
...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:25: in function <...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:24>
[C]: in function 'nvim_buf_call'
...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:24: in function <...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:10>
stack traceback:
[C]: in function 'nvim_buf_call'
...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:24: in function <...ocal/Cellar/neovim/0.9.5/share/nvim/runtime/filetype.lua:10>

[Julian Berman]

You're on nvim 0.9, which is EOL. Update to 0.10, or if you don't want to yet for some reason, use the nvim-0.9 tag with your plugin manager to pin lean.nvim to a version compatible with 0.9.

[mars0i]

Thanks @Julian Berman. Upgrading to 0.10.1 fixed it. (I orginally resisted upgrading--and forgot that my version was so behind--because of glitches with 0.10 on my other computer, but I've resolved those now.) Nice to know about the version tagging option.

[mars0i]

(Such a relief to have the nice, responsive interactive interface back. lean.nvim makes it distressing to find myself staring at a bare source code file when it stopped working.)

[Julian Berman]

lean.nvim v2024.9.2

Oh hello there.

A new release of lean.nvim is out. You should be able to update to it in whatever plugin manager you're using, e.g. via :Lazy update.

There's one 'big' feature and some small tweaks.
The bigger one is...

Infoview View Options

We now have configurable view options, a la VSCode.
This means you can dynamically hide hypotheses which are instances, types, or inaccesible names in the infoview.
You can also reverse the order of the goal state such that the goal is on top.

Here's a quick GIF:

Screen Recording 2024-09-28 at 16.gif

Some documentation for this configuration is in the Manual, but here's the tl;dr:

A new <LocalLeader>v mapping is now enabled within Lean files. It opens a window where you can hit <Tab> on each line to toggle the setting you're on top of. Hit <Enter> when you're done to confirm your choices, or hit K if you want a hover showing you more information about the setting.

Please provide any feedback!

Also... I'd love to hear if anyone has ideas for further filtering beyond these options!
Now's a good time for me to implement any such ideas, and I know the VSCode functionality hasn't really changed since it was introduced, so perhaps if you deal with proofs with lots of hypotheses often, you have suggestions for other things we could configurably filter!
Feel free to post them!

Other Changes

• Did you know that the conv tactic uses a different prefix (|) for showing goals in the infoview? I didn't. But now lean.nvim properly shows that prefix instead.
• Version numbers, clearly. Going forward, lean.nvim will have "releases". This really doesn't affect you as a user, it's at the minute simply an excuse to write up release notes when lean.nvim gets something new + notable.
• lean.nvim is now on Luarocks. Unless you plan on interfacing with Lean via Lua, you probably don't care about this either.

[mars0i]

I updated, and got this error:

lean.nvim:
error: Your local changes to the following files would be overwritten by merge:
doc/tags
Please commit your changes or stash them before you merge.
Aborting
Updating 2bbd5c9..c9ea0f9

I actually didn't realize that the plugin system was using git, but that makes sense. Not sure what I did to modify the tags file. Should I just git stash?

[Julian Berman]

I still don't really fully understand how all the plugin managers manage help tags. Which one are you using?

[mars0i]

VimPlugged https://github.com/junegunn/vim-plug

[Julian Berman]

You can try updating again, I just regenerated the tags -- if that still tells you your local repo is unhappy, yes you should just git restore doc/tags even and discard the local changes.

Most likely you didn't do anything yourself, vim-plug is autoregenerating the help tags, and people seem not to agree whether that file should be tracked or untracked in version control, so now it's unhappy that the upstream ones have changed.

[mars0i]

Updating gave the same error. I misread git restore doc/tags as git reset doc/tags, and did that, but then did git stash, and now the update works fine. Thanks. (Whatever I got rid of with the stash, I'm sure I can live with it.)

[Julian Berman]

(You didn't misread it, I mistyped it and edited the message, sorry! But glad it's working!)

[Jannis Limperg]

Julian Berman said:

Also... I'd love to hear if anyone has ideas for further filtering beyond these options!

Hiding all dependent hypotheses (i.e., all hypotheses on which another hypothesis depends) might be worth a try. It would get rid of a lot of α : Type and n : Nat.

[Chris Henson]

Will this release also be on nixpkgs?

[Julian Berman]

Hiding all dependent hypotheses

I like that idea a lot (I think I've been annoyed by it myself) -- but if I'm not missing something I think the server would need to help there ideally rather than only doing it on the editor side via what is sent right now, because it's hard to know whether seeing n somewhere in a hypothesis type is the n hypothesis. (Which isn't to say we can't do it, we've been playing with some stuff like that for other reasons).

[Julian Berman]

Chris Henson said:

Will this release also be on nixpkgs?

I actually have no idea who's maintaining the nixpkg setup, so I don't know I'm afraid, but hopefully whoever that is is following along? Let's see if I can at least find the nixpkg.

[Chris Henson]

Julian Berman said:

Chris Henson said:

Will this release also be on nixpkgs?

I actually have no idea who's maintaining the nixpkg setup, so I don't know I'm afraid, but hopefully whoever that is is following along? Let's see if I can at least find the nixpkg.

Oh interesting. It is named vimPlugins.lean-nvim.

[Julian Berman]

AFAICT in a few minutes of clicking around, it (the nixpkg) is automatically updated to follow the GitHub repo, and ends up e.g. here: https://github.com/NixOS/nixpkgs/blob/775816a01958f4161829fc15c9e8f3b78de0a8da/pkgs/applications/editors/vim/plugins/generated.nix#L5574-L5582

So tl;dr I think the answer is "yes it will end up in nixpkgs as soon as the autoupdater runs again".

[Chris Henson]

Julian Berman said:

So tl;dr I think the answer is "yes it will end up in nixpkgs as soon as the autoupdater runs again".

Great, thanks!

[Jannis Limperg]

Julian Berman said:

Hiding all dependent hypotheses

I like that idea a lot (I think I've been annoyed by it myself) -- but if I'm not missing something I think the server would need to help there ideally rather than only doing it on the editor side via what is sent right now.

Yes, that seems likely. It could be implemented as a pp option.

[Chris Henson]

Would it be possible to define folds for the terms/types in the infoview? Since I see there is already some highlighting happening it seems plausible at least. But maybe not that useful, because I assume any kind of persisting fold would be much harder or impossible to implement. Use case here is dealing with very large terms/types while doing category theory, other suggestions are welcome!

[Julian Berman]

Yes I've thought about this briefly, but not in full -- I think it needs some design thinking for how it should work, as you say. If you have thoughts... https://github.com/Julian/lean.nvim/issues/31 is the only somewhat related issue (I'll generalize the title to talk about all folds) -- but please share whatever example you'd like and how you'd like to be able to fold it!

[Robin Carlier]

On the topic of possible improvements to lean.nvim, something that would be pretty nice to add is support for unicode superscripts/subscripts with the <C-A> keymap (that increases by one the next number after the cursor on the line). I might try to PR it if I have time (I tried to play around with that a little bit, but lua 5.1's strings don’t support utf8 natively, so this is a bit awful to work with).

And by the way, I’m taking this as an occasion to say thanks for developping this plugin, this is a blessing!

[Patrick Massot]

@Robin Carlier you can take a look at my config, focusing on the use of dial and its configuration.

[Patrick Massot]

It shows you can get <C-A> to do what you want without any collaboration from lean.nvim.

[Robin Carlier]

Patrick Massot said:

Robin Carlier you can take a look at my config, focusing on the use of dial and its configuration.

I was unaware of this plugin, this seems to be exactly what I was looking for, thanks!

[Julian Berman]

That's a good snippet to add to the wiki -- if either of you gets time to do so please feel encouraged, otherwise I'll do it at some point.

[Chris Henson]

Julian Berman said:

Yes I've thought about this briefly, but not in full -- I think it needs some design thinking for how it should work, as you say. If you have thoughts... https://github.com/Julian/lean.nvim/issues/31 is the only somewhat related issue (I'll generalize the title to talk about all folds) -- but please share whatever example you'd like and how you'd like to be able to fold it!

I left a comment with some thoughts.

[mars0i]

Is there a lean.nvim function that will report the version of Lean being used to compile a buffer?

Or: Can I assume that running lean --version from the directory of the buffer's file (or maybe the directory from which I start nvim?) tells me which version of Lean nvim is calling out to?

(Some of the code in FPIL doesn't work with the latest versions of Lean. The current published version of FPIL was checked against Lean 4.1.0. But I'm still getting an error where the book doesn't predict and error, even though lean --version reports 4.1.0. This is for code that's not supposed to import any libraries explicitly.)

[Julian Berman]

Can I assume that running lean --version from the directory of the buffer's file (or maybe the directory from which I start nvim?) tells me which version of Lean nvim is calling out to?

No technically it's neither of those, lean.nvim will search for what looks like the project root (which usually means finding a lakefile.lean or lakefile.toml or lean-toolchain file), and then that's the directory you should try running --version from. Though technically it's lake --version you should check, as that's what will be run.

[Julian Berman]

You can also look at :LspInfo and :checkhealth lean, though I'm realizing probably the latter doesn't take this into account (i.e. it runs lake --version without taking into account the workspace. So that's a minor checkhealth bug I guess.)

[Julian Berman]

Also all the above assumes you have elan installed of course, and that you're not screwing around with some Lean version that may not match the project.

[mars0i]

Thanks @Julian Berman! This is what I needed to know.

(The only place I'm specifying the Lean version, afaik, is in lean-toolchain in the project root, and that corresponds to the Lean version that lake --version, lean --version report, and :checkhealth report. I tried this in two different project roots with different lean-toolchain contents. :LspInfo didn't report a Lean version.)

I do have elan installed, but I never invoke it directly. Maybe I should ask in a different channel about the relationship between lake and elan.

[mars0i]

Earlier I created an issue for FPIL at https://github.com/leanprover/fp-lean because I was getting a very different error than the one the book said I should get. David Christensen commented on my issue that this was happening because the current version of the book hasn't yet been updated for the latest version of Lean.

The first page of FPIL says that it was tested with Lean 4.1.0, but now that I seem to be running Lean 4.1.0, I'm getting essentially the same error message as with v4.13.0-rc3; the error is a syntactic variant is semantically the same afaics. So I am definitely using a different version of Lean, but it's still not giving me the error message that the book claims 4.1.0 should give.

I'm have some reluctance to update my issue with this new info if I'm not certain I running the code in Lean 4.1.0. I can't expect Christensen to test his code in nvim, and I could test it in VSCode, but I've avoided installing and setting up VSCode because I'd rather not use it. lean.nvim is so nice--why bother?

[mars0i]

I did decide to report the apparent-4.1.0 error in the FPIL repo (and didn't install VSCode.)

[Patrick Massot]

Never invoking elan directly is definitely correct. The whole point of elan is to stay in the shadow.

[mars0i]

fwiw the errors I thought were due to FPIL seem to be due to errors in my code. I'm glad to know how to check what version of Lean is running, though.

[Francisco Giordano]

Is there a way to get good automatic formatting/indentation?

For example the fields in a structure don't get indented for me. Neovim produces the following where I would expect x : Nat to be indented one level:

structure Foo where
x : Nat

[Francisco Giordano]

Just found this issue so I suppose this is an unsolved problem. Still curious if others struggle as much as me with their indentation or if there may be something particularly bad in my config

[Julian Berman]

Yeah -- automatic formatting the answer is definitely no, though that's something the community occasionally discusses just in general (and once a general autoformatter exists we can use it of course). But AFAIK no one is making forward progress on it at the minute -- it also will presumably have the "usual" problem that whitespace sensitivity has which is that it's ambiguous what whitespace is intended for a general piece of code, but ok, good is the enemy of perfect.

In terms of autoindenting -- that issue is indeed my reminder. We should I guess really put something basic in place at this point to do it. I wouldn't say I struggle with it but it's certainly annoying that it doesn't happen in Lean and does in every other language I use, so yeah I feel the pain.

[Francisco Giordano]

Would you go the treesitter route or some simpler logic for indentexpr?

[Julian Berman]

I tried the tree-sitter route with https://github.com/Julian/tree-sitter-lean. The grammar broke tree-sitter. It's possible it's worth another shot for the general case, but it's also possible it's worth simply giving up and doing something simpler but which still is as good as regexes (it's so much more maintainable than regexes).

[Utensil Song]

Is there an easy way to restart Lean LSP server(s) in NeoVIm? I know I can :LspRestart <Tab> but I'm seeing around 5 leanls because I'm hopping between Lean projects in one nvim instance, moving things around, and executed some lake command off UI.

[Utensil Song]

It would also be nice if there is a default key mapping for :LeanRestartFile etc. Do <LocalLeader>r and <LocalLeader>R sound reasonable for restarting file and restarting server?

[Julian Berman]

I can :LspRestart <Tab> but I'm seeing around 5 leanls because I'm hopping between Lean projects in one nvim instance

Is the one you want to restart a specific one? Just to check, you know :LspRestart with no arguments will restart the ones for the current buffer? The one you want to restart is some arbitrary other one?

It would also be nice if there is a default key mapping for :LeanRestartFile etc.

Yes that sounds OK to me, I'm surprised we don't have one already. If anyone else has an opinion feel free to mention (someone should double check what the mapping is in VSCode just out of curiosity -- and I know VSCode will autoprompt for restarting files in a way we don't do yet in lean.nvim mostly because I see how VSCode does that and it made me afraid :) but that also we should have at some point I guess.)

[Marc Huisinga]

The VS Code extension doesn't prompt you about restarting files anymore. It issues a sticky diagnostic that is visible in the full file and has a "Restart File" button in the InfoView that is visible at all times.

[Utensil Song]

Yes, I've been used to the restart file button in VSCode for a while, hence the question for nvim. BTW, the button is in the far bottom-right corner, away from everything else, which is weird in UX, but I guess the intention is to avoid cluttering infoview yet stay sticky.

[Marc Huisinga]

Yes, it's in the bottom right so it covers as little InfoView content as possible.

[Utensil Song]

Julian Berman said:

Just to check, you know :LspRestart with no arguments will restart the ones for the current buffer? The one you want to restart is some arbitrary other one?

Ha, I didn't know that, that's handy. Thanks for the tip!

[Julian Berman]

OK cool, so yeah my inclination would certainly be to add a mapping for LeanRestartFile but not for restarting the server entirely since that's a general neovim thing. A PR is certainly welcome, or else I'll do it later today.

[Utensil Song]

Indeed, the latter thing is a general neovim thing, and could be just a tip in the doc.

BTW, the general experience with lean.nvim is great and very smooth out-of-box, thanks for making this! :heart:

[Julian Berman]

Thank you I really appreciate that! Please do keep sending feedback on stuff you want to see.

[Francisco Giordano]

It would be great to have a "sticky" diagnostic in the InfoView when the file needs to be restarted. I only see it if I scroll to the top of the file at the moment.

[Utensil Song]

With trouble.nvim installed, I can see them in the bottom panel (toggled with <Leader>xx). It also helps me to walk through issues in the file, just like VSCode's Problems panel.

[mars0i]

I'm not sure whether to ask here this question here or in the "new members" category. It's about Lean functionality, but maybe there's a lean.nvim key mapping or command that I can use.

With recent versions of Lean at least (4.12, 4.13), when part of a type specification in my code includes a function application such as Nat.plusL n (k + 1), where n and k are Nats, the Infoview window describes the same function application as n.plusL (k + 1). I know that they're equivalent, but is there a way to configure this so that Infoview shows Nat.plusL n (k + 1)? The mental energy I devote to rearranging the variables in my head seems unnecessary, especially when I'm thinking about possible replacements for the n.

[Yaël Dillies]

attribute [pp_no_dot] Nat.plusL should do

[mars0i]

Thanks @Yaël Dillies. OK, so it's not a lean.nvim question. Nice that it's so fine-grained, i.e. function-specific. But I'm getting an error "unknown attribute [pp_no_dot]". Do I need to import a library or something like that? I don't know much about attributes.

[Yaël Dillies]

Ah sorry, the attribute is now called pp_nodot

[mars0i]

Ah, thank you @Yaël Dillies. (Such a relief to see the arguments after the function now, for this case. I'm not against prefix application in general.)

[Julian Berman]

lean.nvim v2024.10.1

Oh hello there. Another new release of lean.nvim is out! There are a few nice features included, as well as a nice announcement you should stick around until the end for :)
Here's what we have coming out of the oven:

Goal State Diffing

When the goal state changes in your proof, or as you introduce new hypotheses, Lean sends little hints saying which parts of your goal have changed.
These can be subtle (I didn't even notice them myself until they were pointed out) but they're very helpful for watching your proof state change.
lean.nvim now supports showing them as well:

goaldiff.mp4

The precise colors you see will depend on your color scheme, but the defaults should be good enough, as they're tied to the colors you should already see in other "diff" contexts.
If that isn't the case, please feel free to share your setup.

Diagnostic Widgets

lean.nvim previously supported interacting with hypotheses in the infoview (e.g. allowing you to click on a term you see and to see its type).
But now it properly renders some widgets within diagnostics, which are sometimes used by commands you may already be familiar with.
As a concrete example, here's what you should now see with the #find_home command:

diagnosticwidgets.mp4

(Note that in the screencast I'm hitting gd to jump to definition -- this is because the widget coming from #find_home is specifically one meant for jumping to a corresponding Lean module being shown).

Mapping Documentation

Neovim key mappings can be "self-documenting", in that when you run e.g. :map <LocalLeader>\\ they can tell you not only that this is mapped to some command or Lua function, but also some documentation about what the mapping does.
lean.nvim now sets this property for all mappings it creates.
In this particular case then, you'll now see:

n  <Space><Space>\ *<Cmd>LeanAbbreviationsReverseLookup<CR>
                 Show how to type the unicode character under the cursor.

where the second line is new.
Similar short descriptions are present for all of what lean.nvim binds both in Lean files as well as the infoview.

Those of you who use which-key.nvim (which actually doesn't include me :) should now see something other than a blank spot in your popovers, as it's this same property which is used to generate the text there.

FRO Sponsorship :tada: :tada: :tada:

I am really happy to be able to share that the Lean FRO has decided to sponsor me working on lean.nvim part-time for a short period.
Sincere thanks are definitely owed (to Leo, @Sebastian Ullrich and many others in the FRO!)
And of course some of the existing work these last 2 weeks already is a direct outcome.

While I feel like I have some decent sense of missing functionality that could be worked on in the coming weeks, please do take this as an official solicitation to share pain points and gaps.
I'll shortly share the list I have which I'm using to prioritize what to do next, but this list is malleable and definitely could use you (yes you!) throwing ideas in the hat to help me reorder priorities.

I'd like to sincerely thank all of you who use it for showing how much interest there is!
Undoubtedly it was instrumental in making this specific sponsorship happen, and bodes well for Neovim and Lean being long term friends.

Other Changes

• A default mapping was added for :LeanRestartFile (<LocalLeader>r). You of course are still free to map it to whatever you'd like if you prefer another mapping. Thanks to @Utensil Song for the contribution!
• Communication with the LSP should be slightly more reliable because we now do a few more retrys when we get a failure, though it's here that I actually want to make my next set of improvements.
• The infoview contains less trailing whitespace. This is something you may not have noticed if you're not as bothered by it as I am, but occasionally we would render extra empty trailing lines, and now we don't :)

Until next time Neovim friends.

---

You should be able to update using whatever plugin manager you're using, e.g. via :Lazy update.

[Johan Commelin]

Great updates! Very nice!

One thing I noticed a couple of days ago: how do I stop the Lean server from within nvim? In VScode you can Do Ctrl-Shift-P "LeanStop" and it will show you an option to stop the server. But in lean.nvim I could only find the restart option.

[Julian Berman]

The native way is :lua vim.lsp.stop_client(vim.lsp.get_clients()) which of course you can bind to a key if you'd like. There's also an equivalent :LspStop in nvim-lspconfig, which you have installed as it's a current dependency of lean.nvim though – small teaser – in the future it will become an optional dependency, as these days similar plugins (like rustaceanvim) are increasingly happy with the newer native Neovim APIs.

[Chris Henson]

Wow, it's great to see FRO support for this. Thank you for your work!

[Mario Carneiro]

Marc Huisinga said:

Yes, it's in the bottom right so it covers as little InfoView content as possible.

How about putting it in the status bar, where it used to be in lean 3? (It would give general status about whether the server is running and whether it is checking the current file or just up to the end of the visible region etc.)

[Mario Carneiro]

Currently I think the lean extension is not using the status bar at all

[Austin Letson]

It's so exciting to see the FRO supporting lean.nvim and the stream of improvements as a result! I am particularly excited about the goal state diffing. Thanks @Julian Berman!

[mars0i]

When I was learning Agda recently, there were some vim and nvim interfaces available, but it soon became clear that I'd probably just cause myself trouble if I didn't use the standard Emacs interface. (Of course I used the latest Emacs vi emulation, but you know that's never the same as the real thing, e.g. nvim.)

lean.nvim is so full-featured and amazing--i.e. Lean is amazing, and lean.nvim gives me access to its amazing features--that I never felt that I was using a second-class tool because it wasn't VSCode. @JulianBerman made lean.nvim first-class despite not having explicit support from the FRO. Now it's not just first-class in practice, but officially, and I'm glad that you're getting financial support for the project.

[Patrick Massot]

This is all great news! Displaying goal diff is really great. If I had to vote for the next daily life improvement, that would be smarter auto-indent that understand focusing bullets. I mean when I write

· apply stuff

and hit enter, I would love to get to the correct indentation level (aligned with a).

[Patrick Massot]

And of course the larger thing is the supporting selecting stuff in the goal like what Shift-click does in VSCode and getting access to all widgets that rely on this functionality. But this is probably a lot of work and many people only rarely use it.

[Julian Berman]

Thanks Patrick! OK this is good motivation to post the list I alluded to, even though it may not be fully coherent without some explanation. Let's try it as a poll. I'll note I'm not including a few bugfixes which I'm working on as well (notably two, which have to do with some slowness when we receive lots of diagnostics coming from Lean, and secondly I don't understand why Lean sometimes claims that Lean.Widget.getInteractiveDiagnostics doesn't exist as an RPC method and sends back an error, but we need to be catching that I guess, right now it can interrupt editing.)

So. Here's the poll:

[Julian Berman]

/poll What should be worked on next? (Feel free to vote for multiple.)
Autoindent support
Shift-click selection
Custom "Try this" code action previewer with goal state previewing
"Import out of date" indicators and optional automatic restarting
Try to make abbreviation expansion work even "across" normal mode entering (i.e. when the buffer contains literally \to)
Autoclose the infoview
Support jumping to arbitrary positions anywhere in the infoview via a hopping plugin (leap.nvim, hop.nvim)
Support for opening/reading some or all of #mil, #tpil, #ref

[Christian Merten]

Thanks for all the work on this! I just updated (from a pretty old version) and finally seeing build error traces in the info view is life changing.

I am regularly running into one issue though with the following error message:

Error executing vim.schedule lua callback: vim/inspect.lua:0: attempt to compare number with nil
stack traceback:
        vim/inspect.lua: in function 'putValue'
        vim/inspect.lua: in function 'putValue'
        vim/inspect.lua: in function 'putValue'
        vim/inspect.lua: in function 'putValue'
        vim/inspect.lua: in function 'inspect'
        /opt/nvim-linux64/share/nvim/runtime/lua/vim/lsp/rpc.lua:292: in function 'notify'
        /opt/nvim-linux64/share/nvim/runtime/lua/vim/lsp/client.lua:784: in function 'notify'
        ...ian/.local/share/nvim/plugged/lean.nvim/lua/lean/rpc.lua:101: in function 'release_now'
        ...ian/.local/share/nvim/plugged/lean.nvim/lua/lean/rpc.lua:115: in function ''
        vim/_editor.lua: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>

Do others encounter this?

[Julian Berman]

I didn't even mention fixing the build error issue but I agree :).
Can you share the output of :checkhealth lean

[Christian Merten]

==============================================================================
lean: require("lean.health").check()

lean.nvim ~
- OK Neovim is new enough.
- OK Lake is runnable.
- `lake --version`:
    Lake version 5.0.0-01d414a (Lean version 4.13.0-rc3)

[Chris Henson]

I'm not at a computer, but I've intermittently seen something similar to what @Christian Merten describes

[Julian Berman]

Interesting, I don't think I've seen that one so if anyone has any info on how it typically happens let me know, will have a look when I get a moment.

[Henrik Böving]

I do encounter this issue as well sometimes, to the best of my knowledge it usually happens when i am working in large files

[mars0i]

I voted for autoindent, which feels very valuable, but because I'm inexperienced, I don't understand the other items, so I can't vote for them!

(I also gather that full-fledged Lean code formatting is hard, but if the community will eventually come back this issue (i.e. this, I assume), maybe if lean.nvim included incremental, even kludgey advances in formatting, that would be OK since it would eventually be replaced in the end. I know that that's the sort of thinking that has sometimes led to major applications that are difficult to maintain, but the risk seems lower here.)

[Julian Berman]

Christian Merten said:

Thanks for all the work on this! I just updated (from a pretty old version) and finally seeing build error traces in the info view is life changing.

I am regularly running into one issue though with the following error message:

I couldn't immediately reproduce the RPC issue in a few minutes playing (so I'll have to play a bit more) -- but in the meantime I've pushed a commit to ignore errors coming from releasing RPC sessions -- this is "safe" in the sense that on the Lean side at worst all that happens is this leaks a bit of memory. For any of you getting this intermittently can you try updating the plugin and let me know if you see the error again afterwards?

[Utensil Song]

When using lean.nvim with trouble.nvim (similar to VSCode Problems panel), it would be nice if clicking on a Lean error message could go to the corresponding file and line, currently clicking on something like

 error: ././././LibraryName/FileName.lean:112:4: error message

in the diagnostic output has no effect.

[Julian Berman]

It seems like there's at least a clear winner for the top spot in the poll, so I'll play with autoindent next.

@Utensil Song would you mind opening an issue -- I don't use trouble.nvim, and it's not immediately clear what could be wrong (Lean has a kind of "fake" diagnostics that are interactive and require special implementation in editor plugins, but just clicking on the filename there shouldn't be anything special, that is probably just a regular diagnostic which trouble should support.) -- but those two things being said, I'm happy to look into it, I know lots of people like trouble.

[Utensil Song]

Filed Julian/lean.nvim#359 , I've added more description on reproducing the issue, it turns out that the issue only applies to errors in imports.

[Patrick Massot]

I updated lean.nvim and today I see a lot of Got a diagnostic from some other line number: "table: 0x7d3c778f4290" in the status line.

[Patrick Massot]

I didn’t check but I assume the hexadecimal number varies.

[Chris Henson]

Patrick Massot said:

I updated lean.nvim and today I see a lot of Got a diagnostic from some other line number: "table: 0x7d3c778f4290" in the status line.

I get this occasionally too, I think since the update before last. (Hadn't mentioned it because I wasn't sure how to reproduce.)

[Julian Berman]

Huh, I log those at debug level, so I expected no one to see them, but I'll hide them entirely later tonight.

[Julian Berman]

Patrick Massot said:

I updated lean.nvim and today I see a lot of Got a diagnostic from some other line number: "table: 0x7d3c778f4290" in the status line.

This is fixed, please update again and it should go away.

[mars0i]

Is there an autocomplete command function that I'm missing?

I'm not a big user of autocomplete in other languages--I find it annoying sometimes--and I haven't missed having it in Lean. However, the Lean manual's section on set_option says that you can get a list of options that can be set using autocomplete (in VSCode, I assume). Since I haven't been able to figure out where to get further information on set_option otherwise (do I have to go to the source?) , autocomplete would be useful for this kind of situation.

Maybe this is a standard LSP trick that I don't know--since I know very little about LSP.

[Julian Berman]

I am about to run out for the day, but the behavior for set_option completion does appear to work, although it's IMHO very slightly quirky -- specifically it seems to trigger if you start typing something (e.g. type set_option t and you'll see suggestions for options starting with t), but it does not simply show all options when you trigger it with nothing typed. Probably filing that as a bug might be worth doing on the Lean 4 repo if it's not already there.

[Julian Berman]

Anyways maybe you're asking a more basic question -- you need a completion library -- nvim-cmp is the current standard one, but I happen to be trying out blink.cmp myself the last week and it works pretty decently. Install one, and then if you choose nvim-cmp (or already have it) you want to also have https://github.com/hrsh7th/cmp-nvim-lsp installed which is completion for LSP (that Lean sends)

[Marc Huisinga]

This might be something that I've broken by accident fairly recently. Please report a bug.

[Christian Merten]

Since the new lean release, file compilation suddenly stops after a few minutes (sometimes seconds) of editing. Reloading the file lets me edit for another few minutes only for it to stop again. I just updated to the latest version of the extension, but the issue persists. Anything I can do about this?

[Julian Berman]

Hmm I haven't tried the new release yet but that sounds unfortunate. I'll have a look. No errors whatsoever?

[Christian Merten]

No errors that I can observe, can I make lean.nvim more verbose?

[Julian Berman]

If editing stops that would sound a bit like the LSP is crashing. You can use vim.lsp.set_log_level("DEBUG") to make Neovim a bit more verbose there (or "TRACE" to make it even more verbose) and then output will go to vim.lsp.log.get_filename(). In terms of internal lean.nvim logging if the issue is inside lean.nvim itself I'm working on adding more now in order to debug another issue so nothing really immediately more useful than print debugging at the moment.

[Julian Berman]

If you go back to a 4.13 rc the problem goes away?

[Julian Berman]

Marc Huisinga said:

This might be something that I've broken by accident fairly recently. Please report a bug.

lean4#5975

[mars0i]

@Christian Merten that sounds like a similar problem to what I had with the 4.13 release candidates. Since going back to 4.12, it's mostly gone away. I didn't realize that 4.13 had been officially released. I'll try it and see.

[mars0i]

@Julian Berman, @Marc Huisinga. Thanks. I didn't know about the completion plugins. I actually did have nvim-cmp and cmp-nvim-lsp installed, only because they were listed on the lean.nvim page when I started and I thought it (probably) couldn't hurt to install them. I assume I have to do something to configure nvim-cmp, since I haven't seen any completion options at all, but I'll figure that out.

[Christian Merten]

Julian Berman said:

If editing stops that would sound a bit like the LSP is crashing. You can use vim.lsp.set_log_level("DEBUG") to make Neovim a bit more verbose there (or "TRACE" to make it even more verbose) and then output will go to vim.lsp.log.get_filename(). In terms of internal lean.nvim logging if the issue is inside lean.nvim itself I'm working on adding more now in order to debug another issue so nothing really immediately more useful than print debugging at the moment.

Thanks, I can't reproduce this anymore after rm -rf .lake and a fresh cache, so maybe this was just a toolchain switching issue that I misinterpreted as a lean.nvim problem. Maybe an error message showing "LSP crashed" would be helpful?

[Julian Berman]

There's an open issue for showing that kind of message, I'll try to get to it.

[Patrick Massot]

@Julian Berman is it possible to hide the expected type panel in lean.nvim?

[Patrick Massot]

I want to show Lean during a talk and the expected type stuff is pretty distracting.

[Julian Berman]

@Patrick Massot I just added a show_term_goals option, does it do what you want? Set it with:

opts = {
  infoview = { show_term_goals = false }
}

[Patrick Massot]

Where would you write that?

[Patrick Massot]

How you mean in the neovim config?

[Patrick Massot]

It seems to work indeed.

[Julian Berman]

Next to where you have mappings = true

[Julian Berman]

Great!

[Patrick Massot]

It’s good enough for my talk, but it would be nice to have something more interactive.

[Patrick Massot]

In the infoview options dialog.

[Julian Berman]

Agree! Will add that when I get to a computer.

[Patrick Massot]

Thanks!

[Julian Berman]

OK Patrick I've now moved that to the view options section so you can interactively turn it on and off.

[Patrick Massot]

Great!

[Christian Merten]

When adding lean code snippets in LaTeX, I often miss the convenience of easily entering unicode symbols. Is there a way to use the great \<name> functionality of lean.nvim to add unicode characters in .tex files?

[Chris Henson]

Christian Merten said:

When adding lean code snippets in LaTeX, I often miss the convenience of easily entering unicode symbols. Is there a way to use the great \<name> functionality of lean.nvim to add unicode characters in .tex files?

This was added recently, adding require('lean.abbreviations').enable('*.tex', {}) to your config should work.

[Christian Merten]

Thanks! This works perfectly.

[Julian Berman]

Christian Merten said:

Maybe an error message showing "LSP crashed" would be helpful?

I've also just knocked this out. Thanks for the push.

[Julian Berman]

Here's a quick indentation question. Note that no matter the answer, I probably will make this configurable, so this is mostly about defaults. When you type:

structure foo where

and hit enter, do you expect the cursor to automatically indent? (Similarly for other declaration commands).

VSCode, for reference

does not autoindent this case AFAICT

[Patrick Massot]

Yes, I expect indentation.

[mars0i]

My opinion doesn't matter so much, because I've rarely used structures so far, but this is the general kind of case where I would expect automatic indentation. But maybe it depends on whether the language is indentation-sensitive with structure.

[Matthew Ballard]

Has this been covered already?

Error executing lua callback: ...m/site/pack/packer/start/lean.nvim/lua/lean/infoview.lua:977: index out of range
stack traceback:
        [C]: in function 'str_utfindex'
        ...m/site/pack/packer/start/lean.nvim/lua/lean/infoview.lua:977: in function 'update_position'
        ...m/site/pack/packer/start/lean.nvim/lua/lean/infoview.lua:1172: in function <...m/site/pack/packer/start/lean.nvim/lua/lean/infoview.lua:1166>

Upon undoing changes.

[Julian Berman]

Are you fully up to date? I fixed that a few days ago (at least I thought).

[Matthew Ballard]

Probably not.

[Julian Berman]

If you update let me know if you still see it, I think you shouldn't.

[mars0i]

I'm interested in plotting some functions, and ProofWidgets4 is supposed to be able to do that. The lean.vim README says "An infoview which can show persistent goal, term & tactic state, as well as interactive widget support (for most widgets renderable as text)."

That suggest that I can't use lean.nvim to see graphical effects with ProofWidgets4, and my experiments with nvim are consistent with that. I've avoided VSCode so far, but maybe now's the time (just for this purpose--I'm not giving up editing in nvim). Thought I should check my understanding, though. ProofWidgets4 is apparently generating HTML, SVG, and Javascript, so in theory I suppose that nvim could send the output to a browser.

[Shanghe Chen]

Yeah I think too that adapting the infoview to neovim and emacs is possible using an external browser (in emacs maybe it can be embedded using something like EAF), as said in vscode-lean4. I did this in some level for this in Intellij as here and think to adapt it to neovim or emacs in some future but currently have no enough time to make the progress. During my experience the apis defined in infoview-app have done almost all the work but some fonts, themes and right click stuffs have to be hanlded too though.

[Julian Berman]

(I'm in transit today and tomorrow, so will be slow to follow-up if need be) --

mars0i said:

though. ProofWidgets4 is apparently generating HTML, SVG, and Javascript, so in theory I suppose that nvim could send the output to a browser.

we do not yet do this, though yes we could, but the one browser I tried so far a few months back (awrit) isn't ready for use yet, it segfaults too easily on my machine at least. But yes at some point I do hope to have this ability.

Shanghe Chen said:

Yeah I think too that adapting the infoview to neovim and emacs is possible using an external browser (in emacs maybe it can be embedded using something like EAF), as said in vscode-lean4. I did this in some level for this in Intellij as here and think to adapt it to neovim or emacs in some future but currently have no enough time to make the progress. During my experience the apis defined in infoview-app have done almost all the work but some fonts, themes and right click stuffs have to be hanlded too though.

I'm not saying we shouldn't consider this at some point, but I think a lot of the "hard parts" of getting an infoview we had to pay already (to get the one lean.nvim supports), so I don't know if there's huge benefit coming from switching. And I think perhaps that if upstream is OK with it that it's always nice to have 2 implementations of something. Again, not saying we won't or shouldn't do it anyhow, or that if we were starting today perhaps we'd even start there. But I don't think this decision is so closely related to @mars0i's question which is more about how or if we can support rendering arbitrary JS when not running inside of a browser (and in particular when running in a terminal). As you say maybe using an external one is an option there, but that kind of solution is always lower priority to me personally given that I wrote lean.nvim in part because I don't really want to leave the terminal for programming :)

[Shanghe Chen]

Oh sorry that I misunderstood the discussion. Yeah I saw the hard work for implementing the current infoview in lean.nvim and definitely do not suggest for switching infoview. Indeed TUI is awesome:)

[mars0i]

Thanks @Julian Berman, @Shanghe Chen.

Thanks Julian for investigating awrit. That's a great idea down the road. In fact I didn't know that there was a real possibility of embedding a browser in nvim. Kind of amazing to me, but I had wondered whether that might be a possibility, because nvim continues to surprise me.

What I was imagining more concretely was sending only the Infoview HTML/SVG/JS/etc. to a separate browser. That might be a completely bad idea, or anyway not worth the trouble. But it's kind of half of what Shanghe was discussing. Regardless, I certainly wouldn't want the current Infoview functionality to leave nvim. This is one of the main things that makes using Lean so nice.

I don't generally use nvim in a terminal. I use the Goneovim GUI front end for nvim. Not sure whether that supports Kitty graphics. There are a couple of other nvim GUIs that I like; maybe one of them would. On the other hand, if I have to use a different setup for plotting from Lean, I'd choose nvim in a terminal app over VSCode.

But for now it will be fine to use VSCode. Not a bad idea for me to be familiar with it given its prominence in the Lean community.

(No need to read this: I came to nvim from MacVim's GUI, which does some things that I like a lot. When I started using nvim instead of vim for coding, I tried out all of the terminal apps that people on the nvim Zulip chat suggested. There was one basic function that's part of my workflow that wasn't possible because of a limitation in nvim--might have been fixed by now, but it wasn't a priority then. It was also clear that I would have had to do quite a bit of experimentation and configuration to make nvim in any of the terminal apps look and function the way I was used to.)

[mars0i]

Kind of off-topic, but people here might know: Does anyone have recommendations about their preferred VSCode vim emulation package?

[mars0i]

Ah, never mind. It looks like there are actually only a couple of options. I'll figure it out.

[Nick Ward]

First of all, let me say that lean.nvim is absolutely top of its class. I try (and often fail) to use every proof assistant in vim, and nothing else comes close to the experience.

I have encountered a mild inconvenience that I can't get to the bottom of. I have a keymap to call cursor(line('.'), 79) with the intention of approximating the keystrokes 79|. For some reason, this seems to be interrupted by lean.nvim. Calling it in a lean file jumps instead to a seemingly random point in the current line, though always somewhat close to column 79.

[Johan Commelin]

Is that maybe because of unicode?

[Julian Berman]

Thanks for the kind words!

Yeah that sounds probably like you're maybe not expecting the cursor position to count bytes? Specifically if you put some line with multibyte characters on it in any file, e.g.:

𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar𝔽oo𝒷ar

you can compare what you get from 79| and lua vim.fn.cursor(vim.fn.line('.'), 79), the latter will leave you around character 40 in that silly example.
If you want screen columns then you could just map 79| itself to your key? That's vim.keymap.set('n', '<leader>Z', function() vim.cmd.normal '79|' end) in case that's not something you've considered.

[Nick Ward]

That was it, thank you! Somehow I hadn't considered that :call cursor(line('.'), 79) was counting bytes while 79| was counting screen columns.

[Julian Berman]

lean.nvim v2024.12.1 :menorah: :holiday_tree:

Oh hello there. Another new release of lean.nvim is out!
By popular request, this one brings initial support for... autoindenting.

Autoindent

This hopefully should be self explanatory.
When you hit enter in places, or use other normal mode commands for creating lines like o, you should see the cursor automatically be indented in places which are stylistically expected.
Similarly, using the = operator should indent code (e.g. gg=G indents all lines in the buffer, which I've used to test that many but not all files in Mathlib will no-op when run through lean.nvim's autoindent support).
Note of course that given that Lean is whitespace sensitive that this = indentation is by nature "impossible" to do unambiguously for all cases, but it should do some right things some of the time.

I'm calling this alpha level, as there certainly are (even known) cases which can be improved and it's very possible that there are still some significant issues to work out, but it's at a state where I'd like more feedback and I've been using it a bit the past few weeks.
Please report any things you wish were indented, or things you wish weren't, as I've done a bit more than was originally requested here which can be both good or bad; in particular what good autoindentation feels like I find to often be slightly subjective and slightly hard to make precise -- so feedback as usual is welcome.

(n.b. you'll find that I've implemented at least one case of autodedenting, specifically when you type sorry you'll find yourself automatically dedented. There's more we could do there, e.g. we could make use of goal states to decide whether to dedent automatically, but I chose for now to get a first version out even though I've played a bit with fancier logic for dedenting, especially given that if you don't like any of this behavior I'd be happy to make it configurable to turn off.)

Turning it off

If for whatever reason you notice undesirable indent behavior, let me know, but you also can completely disable the behavior by creating the file ~/.config/nvim/indent/lean.lua and having it contain:

vim.b.did_ident = true

which tells Neovim that this (empty) file is the indent rules for Lean.

Other Changes

• A fix was contributed for users without satellite.nvim installed who weren't seeing progress bars show up
• blink.cmp support (an alternative completion plugin) was made more stable, avoiding a bug that might cause stack overflows.

Until next time Neovim friends.

---

You should be able to update using whatever plugin manager you're using, e.g. via :Lazy update.

[Francisco Giordano]

awesome! i'm curious if you can share what logic/heuristics you're using, at a high level

[Julian Berman]

The code is not gorgeous, but also not terribly complicated -- it's all here: https://github.com/Julian/lean.nvim/blob/main/lua/lean/indent.lua -- but basically the heuristics are:

• there's a list of words we indent after when appearing at the end of a line
• a list of words we never indent (to disambiguate cases like:

structure foo where
structure bar where

• we preserve indentation on the current line when already present to make sure not to screw up any existing indentation
• we dedent after sorries (in a way that's LSP aware, so when the LSP is up this works for admit)
• we indent after braces {, [ etc., including anonymous structure literals), even though style in Mathlib here seems undecided (on whether you align to the opening brace or just indent once, so I did just the latter for now)
• we specialcase the style that seems prevalent for long types, namely:

theorem foo :
    <four space type>
  := <two space term>

That's mostly it for now, as I say, we can evolve further if there's cases I missed or more intelligent logic we want -- all the current test cases live here: https://github.com/Julian/lean.nvim/tree/main/spec/fixtures/indent which are just lean files that are pre- and post- autoindent, so PRing additional examples there if you encounter a broken one is very welcome.

[Julian Berman]

(I played with reviving tree-sitter-lean to do this with tree sitter again where it's all nicer -- we'll see if I get back to that if things do start to get even more complicated)

[Patrick Massot]

This description worried me because it sounds like you forgot focusing dots, but you didn’t and this is really great!

[Julian Berman]

Yes I forgot that line, we check for focus dots as well!

[Julian Berman]

I'm a simple guy, this makes me happy:

Screenshot 2024-12-24 at 13.53.31.png

(It's mentioned above somewhere, that's all running in a terminal.)

[Adam Topaz]

What’s the browser?

[Julian Berman]

It's awrit! Which is a bit unstable but stable enough to use for this kind of thing.

[Julian Berman]

lean.nvim v2024.12.2 :confetti: :calendar:

Oh hello there. Another new release of lean.nvim is out, sneaking in just before 2025.
It contains some additional autoindent fixes and better widget behavior for try this widgets.

Clickable Suggestions

@Patrick Massot pointed out that in VSCode, when you see suggestions via e.g. the apply?, exact?, rw? tactics, that clicking in the infoview will perform the replacement.
Now this happens in nvim as well -- if you click on a suggestion, you should see the contents of your Lean source change.
Here's a quick demo if you haven't seen this feature before:

output.mp4

Note that "click" here has the same keybinding as other "clicking" operations in the infoview -- namely <CR> or K.

Telescope Picker for Abbreviations

I've also added a telescope picker for inserting abbreviations, which you can activate via :Telescope lean_abbreviations.
Here's how that looks:

telescope.mp4

This isn't a good replacement for \-based abbreviation entering -- not least of which because telescope has a bug that means that after inserting an abbreviation you end up in normal mode. But it's something we'd discussed previously as being cute if only to be able to dynamically see the list of abbreviations (and preview what they'll expand to), and can be improved upon slightly.

Other Changes

• Better dedenting autoindent behavior after some sorrys and => (though there's still one case I know is wrong)
• The order of diagnostics and suggestions in the infoview has been flipped to match VSCode, with widgets now showing up first before diagnostics in the infoview.

I'd still love to hear any feedback on how well (or not well) autoindent is working for anyone, but I hope that the silence there is either everything working well or better everyone enjoying their holidays.

Until next time Neovim friends.

---

You should be able to update using whatever plugin manager you're using, e.g. via :Lazy update.

[mars0i]

Haven't updated for the new release yet, but the autoindent on the previous release seems excellent. I don't notice it--for what I write, it just felt like it was doing the right thing. It was not having autoindent, before that, that I'd notice when I'd hit newline.

[Patrick Massot]

I just realized that I now need to retrain my muscle memory because autoindent is working for me so I don’t have to indent manually after hitting enter, especially after :=!

[Julian Berman]

Well that's good! I have to say I noticed the same :), I instinctively hit <CR> and now I have to actively backspace until my muscles stop doing that.

[Patrick Massot]

Thinking about what would be the next great step for lean.nvim, I went back to the poll and I’m disappointed to see I am the only one who voted for the last great missing piece of functionality which is Shift-click selection in the InfoView. I feel it may be either because many people misunderstood the suggestion or simply don’t use it in VSCode because they don’t know about it. I’m talking about the mechanism that powers the unfold? tactic or the calc widget for instance.

[Patrick Massot]

People who didn’t vote for Shift-click, I advise you to try in VSCode

import Mathlib.Tactic

def cont (f : ℝ → ℝ) := Continuous f

noncomputable def s := Real.sin

example : cont s := by
  -- apply? -- fails
  unfold? -- shift-click on `cont` and accept the suggestion
  unfold? -- shift-click on `s` and accept the first suggestion
  apply? -- will work after the above shift-click

[Julian Berman]

(I suspected the same, that it wasn't highly voted because people don't know about it -- so thanks for sharing the example! I'll have to play with it myself!)

[Patrick Massot]

You can see this Shift-click in action in conv? and calc at https://youtu.be/8MFGhOWeCNE?t=1742.

[Patrick Massot]

Those things are easy to miss when learning Lean because they leave no trace in the finished Lean file.

[Patrick Massot]

(and they are probably not mentioned in MIL :embarrassed:)

[Patrick Massot]

I just noticed something missing compared to the VSCode plugin. When doing monadic programming, putting the cursor on a return in VSCode highlights the corresponding do. This is sometimes very useful to make sure we are exiting only a nested do block. Stupid example:

example : Nat := Id.run do
  let _ ← Id.run do return 1
  return 2

putting the cursor on return on line 2 should highlight the do on line 2.

[Julian Berman]

Great Patrick, keep suggesting things which are one line changes I can do even before having morning coffee. Done.

Screenshot 2024-12-31 at 08.58.23.png

Note that you need (and want) to be using https://github.com/andymass/vim-matchup for this (better % behavior which lean.nvim already has for jumping between namespaces and sections, if/then/else, and soon a few other things.)

[Patrick Massot]

Great!

[Patrick Massot]

Don’t forget to document it.

[Patrick Massot]

However vim-matchup doesn’t seem to work with nested if/then/else.

[Patrick Massot]

It’s more subtle: it seems to be confused when there is no else. For instance put the cursor on else in

example : Nat := Id.run do
  if true then
    if false then
      return 0
    return 1
  else
    return 2

[Patrick Massot]

And also in this example only the first return highlights the do.

[Patrick Massot]

I’m afraid you’re doing something regexp-based instead of asking Lean for the relevant do.

[Patrick Massot]

Well, I guess VScode asks Lean. Probably @Sebastian Ullrich or @Marc Huisinga can confirm.

[Patrick Massot]

Note VScode does not do the highlighting thing with if/then/else although it would be nice (but much less useful than with do).

[Julian Berman]

Oh I can't say I even know do supported multple return statements, that definitely means matchup isn't the right thing for it then. Yes we are certainly doing regex things, this is all the pain of not having a tree-sitter parser -- there's nothing for this in the LSP itself I think? But maybe Lean's LSP has some extension, if Marc doesn't confirm I'll look at the VSCode extension code later.

[Patrick Massot]

Yes, do/return is really flexible. This is precisely why this highlighting is useful.

[Julian Berman]

(OK, I'll revert the simple change until I look later at whatever can be done.)

[Henrik Böving]

Julian Berman said:

Oh I can't say I even know do supported multple return statements, that definitely means matchup isn't the right thing for it then. Yes we are certainly doing regex things, this is all the pain of not having a tree-sitter parser -- there's nothing for this in the LSP itself I think? But maybe Lean's LSP has some extension, if Marc doesn't confirm I'll look at the VSCode extension code later.

Marc is probably not going to respond until next week

[Julian Berman]

Yeah no rush certainly.

[Patrick Massot]

Oh yes, please don’t interpret my messages as “people should be working on December 31st”.

[Henrik Böving]

Just wanted to say that so you don't end up waiting on an answer ^^

[Patrick Massot]

I simply have a weird job where what I’m doing today clearly qualifies as vacations.

[Marc Huisinga]

The return highlighting uses LSP's document highlight request.

[Julian Berman]

Thanks Marc! I had not noticed it only shows up in VSCode when you click on return (and not immediately) -- are there other places that the LS highlights yet via document highlight?

I personally have document highlight turned on on cursor hold already which I forgot to mention. I'll add a doc note for folks to show how to enable it yourselves as well for this use case then. If you can't wait, it's essentially add:

    if client.supports_method('textDocument/documentHighlight') then
      vim.api.nvim_create_autocmd('CursorHold', {
        callback = vim.lsp.buf.document_highlight,
        buffer = 0,
        desc = 'Show document highlight on cursor hold.',
      })
      vim.api.nvim_create_autocmd('CursorMoved', {
        callback = vim.lsp.buf.clear_references,
        buffer = 0,
        desc = 'Clear highlights when the cursor moves.',
      })
    end

to your LSP attach handler.

[Julian Berman]

In unrelated (or related news), lean.nvim passed 300 GitHub stars a few days ago. Thanks to all for all the support!

[Marc Huisinga]

Julian Berman said:

are there other places that the LS highlights yet via document highlight?

It also highlights references: https://github.com/leanprover/lean4/blob/2421f7f79941853da14346a234aec6df70cf36a1/src/Lean/Server/FileWorker/RequestHandling.lean#L324

[Calvin Lee]

This might be a better question for a "lean.nvim dev" stream, since it's about the internals of the plugin (but I know most people who know about the nvim plugin are here):

I'm trying to improve the agda neovim plugin cornelis when multiple buffers are open. Does lean just use a single buffer (the one called curr) for all lean info, and then replaces it based on what buffer your cursor is currently in? Does it cache the text in curr so that it can re-display it when you go back to the right file?

Cornelis opens a new info buffer per agda buffer, which makes it hard to switch between files

[Julian Berman]

I'm trying to improve the agda neovim plugin cornelis when multiple buffers are open. Does lean just use a single buffer (the one called curr) for all lean info, and then replaces it based on what buffer your cursor is currently in? Does it cache the text in curr so that it can re-display it when you go back to the right file?

Yes, same buffer -- it attaches an autocmd which updates the infoview on cursor move and switches which buffer has the right to update the infoview when you enter a new buffer. We actually started support on having multiple infoviews updating separately (say for 2 separate lean windows having 2 separate infoviews), I should get back to that at some point, the work was very minimal (though as you say it should be optional which layout you like).

[Julian Berman]

Does it cache the text in curr so that it can re-display it when you go back to the right file?

No we don't do any caching we just re-request, but we could of course.

[Calvin Lee]

thanks a lot for the code pointers!
Cornelis is written in Haskell (which is a choice...) and Agda is not something that really supports an "ongoing conversation" like lean does through LSP. So I have to adapt this a bit but I think it will help a lot :)

[Mauricio Collares]

The impression I had when following plfa was that it was at least as interactive as Lean, other than lack of tactic support. There are a lot of interactive operations you can do on holes. But maybe you're talking about tactics specifically.

[Julian Berman]

I'll say I've definitely thought of attempting some proof.nvim generalized version of lean.nvim before, which I don't think would be impossible to do, but unfortunately I like Lean too much to want to play with anything else!

[Calvin Lee]

Mauricio Collares said:

The impression I had when following plfa was that it was at least as interactive as Lean, other than lack of tactic support. There are a lot of interactive operations you can do on holes. But maybe you're talking about tactics specifically.

There are some major differences. Agda's interactivity is done in quite a different way, and the current iteration is pretty hard to squeeze into the LSP model that lean uses.

Specifically in agda "loading" a file (getting syntax and typechecking) is a distinct step and must be re-performed after changing the file. There also really isn't any kind of "hover" or inspection for proof terms that are not in a hole. Each hole has its own context that you can interact with, so that part is kind of similar to lean

[Mauricio Collares]

I see, thanks!

[Patrick Massot]

Another low-hanging (I guess?) target that I already mentioned: it would be nice if the infoview could be excluded from the list of buffer when telescope show buffers.

[Julian Berman]

I literally never use the buffer picker, it will depend on whether it actually supports identifying buffers to not consider, but I can put it on the list to look at.

[Julian Berman]

OK it does seem to have one, specifically:

require('telescope.builtin').buffers{ file_ignore_patterns = { "lean://" } }

will ignore infoview windows (if you make that your mapping instead of running require('telescope.builtin').buffers{} or :Telescope buffers directly). Does that help / seem good enough of a solution?

[Patrick Massot]

It seems good enough but I need more help to implement this advice. I only manage to brick my vim when I try to follow it.

[Patrick Massot]

Specifically I tried to modify https://github.com/PatrickMassot/neovim_config/blob/master/lua/telescope-setup.lua#L74 by adding that { file_ignore_patterns = { "lean://" } } and it breaks everything.

[Patrick Massot]

I’m sure I’m missing something obvious but I really don’t understand lua.

[Julian Berman]

The thing you're missing is that foo is a function and foo() is a function call, and in Lua (wonderful as it is) foo{} is also a function call (it's calling foo with a single argument, a Lua table). So if you just added that {...} business what you have instead of binding a key to call a function you invoked telescope during your nvim startup.

Instead you want to change to:

 vim.keymap.set('n', '<leader>fb', function() return require('telescope.builtin').buffers{ file_ignore_patterns = { "lean://" } } end, { desc = '[F]ind [B]uffer' })

[Patrick Massot]

Makes sense, thanks.

[Patrick Massot]

So I vote for putting that into lean.nvim documentation.

[Julian Berman]

Perfect, will add it along with the other thing above that I haven't written out yet either.

[Julian Berman]

OK the two doc changes (on document highlighting and infoview filtering) are here and here. Further suggestions (or direct edits) are of course always welcome.

[David Thrane Christiansen]

Julian Berman said:

are there other places that the LS highlights yet via document highlight?

In Verso, I use it to highlight various matching or indentation-sensitive parts of syntax, like all of the bullets of a list when one of them is clicked. VSCode has a bug where it doesn't send the request if it doesn't think the cursor is on something sufficiently identifier-like, but it's a great experience in Emacs :)

[MrQubo]

Has anyone managed to make this plugin work on NixOS with lake projects?

[Johan Commelin]

Yes, but I don't manage my vim plugins via nix

[MrQubo]

Yeah, having plugins managed by nix was kinda my problem. Neovim was using different version of lake then in my project.

[Francisco Giordano]

Julian Berman said:

require('telescope.builtin').buffers{ file_ignore_patterns = { "lean://" } }

This could be addressed more generally and in the plugin itself by setting 'nobuflisted' for infoview buffers

[Julian Berman]

I thought we already did that when creating the window! But it seems you're right that we don't. I can look again later (or PR of course welcome)

[Julian Berman]

Francisco Giordano said:

This could be addressed more generally and in the plugin itself by setting 'nobuflisted' for infoview buffers

This is fixed in this way now, thanks for noticing!

[Tomaz Mascarenhas]

Hi, I am working on a project that depends heavily on mathlib. I compiled it in around 10 minutes with lake build. I expected that lean.nvim would be able to (since it's already compiled) have everything working instantly. Instead, everytime I open a new file it takes around 2 minutes and gives me some messages as it is compiling it again, and then starts working properly. This is not the case for emacs and visual studio code, which are able to setup everything instantly after building. Maybe I setup something wrongly? Or is it the expected behavior?

[Julian Berman]

That sounds definitely not expected -- can you let me know what you see from :checkhealth lean with the project open, and also from :LspInfo?

[Tomaz Mascarenhas]

sure, this is checkhealth's output:

==============================================================================
lean: require("lean.health").check()

lean.nvim (c470003) ~
- OK Neovim is new enough.
-   `vim.version()`:  0.10.3+g9b5ee7df4e
- OK Lake is runnable.
-   `lake --version`:  Lake version 5.0.0-1165156 (Lean version 4.15.0)

this is LspInfo:

lspconfig: require("lspconfig.health").check()

LSP configs active in this session (globally) ~
- Configured servers: ocamllsp, hls, rust_analyzer, pyright, clangd, gopls, leanls
- OK Deprecated servers: (none)

LSP configs active in this buffer (bufnr: 1) ~
- Language client log: ~/.local/state/nvim/lsp.log
- Detected filetype: `lean`
- 1 client(s) attached to this buffer
- Client: `leanls` (id: 1, bufnr: [1])
  root directory:    ~/Projects/lean-smt/tom/
  filetypes:         lean
  cmd:               ~/.elan/bin/lake serve -- /home/tomazgomes/Projects/lean-smt/tom
  version:           `Lake version 5.0.0-1165156 (Lean version 4.15.0)`
  executable:        true
  autostart:         true

Docs for active configs: ~
- leanls docs: >markdown

  https://github.com/leanprover/lean4

  Lean installation instructions can be found
  [here](https://leanprover-community.github.io/get_started.html#regular-install).

  The Lean language server is included in any Lean installation and
  does not require any additional packages.

  Note: that if you're using [lean.nvim](https://github.com/Julian/lean.nvim),
  that plugin fully handles the setup of the Lean language server,
  and you shouldn't set up `leanls` both with it and `lspconfig`.

  ```

[Tomaz Mascarenhas]

One thing: actually I am not building the entire project, rather I am building a specific file with lake (lake build path.to.file) which imports many other files. Then I am trying to open one of the files that is imported inside the file I am building

[Julian Berman]

Hmm. OK -- is the repo public so that I can try to reproduce?

If not, or even if so -- I am slightly suspicious of the root directory maybe -- it says ~/Projects/lean-smt/tom/ that means lean.nvim thinks your lean project lives there -- does it? That directory has the lakefile.toml and toolchain etc.? Or is it really ~/Projects/lean-smt/

[Tomaz Mascarenhas]

no, the root of the project is ~/Projects/lean-smt/tom indeed

[Julian Berman]

OK, so there goes that guess.

[Tomaz Mascarenhas]

this is the branch of the project: https://github.com/tomaz1502/lean-smt/tree/feat/transfns

[Tomaz Mascarenhas]

what I tried to do was to run lake build Smt.Reconstruct.Arith.TransFns and then open Smt/Reconstruct/Arith/TransFns/ArithTransPi.lean

[Julian Berman]

(Building)

[Julian Berman]

Ah, the build output makes me worry you're seeing the docPrime linter issue :/

[Julian Berman]

Which, in short -- is that because the docPrime linter emitted thousands of diagnostic messages that would make lean.nvim slow to a crawl -- I am pretty sure more recent Mathlibs have silenced the linter, but it's possible this 4.15 commit still has it on

[Julian Berman]

Of course it's a lean.nvim performance issue to fix -- it has to do with us not having proper backoff for re-rendering the infoview when there are so many diagnostics coming in

[Julian Berman]

I assume it's not trivial for you to upgrade Mathlib here? If not maybe you can just try to turn that linter off, I forget if downstream projects can do that or not

[Julian Berman]

It's still building here but yeah I suspect that's the issue

[Tomaz Mascarenhas]

Ah I see.. Indeed, the messages I see after opening the file have to do with this linter option

[Tomaz Mascarenhas]

I think it's fine to upgrade lean and mathlib - 4.16 should be enough?

[Julian Berman]

Probably yes, I think it was turned off a few months ago so 4.16 I think is already good

[Tomaz Mascarenhas]

Great, thanks a lot Julian!

[Julian Berman]

I really should figure out how to fix it but I haven't been able to figure out how to do so yet in a way that isn't quite fiddly.

[Julian Berman]

No problem.

[Julian Berman]

Hi hi. A few times folks have asked me if I know what the number of current Lean users are that use lean.nvim, and I've estimated based on folks I see here self-identifying, and/or folks on the issue tracker. But I'm honestly perhaps curious to check my estimate by just asking!

This is clearly completely optional, and lean.nvim does not ship any code to collect analytics (and will never do so). But if you're comfortable sharing that you use it just so I have a rough count, can you vote on the poll below? I assume the numbers will not immediately be correct, as not everyone follows the Zulip closely, but let's see what happens.

[Julian Berman]

/poll I currently use Neovim / lean.nvim to work with Lean:
⊤ (all or nearly all the time)
≃ (sometimes, and sometimes VSCode)
:thinking: (not yet, but I'm planning on it)
⊥ (not at all, and I'm not sure why I'm responding to this poll)

[Chris Henson]

I think the only time I have ever really used VSCode (at least post Lean 3) is when I wanted to try out the ProofWidgets library.

[Robin Carlier]

If VS code was the only editor option I wouldn't be doing lean at all I think.

[Chris Henson]

Is there a way to supress the ... is not a supported Lean widget type messages caused by ProofWidgets? It is a bit of an annoyance when using calc.

[Chris Henson]

(it would also be cool to support them, but I don't have enough understanding of the plugin or widgets to help)

[Patrick Massot]

I agree it would be nice to have a config variable telling vim to never display this message. But the good news is that the calc widget and its friends seems to be very close to become supported in lean.nvim!

[Julian Berman]

Chris Henson said:

Is there a way to supress the ... is not a supported Lean widget type messages caused by ProofWidgets? It is a bit of an annoyance when using calc.

Where do you see these / how up to date are you? They shouldn't be visible unless you specifically enable extra logging

[Chris Henson]

It happens the first time my cursor is over calc when opening a file. I'm likely using an old version accidentally, between using nix and tinkering with the plugin a bit.

[Julian Berman]

They should have entirely gone away after https://github.com/Julian/lean.nvim/commit/bf9bb854faf82d30f36b3211450223b063cfab9e , I'd check if you're newer than that

[Robin Carlier]

Is there a command to tell lean.nvim to "freeze" lsp data for a while, and then resume? On a not that powerful laptop, editing files with heavy proofs causes a noticeable delay at every keystroke due to re-elaborating the whole file all the time (not to mention constant high CPU usage). I sometime slap a #exit after or before whatever i’m doing until I’m done editing to speed things up, but it’d be nice to have a "pause untill I say I’m done" function that could be assigned to a binding.

[Julian Berman]

Right there's #exit which is just Lean functionality -- if you just want to pause edits in the plugin you might want :LeanInfoviewPinTogglePause (boy is that a mouthful :/) which we bind to <LocalLeader>p by default, it pauses updating the infoview -- I will say that though I think we have a few tests for that functionality that I have used it precisely 0 times, so if you find an issue with it (or if you don't!) do let me know. Maybe that's what you want?

[Robin Carlier]

It looks like LeanInfoviewPinTogglePause does not prevent the plugin from restarting elaboration at every keystroke and re-sending the file to the server. I’m testing it right now and it seems to work as intended (I mean the "freezing infoview" part) at least.

[Julian Berman]

Just to be sure, that's what you want, or what you don't want?

[Julian Berman]

(If you don't want the server doing any work, you can also stop and then re-start the LSP.)

[Robin Carlier]

Sorry, I wasn’t clear. I don’t want the server to do any work for a while.

[Robin Carlier]

I guess I’ll just bind something to a LSP kill-switch then. It’s just that it could be nice to have something that pauses it without having to completely restart it.

[Julian Berman]

No you're fine, apologies I'm also splitting my attention between 3 places while trying to understand the question -- I guess what I mean to ask is what things do you want to still actually continue updating while paused?

[Julian Berman]

E.g. lean.nvim doesn't control the Lean server sending diagnostics, so long as Lean is "alive" it will send those, and thereby be elaborating what you're doing -- stopping that really means stopping the LSP sending stuff back and forth, which is easiest to do by stopping the server. But I guess I partially understand the question now, you want that, and to not pay whatever startup cost of starting the process and importing stuff or whatever

[Robin Carlier]

Yep, exactly! Basically not sending any data for a while (I understand this means temporarily giving up completions, diagnostics, infoview etc), while keeping the connection alive but nothing more, and then when resuming sending the new file state and cursor position to receive new diagnostics.

[Kevin Buzzard]

Just to add that "every time I press a key everything in the proof recompiles" is not a problem specific to nvim :-)

[Julian Berman]

@Robin Carlier I can't think of an immediate way to do this but I also am not convinced there isn't one... so it's a good question

[Julian Berman]

(Feel free to open an issue if you'd like, I have 2 features that need to get out the door any day now and I can't think about anything else until I get them fully done, but I'm happy to look into this sometime after, it'll be something not specific to Lean at all presumably)

[Robin Carlier]

Will do ! I will think about it as well, but I’m not to familiar with the internals of lsp integrations in nvim (I agree that this is general and could apply to any lsp servers, it’s just that not all languages recompile the files all the time) so I can’t guarantee that I’ll be able to think about something meaningful

[Julian Berman]

30 seconds of googling didn't find an existing nvim plugin that does this, though I did find 2 people asking for it -- the relevant object is vim.lsp.Client -- and I think one crazy-enough-but-might-work kind of strategy is to monkey patch out one or more of the request methods from the active client, so it stops sending updates to the server, but how feasible that really is is down to details (e.g. Lean's server expects to be "kept alive" for RPC sessions, but that's not an issue because indeed it will kill the RPC session but lean.nvim will restart that when you unpause -- but there might be some other protocol-level LSP stuff that will be less happy by being silenced which I'm not thinking of)