diff options
author | Michael Smith <mikesmiffy128@gmail.com> | 2024-07-15 20:05:47 +0100 |
---|---|---|
committer | Michael Smith <mikesmiffy128@gmail.com> | 2024-07-15 20:05:47 +0100 |
commit | 522d56557b00246286d803425751a4334f3a94a5 (patch) | |
tree | 23ca335a3526197c2a6327ce10bfd58411b0a609 /start/lspconfig-0.1.3/lua/lspconfig/server_configurations/lean3ls.lua | |
parent | a7b72fc27edac2305dbf0af807981bd703835b25 (diff) |
indent-blankline is probably old because I've actually been using it for
ages, but I have a strict if-it-ain't-broke policy, so I'm not going to
update it.
lspconfig *was* broke though with nvim 0.10, so now it's fixed.
Diffstat (limited to 'start/lspconfig-0.1.3/lua/lspconfig/server_configurations/lean3ls.lua')
-rw-r--r-- | start/lspconfig-0.1.3/lua/lspconfig/server_configurations/lean3ls.lua | 54 |
1 files changed, 0 insertions, 54 deletions
diff --git a/start/lspconfig-0.1.3/lua/lspconfig/server_configurations/lean3ls.lua b/start/lspconfig-0.1.3/lua/lspconfig/server_configurations/lean3ls.lua deleted file mode 100644 index b35a693..0000000 --- a/start/lspconfig-0.1.3/lua/lspconfig/server_configurations/lean3ls.lua +++ /dev/null @@ -1,54 +0,0 @@ -local util = require 'lspconfig.util' - -local bin_name = 'lean-language-server' -local args = { '--stdio', '--', '-M', '4096', '-T', '100000' } -local cmd = { bin_name, unpack(args) } - -if vim.fn.has 'win32' == 1 then - cmd = { 'cmd.exe', '/C', bin_name, unpack(args) } -end - -return { - default_config = { - cmd = cmd, - filetypes = { 'lean3' }, - offset_encoding = 'utf-32', - root_dir = function(fname) - fname = util.path.sanitize(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 - - return util.root_pattern 'leanpkg.toml'(fname) - or util.root_pattern 'leanpkg.path'(fname) - or stdlib_dir - or util.find_git_ancestor(fname) - end, - single_file_support = true, - }, - docs = { - description = [[ -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`. - ]], - default_config = { - root_dir = [[root_pattern("leanpkg.toml") or root_pattern(".git")]], - }, - }, -} |