From 6c2fb86c6a03e20abea5ddd17d735885f0b7cb5e Mon Sep 17 00:00:00 2001 From: Michael Lingelbach Date: Wed, 24 Nov 2021 23:01:07 -0500 Subject: feat: expose configs --- lua/lspconfig/server_configurations/leanls.lua | 41 ++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 lua/lspconfig/server_configurations/leanls.lua (limited to 'lua/lspconfig/server_configurations/leanls.lua') diff --git a/lua/lspconfig/server_configurations/leanls.lua b/lua/lspconfig/server_configurations/leanls.lua new file mode 100644 index 00000000..f9bdaef9 --- /dev/null +++ b/lua/lspconfig/server_configurations/leanls.lua @@ -0,0 +1,41 @@ +local util = require 'lspconfig/util' + +return { + default_config = { + cmd = { 'lean', '--server' }, + filetypes = { 'lean' }, + root_dir = function(fname) + -- check if inside elan stdlib + local stdlib_dir + do + local _, endpos = fname:find(util.path.sep .. util.path.join('lib', 'lean')) + if endpos then + stdlib_dir = fname:sub(1, endpos) + end + end + + return util.root_pattern('lakefile.lean', 'lean-toolchain', 'leanpkg.toml')(fname) + or stdlib_dir + or util.find_git_ancestor(fname) + end, + single_file_support = true, + }, + docs = { + description = [[ +https://github.com/leanprover/lean4 + +Lean installation instructions can be found +[here](https://leanprover-community.github.io/get_started.html#regular-install). + +The Lean 4 language server is built-in with a Lean 4 install +(and can be manually run with, e.g., `lean --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 `leanls` both with it and `lspconfig`. + ]], + default_config = { + root_dir = [[root_pattern("lakefile.lean", "lean-toolchain", "leanpkg.toml", ".git")]], + }, + }, +} -- cgit v1.2.3-70-g09d2