From 57109ecf97d9e6554ed0a1fe7e2ff4cc174dd1cf Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Tue, 17 Oct 2023 22:30:36 -0400 Subject: [PATCH] One more. --- lua/tests/current_search_paths_spec.lua | 31 +++---------------- lua/tests/lean3/current_search_paths_spec.lua | 25 +++++++++++++++ 2 files changed, 29 insertions(+), 27 deletions(-) create mode 100644 lua/tests/lean3/current_search_paths_spec.lua diff --git a/lua/tests/current_search_paths_spec.lua b/lua/tests/current_search_paths_spec.lua index cd4eeacd..90b4b1f6 100644 --- a/lua/tests/current_search_paths_spec.lua +++ b/lua/tests/current_search_paths_spec.lua @@ -1,11 +1,7 @@ -local lean = require('lean') local helpers = require('tests.helpers') local fixtures = require('tests.fixtures') -require('lean').setup { - lsp = { enable = true }, - lsp3 = { enable = true }, -} +require('lean').setup { lsp = { enable = true } } describe('lean.current_search_paths', function() for kind, path in unpack(fixtures.lean_project.files_it) do @@ -13,34 +9,15 @@ describe('lean.current_search_paths', function() vim.api.nvim_command('edit ' .. path) helpers.wait_for_ready_lsp() - local paths = lean.current_search_paths() + local paths = require('lean').current_search_paths() assert.are_equal(3, #paths) -- via its leanpkg.path: assert.has_all( table.concat(paths, '\n') .. '\n', - { "/lib/lean\n", -- standard library - fixtures.lean_project.path .. '\n', -- the project itself + { "/lib/lean\n", -- standard library + fixtures.lean_project.path .. '\n', -- the project itself fixtures.lean_project.path .. '/foo\n' } -- its dependency ) end) end - - for kind, path in unpack(fixtures.lean3_project.files_it) do - it(string.format('returns the paths for %s lean3 files', kind), function() - vim.api.nvim_command('edit ' .. path) - helpers.wait_for_ready_lsp() - - local paths = lean.current_search_paths() - assert.are_equal(3, #paths) - -- via its leanpkg.path: - assert.has_all( - table.concat(paths, '\n') .. '\n', - { - '/lib/lean/library\n', -- Lean 3 standard library - fixtures.lean3_project.path .. '/src\n', -- the project itself - fixtures.lean3_project.path .. '/_target/deps/mathlib/src\n' -- the project itself - } - ) - end) - end end) diff --git a/lua/tests/lean3/current_search_paths_spec.lua b/lua/tests/lean3/current_search_paths_spec.lua new file mode 100644 index 00000000..6d3bbb98 --- /dev/null +++ b/lua/tests/lean3/current_search_paths_spec.lua @@ -0,0 +1,25 @@ +local helpers = require('tests.helpers') +local fixtures = require('tests.fixtures') + +require('lean').setup { lsp3 = { enable = true } } + +helpers.if_has_lean3('lean.current_search_paths', function() + for kind, path in unpack(fixtures.lean3_project.files_it) do + it(string.format('returns the paths for %s lean 3 files', kind), function() + vim.api.nvim_command('edit ' .. path) + helpers.wait_for_ready_lsp() + + local paths = require('lean').current_search_paths() + assert.are_equal(3, #paths) + -- via its leanpkg.path: + assert.has_all( + table.concat(paths, '\n') .. '\n', + { + '/lib/lean/library\n', -- Lean 3 standard library + fixtures.lean3_project.path .. '/src\n', -- the project itself + fixtures.lean3_project.path .. '/_target/deps/mathlib/src\n' -- the project itself + } + ) + end) + end +end)