Add support for the Lean 4 LSP, served by lake. (#4952)

ale_linters/lean/lake.vim

@@ -0,0 +1,28 @@
+" Author: Benjamin Block <https://github.com/benjamindblock>
+" Description: A language server for Lean 4.
+
+function! ale_linters#lean#lake#GetProjectRoot(buffer) abort
+    let l:lakefile_toml = ale#path#FindNearestFile(a:buffer, 'lakefile.toml')
+    let l:lakefile_lean = ale#path#FindNearestFile(a:buffer, 'lakefile.lean')
+
+    if !empty(l:lakefile_toml)
+        return fnamemodify(l:lakefile_toml, ':p:h')
+    elseif !empty(l:lakefile_lean)
+        return fnamemodify(l:lakefile_lean, ':p:h')
+    else
+        return fnamemodify('', ':h')
+    endif
+endfunction
+
+call ale#Set('lean_lake_executable', 'lake')
+call ale#Set('lean_lake_config', {})
+
+call ale#linter#Define('lean', {
+\   'name': 'lake',
+\   'lsp': 'stdio',
+\   'language': 'lean',
+\   'lsp_config': {b -> ale#Var(b, 'lean_lake_config')},
+\   'executable': {b -> ale#Var(b, 'lean_lake_executable')},
+\   'command': '%e serve',
+\   'project_root': function('ale_linters#lean#lake#GetProjectRoot'),
+\})

doc/ale-lean.txt

@@ -0,0 +1,29 @@
+===============================================================================
+ALE Lean Integration                                         *ale-lean-options*
+                                                         *ale-integration-lean*
+
+===============================================================================
+Integration Information
+
+  Currently, the only supported LSP for Lean 4 is lake.
+
+===============================================================================
+lake                                                            *ale-lean-lake*
+
+g:ale_lean_lake_executable                         *g:ale_lean_lake_executable*
+                                                   *b:ale_lean_lake_executable*
+  Type: |String|
+  Default: `'lake'`
+
+  This variable can be modified to change the executable path for `lake`.
+
+
+g:ale_lean_lake_config                                 *g:ale_lean_lake_config*
+                                                       *b:ale_lean_lake_config*
+  Type: |Dictionary|
+  Default: `{}`
+
+  Dictionary with configuration settings for lake.
+
+===============================================================================
+  vim:tw=78:ts=2:sts=2:sw=2:ft=help:norl:

doc/ale-supported-languages-and-tools.txt

@@ -370,6 +370,8 @@ Notes:
   * `textlint`
   * `vale`
   * `write-good`
+* Lean 4
+  * `lake`
 * Less
   * `lessc`
   * `prettier`

doc/ale.txt

@@ -3632,6 +3632,8 @@ documented in additional help files.
     cspell................................|ale-latex-cspell|
     write-good............................|ale-latex-write-good|
     textlint..............................|ale-latex-textlint|
+  lean....................................|ale-lean-options|
+    lake..................................|ale-lean-lake|
   less....................................|ale-less-options|
     lessc.................................|ale-less-lessc|
     prettier..............................|ale-less-prettier|

supported-tools.md

@@ -379,6 +379,8 @@ formatting.
   * [textlint](https://textlint.github.io/)
   * [vale](https://github.com/ValeLint/vale)
   * [write-good](https://github.com/btford/write-good)
+* Lean 4
+  * [lake](https://github.com/leanprover/lean4)
 * Less
   * [lessc](https://www.npmjs.com/package/less)
   * [prettier](https://github.com/prettier/prettier)

test/linter/test_lean_lake.vader

@@ -0,0 +1,27 @@
+Before:
+  call ale#assert#SetUpLinterTest('lean', 'lake')
+
+After:
+  call ale#assert#TearDownLinterTest()
+
+Execute(The default executable path should be correct):
+  AssertLinter 'lake', ale#Escape('lake') . ' serve'
+
+Execute(The project root should be detected correctly without a lakefile):
+  AssertLSPProject '.'
+
+Execute(The project root should be detected correctly from .toml):
+  call ale#test#SetFilename('../test-files/lean/lakefile_toml/lakefile.toml')
+  AssertLSPProject ale#path#Simplify(g:dir . '/../test-files/lean/lakefile_toml')
+
+Execute(The project root should be detected correctly from .lean):
+  call ale#test#SetFilename('../test-files/lean/lakefile_lean/lakefile.lean')
+  AssertLSPProject ale#path#Simplify(g:dir . '/../test-files/lean/lakefile_lean')
+
+Execute(The LSP values should be set correctly):
+  call ale#test#SetFilename('../test-files/lean/lakefile_lean/Main.lean')
+
+  AssertLSPLanguage 'lean'
+  AssertLSPOptions {}
+  AssertLSPConfig {}
+  AssertLSPProject ale#path#Simplify(g:dir . '/../test-files/lean/lakefile_lean')