Zulip Chat Archive

yeah, I did notice this when reading the general Linux instructions https://leanprover-community.github.io/install/linux.html. I'll submit a PR in a bit fixing this

Eric Rodriguez (Feb 08 2022 at 15:36):

I'm not a ~~Lean~~ vim! user but I've heard good things about it recently, @Julian Berman is in charge of it

Patrick Massot (Feb 08 2022 at 15:40):

I think part of the issue is they are most focused on Lean 4.

Patrick Massot (Feb 08 2022 at 15:40):

Last time I tried it was crashing so often that I gave up

Alex J. Best (Feb 08 2022 at 15:41):

I've found it quite reliable recently, different to vscode for sure but probably worth trying again and reporting any crashes

Anne Baanen (Feb 08 2022 at 15:46):

I have had little complaints with lean.nvim since October, apart from some irregular crashing and slightly wonky UTF-16 handling (which might have been fixed by now, I should really update...)

Julian Berman (Feb 08 2022 at 15:47):

Patrick Massot said:

Last time I tried it was crashing so often that I gave up

Patrick is this still the case? If so please say so when that happens

Julian Berman (Feb 08 2022 at 15:48):

I wouldn't say we (if there's a we) are more focused on Lean 4 -- I want both to work equally well until Lean 4 is what everyone uses. Lean 4 has new LSP functionality so there's some cool things that only work on Lean 4, but I personally use it with Lean 3

Julian Berman (Feb 08 2022 at 15:48):

Anne Baanen said:

I have had little complaints with lean.nvim since October, apart from some irregular crashing and slightly wonky UTF-16 handling (which might have been fixed by now, I should really update...)

Yes this is fixed (it was partially a neovim bug actually, not a lean.nvim one, so update both)

Patrick Massot (Feb 08 2022 at 15:49):

I'll try to find time to try again.

Julian Berman (Feb 08 2022 at 15:49):

But yes please no one keep complaints to yourself :)? We are likely more than happy to fix them but we can't fix what we don't know.

Patrick Massot (Feb 08 2022 at 15:50):

Last time it was so unstable that I thought everybody would see it.

Julian Berman (Feb 08 2022 at 15:51):

The only crash related thing I'm aware of is this issue: https://github.com/Julian/lean.nvim/issues/203 which I believed was macOS only -- if that's what you're running into the crashes would indeed be suuuuuuper annoying. So if it's that (if you see lots of segfaults) let me know, though I'm not sure what to do, it just requires some time digging through the source code.

Rish Vaishnav (Feb 08 2022 at 17:46):

I've been using it exclusively with Lean 3 for quite a while now (will get back into development as soon as I've PR'ed some of my work on random variables). Haven't run into any major issues yet, but I do get SigAbrtonce or twice daily (on Linux) and do :LspRestart when that happens -- but it's something I'm willing to accept so that can use vim...

Julian Berman (Feb 08 2022 at 17:52):

Interesting, I didn't know you saw the sigabrts too -- we could shove in a hack to just auto-restart until we figure out what's causing them

Julian Berman (Feb 08 2022 at 17:52):

(By the way I should have said earlier that @Rish Vaishnav is the one responsible for figuring out the pesky utf-16 issue, which would have been hell to debug!)

David Sprayberry (Sep 04 2023 at 17:50):

I have a question about installing lean.nvim. Since a package manager doesn't seem to have much use anymore I don't use one. I made a package ~/.config/nvim/pack/lean and cloned the 6 dependencies and lean.vim to ~/.config/nvim/pack/lean/start but was wondering about the ~/.config/nvim/plugin/lean.lua configuration file. I made it anyways but was wondering if it is something a package manager is supposed to use or if the lean.nvim plugin itself uses it without the help of a plugin manager.

Julian Berman (Sep 04 2023 at 18:25):

(You mean lean.nvim right not lean.vim)

I'd say yeah a package manager is still extremely common to use, probably 95% plus of users I'd guess use it.

Julian Berman (Sep 04 2023 at 18:25):

There's instructions for using lazy.nvim or vim-plug in the README

