From 23d53b5d7bc2f31eed672c0a8d26dc608fb6d0ba Mon Sep 17 00:00:00 2001 From: Ibrahim Muftee Date: Mon, 4 Aug 2025 07:45:42 -0500 Subject: feat(nvim) slim down new config --- dot_config/nvim_new/lsp/lean3ls.lua | 39 +++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 dot_config/nvim_new/lsp/lean3ls.lua (limited to 'dot_config/nvim_new/lsp/lean3ls.lua') diff --git a/dot_config/nvim_new/lsp/lean3ls.lua b/dot_config/nvim_new/lsp/lean3ls.lua new file mode 100644 index 0000000..07ff059 --- /dev/null +++ b/dot_config/nvim_new/lsp/lean3ls.lua @@ -0,0 +1,39 @@ +---@brief +--- +--- https://github.com/leanprover/lean-client-js/tree/master/lean-language-server +--- +--- Lean installation instructions can be found +--- [here](https://leanprover-community.github.io/get_started.html#regular-install). +--- +--- Once Lean is installed, you can install the Lean 3 language server by running +--- ```sh +--- npm install -g lean-language-server +--- ``` +--- +--- Note: that if you're using [lean.nvim](https://github.com/Julian/lean.nvim), +--- that plugin fully handles the setup of the Lean language server, +--- and you shouldn't set up `lean3ls` both with it and `lspconfig`. + +return { + cmd = { 'lean-language-server', '--stdio', '--', '-M', '4096', '-T', '100000' }, + filetypes = { 'lean3' }, + offset_encoding = 'utf-32', + root_dir = function(bufnr, on_dir) + local fname = vim.api.nvim_buf_get_name(bufnr) + fname = vim.fs.normalize(fname) + -- check if inside elan stdlib + local stdlib_dir + do + local _, endpos = fname:find '/lean/library' + if endpos then + stdlib_dir = fname:sub(1, endpos) + end + end + + on_dir( + vim.fs.root(fname, { 'leanpkg.toml', 'leanpkg.path' }) + or stdlib_dir + or vim.fs.dirname(vim.fs.find('.git', { path = fname, upward = true })[1]) + ) + end, +} -- cgit v1.2.3