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.8/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.8/lua/lspconfig/server_configurations/lean3ls.lua')
-rw-r--r-- | start/lspconfig-0.1.8/lua/lspconfig/server_configurations/lean3ls.lua | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/start/lspconfig-0.1.8/lua/lspconfig/server_configurations/lean3ls.lua b/start/lspconfig-0.1.8/lua/lspconfig/server_configurations/lean3ls.lua new file mode 100644 index 0000000..ebcec10 --- /dev/null +++ b/start/lspconfig-0.1.8/lua/lspconfig/server_configurations/lean3ls.lua @@ -0,0 +1,46 @@ +local util = require 'lspconfig.util' + +return { + default_config = { + cmd = { 'lean-language-server', '--stdio', '--', '-M', '4096', '-T', '100000' }, + 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")]], + }, + }, +} |