Add a thing we'll use to skip Lean 3 tests when not present.

.luacheckrc

@@ -1,6 +1,8 @@
 globals = {
-    "_clean_buffer_count",
-    "vim",
-    "lean_nvim_default_filetype",
-    assert = {fields = {"message"}},
+  "_clean_buffer_count",
+  "vim",
+  "lean_nvim_default_filetype",
+  "describe",
+  "it",
+  assert = {fields = {"message"}},
 }

lua/lean/lean3/health.lua

@@ -1,18 +1,11 @@
-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()
+    if require('lean.lean3').works() then
       vim.health.ok('`lean-language-server`')
     else
       vim.health.warn('`lean-language-server` not found, lean 3 support will not work')

lua/lean/lean3/init.lua

@@ -1,4 +1,5 @@
-local a = require'plenary.async.util'
+local Job = require('plenary.job')
+local a = require('plenary.async.util')
 
 local Element = require('lean.widgets').Element
 local components = require('lean.infoview.components')
@@ -10,6 +11,20 @@ local subprocess_check_output = util.subprocess_check_output
 local lean3 = {}
 
 
+--- Check if Lean 3 is installed on the current system.
+---
+--- @return boolean succeeded whether starting Lean 3 worked or not
+function lean3.works()
+  local succeeded, lean3ls = pcall(Job.new, Job, {
+    command = 'lean-language-server',
+    args = { '--stdio' },
+    writer = ''
+  })
+  if succeeded then lean3ls:sync() end
+  return succeeded
+end
+
+
 --- Return the current Lean 3 search path.
 ---
 --- Includes both the Lean 3 core libraries as well as project-specific

lua/tests/helpers.lua

@@ -1,12 +1,26 @@
 local assert = require('luassert')
 
-local dedent = require('lean._util').dedent
-local lean_lsp_diagnostics = require('lean._util').lean_lsp_diagnostics
 local fixtures = require('tests.fixtures')
 local infoview = require('lean.infoview')
 local progress = require('lean.progress')
+local util = require('lean._util')
 
-local helpers = {_clean_buffer_counter = 1}
+local helpers = { _clean_buffer_counter = 1 }
+
+--- Run the given tests if Lean 3 is available, otherwise skip.
+if require('lean.lean3').works() then
+  function helpers.if_has_lean3(description, fn)
+    return describe(description, fn)
+  end
+else
+  function helpers.if_has_lean3(description, _)
+    return describe(description, function()
+      it('lean 3 missing', function()
+        print('Lean 3 missing. Skipping.')
+      end)
+    end)
+  end
+end
 
 --- Feed some keystrokes into the current buffer, replacing termcodes.
 function helpers.feed(text, feed_opts)
@@ -136,7 +150,7 @@ end
 function helpers.wait_for_line_diagnostics()
   local succeeded, _ = vim.wait(15000, function()
     if progress.is_processing(vim.uri_from_bufnr(0)) then return false end
-    local diagnostics = lean_lsp_diagnostics{
+    local diagnostics = util.lean_lsp_diagnostics{
       lnum = vim.api.nvim_win_get_cursor(0)[1] - 1
     }
 
@@ -171,7 +185,7 @@ assert:register('assertion', 'contents', has_buf_contents)
 
 --- Assert about the current infoview contents.
 local function has_infoview_contents(_, arguments)
-  local expected = dedent(arguments[1][1] or arguments[1])
+  local expected = util.dedent(arguments[1][1] or arguments[1])
   local target_infoview = arguments[1].infoview or infoview.get_current_infoview()
   -- In Lean 3, the fileProgress notification is unreliable,
   -- so we may think we're done processing when we're actually not.
@@ -207,15 +221,15 @@ end
 
 --- Assert about the current infoview contents without waiting for the pins to load.
 local function has_infoview_contents_nowait(_, arguments)
-  local expected = dedent(arguments[1][1] or arguments[1])
+  local expected = util.dedent(arguments[1][1] or arguments[1])
   local target_infoview = arguments[1].infoview or infoview.get_current_infoview()
   local got = table.concat(target_infoview:get_lines(), '\n')
   assert.are.same(expected, got)
   return true
 end
 
 local function has_diff_contents(_, arguments)
-  local expected = dedent(arguments[1][1] or arguments[1])
+  local expected = util.dedent(arguments[1][1] or arguments[1])
   local target_infoview = arguments[1].infoview or infoview.get_current_infoview()
   local got = table.concat(target_infoview:get_diff_lines(), '\n')
   assert.are.same(expected, got)

lua/tests/lean3/checkhealth_spec.lua

@@ -1,6 +1,6 @@
-require('tests.helpers')
+local if_has_lean3 = require('tests.helpers').if_has_lean3
 
-describe('checkhealth', function()
+if_has_lean3('checkhealth', function()
   it('passes the health check', function()
     vim.api.nvim_command('silent checkhealth lean3')
     assert.has_match([[

lua/tests/lean3/ft_spec.lua

@@ -3,7 +3,7 @@ local fixtures = require('tests.fixtures')
 
 require('lean').setup { lsp3 = { enable = true } }
 
-describe('ft.detect', function()
+helpers.if_has_lean3('ft.detect', function()
   for kind, path in unpack(fixtures.lean3_project.files_it) do
     it('detects ' .. kind .. ' lean 3 files', function()
       vim.cmd('edit! ' .. path)