diff options
| author | github-actions[bot] <github-actions[bot]@users.noreply.github.com> | 2024-07-18 06:02:13 +0000 |
|---|---|---|
| committer | github-actions[bot] <github-actions[bot]@users.noreply.github.com> | 2024-07-18 06:02:13 +0000 |
| commit | df9c116cbcf0aa7e58f2b36b0296fa687e87f36f (patch) | |
| tree | 5cb47bea6de3cab6e4e65115e6daa5d23359dcda | |
| parent | feat(leanls): add support for lakefile.toml-only packages (#3238) (diff) | |
| download | nvim-lspconfig-df9c116cbcf0aa7e58f2b36b0296fa687e87f36f.tar nvim-lspconfig-df9c116cbcf0aa7e58f2b36b0296fa687e87f36f.tar.gz nvim-lspconfig-df9c116cbcf0aa7e58f2b36b0296fa687e87f36f.tar.bz2 nvim-lspconfig-df9c116cbcf0aa7e58f2b36b0296fa687e87f36f.tar.lz nvim-lspconfig-df9c116cbcf0aa7e58f2b36b0296fa687e87f36f.tar.xz nvim-lspconfig-df9c116cbcf0aa7e58f2b36b0296fa687e87f36f.tar.zst nvim-lspconfig-df9c116cbcf0aa7e58f2b36b0296fa687e87f36f.zip | |
docs: update server_configurations.md
skip-checks: true
| -rw-r--r-- | doc/server_configurations.md | 12 | ||||
| -rw-r--r-- | doc/server_configurations.txt | 12 |
2 files changed, 6 insertions, 18 deletions
diff --git a/doc/server_configurations.md b/doc/server_configurations.md index cf20c607..03b6b13d 100644 --- a/doc/server_configurations.md +++ b/doc/server_configurations.md @@ -6280,8 +6280,8 @@ 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`). +The Lean language server is included in any Lean installation and +does not require any additional packages. 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, @@ -6308,15 +6308,9 @@ require'lspconfig'.leanls.setup{} ```lua see source file ``` - - `options` : - ```lua - { - no_lake_lsp_cmd = { "lean", "--server" } - } - ``` - `root_dir` : ```lua - root_pattern("lakefile.lean", "lean-toolchain", "leanpkg.toml", ".git") + root_pattern("lakefile.toml", "lakefile.lean", "lean-toolchain", ".git") ``` - `single_file_support` : ```lua diff --git a/doc/server_configurations.txt b/doc/server_configurations.txt index cf20c607..03b6b13d 100644 --- a/doc/server_configurations.txt +++ b/doc/server_configurations.txt @@ -6280,8 +6280,8 @@ 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`). +The Lean language server is included in any Lean installation and +does not require any additional packages. 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, @@ -6308,15 +6308,9 @@ require'lspconfig'.leanls.setup{} ```lua see source file ``` - - `options` : - ```lua - { - no_lake_lsp_cmd = { "lean", "--server" } - } - ``` - `root_dir` : ```lua - root_pattern("lakefile.lean", "lean-toolchain", "leanpkg.toml", ".git") + root_pattern("lakefile.toml", "lakefile.lean", "lean-toolchain", ".git") ``` - `single_file_support` : ```lua |