diff options
| author | awy <awy@awy.one> | 2025-10-18 00:10:58 +0300 | 
|---|---|---|
| committer | awy <awy@awy.one> | 2025-10-18 00:10:58 +0300 | 
| commit | abf932d721142a35e01a57ab9187ca35896cb237 (patch) | |
| tree | 2cce67586b1792f33fd703072673b2a0767b473e /.config/nvim/lsp/lean3ls.lua | |
| parent | de009fd679e10d053fdcc10785f91ad5317449ea (diff) | |
| download | hyprdots-abf932d721142a35e01a57ab9187ca35896cb237.tar.gz | |
revert
Diffstat (limited to '.config/nvim/lsp/lean3ls.lua')
| -rw-r--r-- | .config/nvim/lsp/lean3ls.lua | 40 | 
1 files changed, 0 insertions, 40 deletions
diff --git a/.config/nvim/lsp/lean3ls.lua b/.config/nvim/lsp/lean3ls.lua deleted file mode 100644 index aefbbe9..0000000 --- a/.config/nvim/lsp/lean3ls.lua +++ /dev/null @@ -1,40 +0,0 @@ ----@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`. - ----@type vim.lsp.Config -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, -}  |