Skip to content

Commit df9c116

Browse files
docs: update server_configurations.md
skip-checks: true
1 parent a481793 commit df9c116

File tree

2 files changed

+6
-18
lines changed

2 files changed

+6
-18
lines changed

doc/server_configurations.md

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6280,8 +6280,8 @@ https://github.com/leanprover/lean4
62806280
Lean installation instructions can be found
62816281
[here](https://leanprover-community.github.io/get_started.html#regular-install).
62826282

6283-
The Lean 4 language server is built-in with a Lean 4 install
6284-
(and can be manually run with, e.g., `lean --server`).
6283+
The Lean language server is included in any Lean installation and
6284+
does not require any additional packages.
62856285

62866286
Note: that if you're using [lean.nvim](https://github.com/Julian/lean.nvim),
62876287
that plugin fully handles the setup of the Lean language server,
@@ -6308,15 +6308,9 @@ require'lspconfig'.leanls.setup{}
63086308
```lua
63096309
see source file
63106310
```
6311-
- `options` :
6312-
```lua
6313-
{
6314-
no_lake_lsp_cmd = { "lean", "--server" }
6315-
}
6316-
```
63176311
- `root_dir` :
63186312
```lua
6319-
root_pattern("lakefile.lean", "lean-toolchain", "leanpkg.toml", ".git")
6313+
root_pattern("lakefile.toml", "lakefile.lean", "lean-toolchain", ".git")
63206314
```
63216315
- `single_file_support` :
63226316
```lua

doc/server_configurations.txt

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6280,8 +6280,8 @@ https://github.com/leanprover/lean4
62806280
Lean installation instructions can be found
62816281
[here](https://leanprover-community.github.io/get_started.html#regular-install).
62826282

6283-
The Lean 4 language server is built-in with a Lean 4 install
6284-
(and can be manually run with, e.g., `lean --server`).
6283+
The Lean language server is included in any Lean installation and
6284+
does not require any additional packages.
62856285

62866286
Note: that if you're using [lean.nvim](https://github.com/Julian/lean.nvim),
62876287
that plugin fully handles the setup of the Lean language server,
@@ -6308,15 +6308,9 @@ require'lspconfig'.leanls.setup{}
63086308
```lua
63096309
see source file
63106310
```
6311-
- `options` :
6312-
```lua
6313-
{
6314-
no_lake_lsp_cmd = { "lean", "--server" }
6315-
}
6316-
```
63176311
- `root_dir` :
63186312
```lua
6319-
root_pattern("lakefile.lean", "lean-toolchain", "leanpkg.toml", ".git")
6313+
root_pattern("lakefile.toml", "lakefile.lean", "lean-toolchain", ".git")
63206314
```
63216315
- `single_file_support` :
63226316
```lua

0 commit comments

Comments
 (0)