From 2eb59c1ccd4e7c8ff61ae6c570e7f61804b052e0 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Mon, 16 Oct 2023 16:57:00 -0400
Subject: [PATCH] Split off the Lean 3 health check.

---
 lua/lean/health.lua                    | 44 ++++++++------------------
 lua/lean/lean3/health.lua              | 21 ++++++++++++
 lua/lean/{lean3.lua => lean3/init.lua} |  5 +--
 lua/lean/lsp.lua                       |  1 +
 lua/tests/checkhealth_spec.lua         |  1 -
 lua/tests/lean3/checkhealth_spec.lua   | 11 +++++++
 6 files changed, 49 insertions(+), 34 deletions(-)
 create mode 100644 lua/lean/lean3/health.lua
 rename lua/lean/{lean3.lua => lean3/init.lua} (99%)
 create mode 100644 lua/tests/lean3/checkhealth_spec.lua

diff --git a/lua/lean/health.lua b/lua/lean/health.lua
index e170fa9f..23a2c01e 100644
--- a/lua/lean/health.lua
+++ b/lua/lean/health.lua
@@ -2,48 +2,30 @@
 --- Support for `:checkhealth` for lean.nvim.
 ---@brief ]]
 
-local health = {}
-
-local Job = require('plenary.job')
 local subprocess_check_output = require('lean._util').subprocess_check_output
 
 local function check_lean_runnable()
   local lean = subprocess_check_output{ command = "lean", args = { "--version" } }
-  vim.health.report_ok('`lean --version`')
-  vim.health.report_info(table.concat(lean, '\n'))
-end
-
-local function check_lean3ls_runnable()
-  local succeeded, lean3ls = pcall(Job.new, Job, {
-    command = 'lean-language-server',
-    args = { '--stdio' },
-    writer = ''
-  })
-  if succeeded then
-    lean3ls:sync()
-    vim.health.report_ok('`lean-language-server`')
-  else
-    vim.health.report_warn('`lean-language-server` not found, lean 3 support will not work')
-  end
+  vim.health.ok('`lean --version`')
+  vim.health.info(table.concat(lean, '\n'))
 end
 
 local function check_for_timers()
   if not vim.tbl_isempty(vim.fn.timer_info()) then
-    vim.health.report_warn(
+    vim.health.warn(
       'You have active timers, which can degrade infoview (CursorMoved) ' ..
       'performance. See https://github.com/Julian/lean.nvim/issues/92.'
     )
   end
 end
 
---- Check whether lean.nvim is healthy.
----
---- Call me via `:checkhealth lean`.
-function health.check()
-  vim.health.report_start('lean.nvim')
-  check_lean_runnable()
-  check_lean3ls_runnable()
-  check_for_timers()
-end
-
-return health
+return {
+  --- Check whether lean.nvim is healthy.
+  ---
+  --- Call me via `:checkhealth lean`.
+  check = function()
+    vim.health.start('lean.nvim')
+    check_lean_runnable()
+    check_for_timers()
+  end
+}
diff --git a/lua/lean/lean3/health.lua b/lua/lean/lean3/health.lua
new file mode 100644
index 00000000..a71eb63c
--- /dev/null
+++ b/lua/lean/lean3/health.lua
@@ -0,0 +1,21 @@
+local Job = require('plenary.job')
+
+return {
+  --- Check whether Lean 3 support is healthy.
+  ---
+  --- Call me via `:checkhealth lean3`.
+  check = function()
+    vim.health.start('lean3')
+    local succeeded, lean3ls = pcall(Job.new, Job, {
+      command = 'lean-language-server',
+      args = { '--stdio' },
+      writer = ''
+    })
+    if succeeded then
+      lean3ls:sync()
+      vim.health.ok('`lean-language-server`')
+    else
+      vim.health.warn('`lean-language-server` not found, lean 3 support will not work')
+    end
+  end
+}
diff --git a/lua/lean/lean3.lua b/lua/lean/lean3/init.lua
similarity index 99%
rename from lua/lean/lean3.lua
rename to lua/lean/lean3/init.lua
index dd884220..c0646dcc 100644
--- a/lua/lean/lean3.lua
+++ b/lua/lean/lean3/init.lua
@@ -1,9 +1,10 @@
+local a = require'plenary.async.util'
+
 local Element = require('lean.widgets').Element
 local components = require('lean.infoview.components')
 local lsp = require('lean.lsp')
 local util = require('lean._util')
-local a = require'plenary.async.util'
-local progress = require"lean.progress"
+local progress = require('lean.progress')
 local subprocess_check_output = util.subprocess_check_output
 
 local lean3 = {}
diff --git a/lua/lean/lsp.lua b/lua/lean/lsp.lua
index f3ba6c5f..199af056 100644
--- a/lua/lean/lsp.lua
+++ b/lua/lean/lsp.lua
@@ -19,6 +19,7 @@ end
 --- given bufnr.
 function lsp.get_lean4_server(bufnr)
   local lean_client
+  -- local clients = vim.lsp.get_clients{ name = 'leanls' }
   vim.lsp.for_each_buffer_client(bufnr, function (client)
     if client.name == 'leanls' then lean_client = client end
   end)
diff --git a/lua/tests/checkhealth_spec.lua b/lua/tests/checkhealth_spec.lua
index 639275fd..7a6b5f15 100644
--- a/lua/tests/checkhealth_spec.lua
+++ b/lua/tests/checkhealth_spec.lua
@@ -7,7 +7,6 @@ describe('checkhealth', function()
 .*lean.nvim.*
 .*- .*OK.* `lean ----version`
 .*-.* Lean .*version .+
-.*- .*OK.* `lean--language--server`
 ]], table.concat(vim.api.nvim_buf_get_lines(0, 0, -1, false), '\n'))
   end)
 end)
diff --git a/lua/tests/lean3/checkhealth_spec.lua b/lua/tests/lean3/checkhealth_spec.lua
new file mode 100644
index 00000000..ba37cc13
--- /dev/null
+++ b/lua/tests/lean3/checkhealth_spec.lua
@@ -0,0 +1,11 @@
+require('tests.helpers')
+
+describe('checkhealth', function()
+  it('passes the health check', function()
+    vim.api.nvim_command('silent checkhealth lean3')
+    assert.has_match([[
+.*lean3:.*
+.*- .*OK.* `lean--language--server`
+]], table.concat(vim.api.nvim_buf_get_lines(0, 0, -1, false), '\n'))
+  end)
+end)