I have vague recollections this didn't work last time either :/

spec/ft_spec.lua

@@ -12,7 +12,7 @@ describe('ft.detect', function()
   end
 
   it('detects standard library files', function()
-    vim.cmd.edit { project.child 'Test/JumpToStdlib.lean', bang = true }
+    helpers.jump_to_core()
     assert.are.equal('lean', vim.bo.filetype)
     local initial_path = vim.api.nvim_buf_get_name(0)
 

spec/helpers.lua

@@ -57,6 +57,19 @@ function helpers.move_cursor(opts)
   vim.cmd.doautocmd 'CursorMoved'
 end
 
+--- Jump to an arbitrary file in Lean core.
+function helpers.jump_to_core()
+  vim.cmd.edit(fixtures.project.child 'Test/JumpToStdlib.lean')
+  vim.cmd.normal '$'
+
+  helpers.wait_for_ready_lsp()
+  vim.lsp.buf.definition()
+
+  assert.is_truthy(vim.wait(15000, function()
+    return vim.api.nvim_buf_get_name(0):match '.*/src/lean/.*'
+  end))
+end
+
 ---@class MoveCursorOpts
 ---@field window? integer @the window handle. Defaults to the current window.
 ---@field to table @the new cursor position (1-row indexed, as per nvim_win_set_cursor)

spec/helpers_spec.lua

@@ -84,3 +84,12 @@ describe(
     end
   )
 )
+
+describe('jump_to_core', function()
+  it('jumps to a file in core Lean', function()
+    helpers.jump_to_core()
+    local name = vim.api.nvim_buf_get_name(0)
+    local is_core = name:match '.*/src/lean/.*'
+    assert.message("Didn't jump to core Lean!").is_truthy(is_core)
+  end)
+end)