lean.nvim build failed error when opening NeoVim

Stream: new members

[Michael Novak]

When opening nvim, the lazy plugin updates opens (I think on install mode, because it is highlighted compared to the others - Update, Sync, ...) and I get this error message:

Home (H)   Install (I)   Update (U)   Sync (S)   Clean (X)
    Check (C)   Log (L)   Restore (R)   Profile (P)   Debug (D)
    Help (?)

   Total: 7 plugins

   Failed (1)
     ● lean.nvim 41.09ms  start
         Failed to spawn process luarocks {
           args = { "--tree", "/home/michael/.local/share/nvim/lazy-rocks/lean.nvim", "
           cwd = "/home/michael/.local/share/nvim/lazy/lean.nvim",
           env = {
             PATH = "/home/michael/.local/share/nvim/lazy-rocks/hererocks/bin:/home/mic
           },
           on_line = <function 1>,
           timeout = 120000
         }
         Failed installing lean.nvim with `luarocks`.

         ------------------------------------------------------------------------------

         Trying to build from source.
         Failed to spawn process luarocks {
           args = { "--tree", "/home/michael/.local/share/nvim/lazy-rocks/lean.nvim", "
 16           cwd = "/home/michael/.local/share/nvim/lazy/lean.nvim",
 15           env = {
             PATH = "/home/michael/.local/share/nvim/lazy-rocks/hererocks/bin:/home/mic
           },
           on_line = <function 1>,
           timeout = 120000
         }

   Loaded (5)
     ● kanagawa.nvim 5.87ms  start
     ● lazy.nvim 169.21ms  init.lua
     ● nvim-lspconfig 6.34ms  lean.nvim
     ● plenary.nvim 0.37ms  lean.nvim
     ● telescope.nvim 0.84ms 󰢱 telescope  lean.nvim

   Not Loaded (1)
      ○ hererocks

I can still use lean in nvim without any problem, but I just wanted to make sure that this is a known issue that will be fixed in the future and not a more serious problem, I should have to do something about.

[Julian Berman]

That looks like the error is saying it's trying to install lean.nvim from Luarocks. I have no idea what magic nonsense is causing it to suddenly do that and I have to teach in an hour and then work after that so I don't have time to look at the minute -- if things are working and it just started happening it's almost certainly nothing you did. Feel free to open an issue and I can find why lazy.nvim is trying to detect where to install things from without being asked to.

[Michael Novak]

When you say open an issue, do you mean in the github page of lean.nvim? I just never used github, sorry if that's an obvious question. If so, it's probably a good opportunity for me to open a github account, since I plan in the future to contribute to mathlib. Anyway thank you very much for taking the time to respond despite being so busy, take your time, don't feel pressure, as I said lean still works despite this error message.

[Julian Berman]

yes on lean.nvim and my pleasure!