help installing lean for neovim - novice user

Stream: new members

[Michael Novak]

Hi, I'm a new user, I want to learn Lean. I'm not really experienced in VS Code or NeoVim, but I'm pretty comfortable in Vim, which I used without too much advanced configuration. But I'm mainly a math student,I barely ever program. I also use Parabola GNU/Linux, and I prefer to use free software so I would like to learn Lean in nvim rather than VS Code (which also seems to be hard to install in my Linux distro anyway). Following the Arch wiki, I installed elan and then install stable Lean 4. Now I'm a bit struggling to install the lean plugin for nvim. I don't have yet a configuration file for nvim as I never used it before (I only used vim for a few years). Could someone help me creating a configuration file for nvim and installing the plugin for lean?

[Julian Berman]

Hi! Welcome! I'm afraid my spare time this week is near 0, so another fellow lean.nvim user may be able to walk you through things a bit slower if need be, but here's at least a start hopefully. You have 2 choices:

• a super minimal setup with just lean.nvim (and a package manager, which in theory you could also get rid of but it's easier to explain with one)
• a Neovim distribution that installs a bunch of plugins.

For the former, you can essentially do 2 things:

• https://lazy.folke.io/installation has a "single-file" block of code you can place at ~/.config/nvim/init.lua
• where it says "spec", i.e. which plugins you want, take this and put it there: https://github.com/Julian/lean.nvim/blob/main/.devcontainer/lazyvim/lean.lua#L2-L17 to install lean.nvim

For the latter, LazyNvim is what I demo there in the lean.nvim repo, in which case you take that whole file from lean.vim and place it at ~/.config/nvim/plugins

I'm out of time for the moment but do ask questions and I'll try and pop back in, or someone else will help I'm sure.

[Matthew Ballard]

Caution: I just dump everything into init.lua but https://github.com/mattrobball/nvim has a copy.

Do you have a ~/.config/nvim folder?

[Michael Novak]

Julian Berman said:

Hi! Welcome! I'm afraid my spare time this week is near 0, so another fellow lean.nvim user may be able to walk you through things a bit slower if need be, but here's at least a start hopefully. You have 2 choices:

• a super minimal setup with just lean.nvim (and a package manager, which in theory you could also get rid of but it's easier to explain with one)
• a Neovim distribution that installs a bunch of plugins.

For the former, you can essentially do 2 things:

• https://lazy.folke.io/installation has a "single-file" block of code you can place at ~/.config/nvim/init.lua
• where it says "spec", i.e. which plugins you want, take this and put it there: https://github.com/Julian/lean.nvim/blob/main/.devcontainer/lazyvim/lean.lua#L2-L17 to install lean.nvim

For the latter, LazyNvim is what I demo there in the lean.nvim repo, in which case you take that whole file from lean.vim and place it at ~/.config/nvim/plugins

I'm out of time for the moment but do ask questions and I'll try and pop back in, or someone else will help I'm sure.

Thank you very much! I did what you suggested for the LazyNvim and I think it worked, but when I open nvim I always get this message:

# Plugin Updates
- **lazy.nvim**
- **nvim-lspconfig**
- **plenary.nvim**
Press ENTER or type command to continue

What do I need to do?

[Michael Novak]

Matthew Ballard said:

Caution: I just dump everything into init.lua but https://github.com/mattrobball/nvim has a copy.

Do you have a ~/.config/nvim folder?

Yes

[Matthew Ballard]

I would guess that you could dump that init.lua file there, open nvim, :PackerUpdate (or maybe other Packer invocations) to get up and running. You may need to create some directory in the file also.

[Michael Novak]

I created an init.lua file in ~/.config/nvim and I copied the single file from the LazyNvim website, and then after where it says spec I pasted what Julian told me to (without the return). Maybe I should do what Julian said in the end:

For the latter, LazyNvim is what I demo there in the lean.nvim repo, in which case you take that whole file from lean.vim and place it at ~/.config/nvim/plugins

I just didn't understand which file is he talking about about and also I don't have a plugins directory (but I can create one if it's needed).
I also tried to do the :PackerUpdate command in nvim but it seems like there isn't such a command

[Matthew Ballard]

Hmm, I don't remember doing anything else when I migrated to my lima vm.

[Michael Novak]

Inside ~/.config/nvim I have an init.lua file with the follwing:

- Bootstrap lazy.nvim
 local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"
 if not (vim.uv or vim.loop).fs_stat(lazypath) then
   local lazyrepo = "https://github.com/folke/lazy.nvim.git"
   local out = vim.fn.system({ "git", "clone", "--filter=blob:none", "--branch=stable", lazyrepo, lazypath })
   if vim.v.shell_error ~= 0 then
     vim.api.nvim_echo({
      { "Failed to clone lazy.nvim:\n", "ErrorMsg" },
       { out, "WarningMsg" },
       { "\nPress any key to exit..." },
     }, true, {})
     vim.fn.getchar()
     os.exit(1)
   end
 end
 vim.opt.rtp:prepend(lazypath)

 -- Make sure to setup `mapleader` and `maplocalleader` before
 -- loading lazy.nvim so that mappings are correct.
 -- This is also a good place to setup other settings (vim.opt)
 vim.g.mapleader = " "
 vim.g.maplocalleader = "\\"

 -- Setup lazy.nvim
 require("lazy").setup({
   spec = {
     -- add your plugins here
   {
     'Julian/lean.nvim',
      dependencies = {
       'nvim-lua/plenary.nvim',
       'neovim/nvim-lspconfig',
     },
     ---@module 'lean'
     ---@type lean.Config
     opts = {
       infoview = {
         horizontal_position = 'top',
         show_processing = false,
       },
       mappings = true,
     },
   },
   },
   -- Configure any other settings here. See the documentation for more details.
   -- colorscheme that will be used when installing plugins.
   install = { colorscheme = { "habamax" } },
   -- automatically check for plugin updates
   checker = { enabled = true },
})

And I also have a lazy-lock.file that was created automatically. Is that fine?

[Matthew Ballard]

I know nothing about lazynvim, apologies.

[Julian Berman]

@Michael Novak does :Lazy update make your upgrade message disappear?

[Michael Novak]

Julian Berman said:

Michael Novak does :Lazy update make your upgrade message disappear?

Yes! Thank you very much!

[Michael Novak]

I've started learning from the mathematics in lean book using nvim and everything works pretty well, but I was wondering if it's possible to get the lean code to be a bit more colorful, because right now it's mainly just white with some parts in bold. Maybe that's something related to nvim syntax highlighting, I'm not sure.

[Julian Berman]

Everyone has their favorite color scheme generally, I use kanagawa personally -- you can see what that looks like in the demo video in lean.nvim's README, but it's still essentially 3 or 4 main colors you'll see at a time. If you're someone who's expecting rainbow sorbet you can thumbs up https://github.com/leanprover/lean4/issues/2305

[Michael Novak]

Thank you very much! Where do I need to put the use "rebelot/kanagawa.nvim" line? Is it fine to put in the end of the init.lua file?

[Julian Berman]

in the spec table, say above the table you added with lean.nvim's own configuration, add these lines: https://github.com/Julian/dotfiles/blob/main/.config/nvim/lua/plugins/init.lua#L2-L13

[Michael Novak]

It worked! Thank you very much again and sorry for the stupid questions

[Julian Berman]

Great, no worries, glad you're off the ground, now hopefully you can focus on Lean itself :)!

[Jakub Nowak]

I'll drop a hint, one thing I use all the time is :lua vim.lsp.buf.hover() command, which will show you the documentation for the function/variable/tactic under the cursor.

[Julian Berman]

(Good tip certainly.) In any sufficiently new version of Neovim, i.e. ones lean.nvim supports, this should simply be pressing K.

[Jakub Nowak]

Oh, didn't knew that, I have my own mapping for that. Is there also a default mapping for :lua vim.lsp.buf.code_action()?

[Julian Berman]

Yes, :h gra -- though I find <C-a> easier for that.