David Sprayberry (Sep 04 2023 at 18:41):

Julian Berman said:

(You mean lean.nvim right not lean.vim)

I'd say yeah a package manager is still extremely common to use, probably 95% plus of users I'd guess use it.

Yes sorry typo. Yea historically it had use and that's why they're so common. Vim and nvim don't really need them anymore though.

Julian Berman (Sep 04 2023 at 18:42):

Most people still think they do, there's lots of additional functionality they provide, but yes, vim and nvim now have at least pathogen-style package managers in them.

Julian Berman (Sep 04 2023 at 18:46):

(Having instructions for using vanilla nvim packaging would certainly be a welcome addition to the README if you're interested!)

Julian Berman (Sep 04 2023 at 18:47):

Oh, I'm just now seeing your edit to your original message -- that sounds like your nvim is too old, what version are you on?

David Sprayberry (Sep 04 2023 at 21:09):

Julian Berman said:

(Having instructions for using vanilla nvim packaging would certainly be a welcome addition to the README if you're interested!)

It can just be install lean4 and make sure you have export PATH="/home/david/lean4/build/release/stage1/bin:$PATH" in your .bashrc and clone your plugins into ~/.config/nvim/pack/*/start and the github has the rest covered.

David Sprayberry (Sep 04 2023 at 21:09):

Julian Berman said:

Oh, I'm just now seeing your edit to your original message -- that sounds like your nvim is too old, what version are you on?

I'm using v0.7.2, the newest version for my package manager (apt on Debian). I uninstalled that and built it from source, now I have v0.10.0 but it still had an error turned out I did not have lean in my path.

David Sprayberry (Sep 24 2023 at 21:57):

I'm reading Type Driven Development and saw that in the text editor it uses there's a way where you just write the name and type for a definition and with a shortcut the editor will insert a skeleton definition for it, using the equivalent of sorry for the parts that still have to be implemented. There's no equivalent for Lean, right?

Julian Berman (Sep 24 2023 at 23:08):

I think that general question is being tackled "generically" (as in not specifically to nvim) now thankfully.

I think the answer is "partially yes" for some kinds of declarations. E.g. if you write something like:

instance : Add ℕ := _

and put your cursor on the _ (in either normal or insert mode) and then ask for a code action, you'll see:

Screenshot-2023-09-24-at-19.07.51.png

Julian Berman (Sep 24 2023 at 23:09):

If your question has to do with setting code actions up entirely, there's an example here for how I do it which I suppose probably belongs in a note in the Wiki if it's not already there, I forget: https://github.com/Julian/dotfiles/blob/4a711e30c4efdb3df5e79f9a868037cffc7d34e0/.config/nvim/lua/plugins/lsp.lua#L71-L74

Adam Topaz (Sep 24 2023 at 23:30):

I think the book David is reading is based on idris, right? Anyway I think the closest we came to this was extract_goal in lean3. I’m not sure about the status with lean4.

Alex J. Best (Sep 25 2023 at 00:44):

There is Mathlib.Tactic.ExtractGoal I dont think it yet produces a code action though (partly as its a bit unclear how to get the location where it should be inserted

David Sprayberry (Sep 25 2023 at 14:34):

Julian Berman said:

I think that general question is being tackled "generically" (as in not specifically to nvim) now thankfully.

I think the answer is "partially yes" for some kinds of declarations. E.g. if you write something like:
instance : Add ℕ := _
and put your cursor on the _ (in either normal or insert mode) and then ask for a code action, you'll see:

Screenshot-2023-09-24-at-19.07.51.png

Oh that's great to hear! I'm relatively new to plugin configurations, so now I'm learning lua and nvim+lua. I had some trouble getting your plugin to work 3 weeks ago but didn't install the additional plugins until recently. I haven't been able to get nvim-lightbulb and lsp-status to work yet.

David Sprayberry (Sep 25 2023 at 14:36):

Julian Berman said:

If your question has to do with setting code actions up entirely, there's an example here for how I do it which I suppose probably belongs in a note in the Wiki if it's not already there, I forget: https://github.com/Julian/dotfiles/blob/4a711e30c4efdb3df5e79f9a868037cffc7d34e0/.config/nvim/lua/plugins/lsp.lua#L71-L74

Thanks, this is helpful. I should be able to get it working once I learn lua and plugin configurations.

David Sprayberry (Sep 25 2023 at 14:37):

Adam Topaz said:

I think the book David is reading is based on idris, right? Anyway I think the closest we came to this was extract_goal in lean3. I’m not sure about the status with lean4.

Yes, it's based on Idris 1.

David Sprayberry (Sep 28 2023 at 18:16):

Hi, I'm still confused on setting up your plugin. I don't use completion but was hoping to be able to get lightbulb and lsp-status working. The plugin I have besides those are lsp-config, plenary, switch, and tcomment. I've been putting .lua config files in runtimepath/lua/. I was wondering how init.lua and the config files should look?

Julian Berman (Sep 30 2023 at 02:09):

That's more about setting up neovim than it is setting up lean.nvim specifically. My recommendation is still to use a plugin manager :), for which you can then simply follow the instructions in the README. If you insist on doing things without one I probably am still happy to help (tomorrow) but please then pastebin what you have somewhere so I can see what you've done so far.

David Sprayberry (Oct 02 2023 at 17:39):

Julian Berman said:

That's more about setting up neovim than it is setting up lean.nvim specifically. My recommendation is still to use a plugin manager :), for which you can then simply follow the instructions in the README. If you insist on doing things without one I probably am still happy to help (tomorrow) but please then pastebin what you have somewhere so I can see what you've done so far.

Sorry configuration questions are probably inappropriate; that's probably why nobody responded to my initial configuration questions on the neovim chat. I learned some lua basics and reading the nvim documentation I thought it would be good learning to write my own little plugin for lean. I got the basics working and I used your syntax and abbreviations files

Edoardo (Oct 03 2023 at 09:15):

Hello! Is there an interaction function that allows the user to automatically split on match cases, like done for examples in Agda?

Alex J. Best (Oct 03 2023 at 10:01):

Can you give an example of a proof state and what you'd like the tactic to do more precisely (for those of us that dont know agda)

Edoardo (Oct 03 2023 at 10:41):

Sure! It's not really a tactic, it's just a convenient help from the LSP/editor support. For example, in Agda one might define a simple function such as

add : ℕ -> ℕ -> ℕ
add x y = {! !}

where {! !} is something similar to goals in Lean. In my editor, for example, if I get the cursor into the goal and press the correct combination of keys, I get a prompt that asks me "on what I want to split": say I want to split on x, it automatically changes the definition of add to

add : ℕ -> ℕ -> ℕ
add zero y = {! !}
add (suc x) y = {! !}

Of course, I'm not asking what combination do I have to press to do stuff I do in a completely different framework, just if Lean (or lean.nvim) supports something similar

Edoardo (Oct 03 2023 at 10:42):

If, for example, I have a similar situation:

def add (x y : Nat) : Nat :=
 match x with
 | n => _

is there a way to automatically "split" n?

Henrik Böving (Oct 03 2023 at 11:05):

You can do stuff like this with the LSP code actions that are provided by std4. But it is not built in right now. In general I would not expect these features to be provided by the editor in a Lean context but instead by user libraries that define code actions. You can of course bind the execution of specific code actions to some keys I guess.

David Sprayberry (Oct 03 2023 at 14:33):

Henrik Böving said:

You can do stuff like this with the LSP code actions that are provided by std4. But it is not built in right now. In general I would not expect these features to be provided by the editor in a Lean context but instead by user libraries that define code actions. You can of course bind the execution of specific code actions to some keys I guess.

Do you know of any such libraries that have been written?

Jireh Loreaux (Oct 03 2023 at 15:44):

I would expect Std to (eventually) contain a code action for auto-expanding match statements. We already have this for cases and induction. See here: docs#Std.CodeAction.casesExpand. Probably a code action for match would be similar.

Last updated: Dec 20 2023 at 11:08 UTC