Try splitting off the Lean 3 health check.

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
+}

lua/lean/lean3.lua

@@ -1,12 +1,34 @@
+local Job = require('plenary.job')
+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 = {}
+local lean3 = {
+  health = {
+    --- 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
+  }
+}
 
 
 --- Return the current Lean 3 search path.

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)

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([[
+.*lean.nvim.*
+.*- .*OK.* `lean--language--server`
+]], table.concat(vim.api.nvim_buf_get_lines(0, 0, -1, false), '\n'))
+  end)
+end)