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