High-level idea of how the infoview in lean.nvim works?

Stream: general

[nrs]

I'm trying to set up my lsp so that it depends on elan instead of the lean or lake commands, so I've disabled lean.nvim's lsp config and manually added my own autocmd with vim.api.nvim_create_autocmd and vim.lsp.start. Issue is, this only configures the lsp and having the infoview reflect the proof state by using what's given by the lsp isn't set up by this. Would anyone have a high-level idea/overview of how the infoview interacts with the lsp so I can configure it in lua?

[Julian Berman]

I'm not sure I follow -- elan provides (wraps) those two commands. Specifically lean.nvim is out of the box expecting to be using elan. What issue were you having?

[nrs]

Julian Berman said:

I'm not sure I follow -- elan provides (wraps) those two commands. Specifically lean.nvim is out of the box expecting to be using elan. What issue were you having?

If I check :LspInfo, the command used to start the lsp is lake serve, and for some reason List.IsSuffix is not recognized when importing import Init.Data.List.Basic. This issue disappears when I start the lsp with elan run stable lake serve

[nrs]

ah, it turns out I was using an outdated version of lean.nvim! thanks for pointing out that it's expected to use elan, with the newest version I now get a call to elan