How can i help the project?

[RamonJales]

Hello, i am interesting in contributing to the project. How can i do this, where can i start and what I need know?

[Julian]

Hey there. Thanks for offering! It might be easier to guide an answer if I knew a bit about your background. Are you already familiar with any or all of Lua, neovim plugin development, Lean, and/or this project's codebase? I assume you've hopefully at least used this plugin already with Lean? The above may help with figuring out what to suggest, there's of course a ton of things that need doing so more help is always welcome.

[RamonJales]

Ok... I guess I was hasty, I thought the idea was so cool that I was premature. I confess that I didn't even install the plugin. My only experience was with Lean 4, where I used it in an undergraduate course. I dont know if this work, but I have experience with Haskell and Coq too. So, I guess my first task is to install the plugin and learn the basics of Lua, right? About neovim plugin development, I dont even know where to start, can you advise me what to look for? If there is any issue more mechanical or issue that you think I can do just searching, assign me.

[Julian]

No worries at all, you're still welcome even if you're new, and thanks for the kind words -- though yeah I suspect using the plugin is the right first step!

If you want advice, my suggestion would be:

• try using this to do a bit of lean. Perhaps try using it to make a tiny contribution to batteries or to Mathlib depending on your interests

• once you've used it for a few hours then hopefully what works well and what doesn't in the plugin will be a bit clearer

• and then if you want a concrete thing you could definitely try helping with, three immediate ideas you could check out are:

• 329 -- this is going to turn out to either be something very simple we should be tweaking, or else it will turn out to not be possible right now due to needing some extra Lua API from neovim core itself (in which case we put it on hold)

• 30 -- this also shouldn't be too difficult, it probably just will involve adding a component to lean.infoview.components which checks whether the LSP client is connected or not

• 317 -- this is more new functionality -- we have a :Telescope loogle which @hargoniX helpfully contributed and which I made a bit worse by poking at it unfortunately, but if you're looking for a larger thing to poke at you could have a look at some of the areas of improvement there and maybe try playing with it again.

(I'm going to close this just to keep the issue list clean, but you're again quite welcome, and if you're not on the Zulip already that's also a good place to ask questions if you get stuck!)

[RamonJales]

Ok! Thanks again. I will try these things. Is there any way I can communicate with you in the future(email or something else)?

[Julian]

I'm on the Zulip myself, you can ping me there!