diff --git a/lua/lean/_util.lua b/lua/lean/_util.lua index 00dbb594..0188e02c 100644 --- a/lua/lean/_util.lua +++ b/lua/lean/_util.lua @@ -102,9 +102,9 @@ end --- --- REPLACEME: plenary.nvim has a version of this but it has odd behavior. function M.dedent(str) - str = str:gsub(" +$", ""):gsub("^ +", "") -- remove spaces at start and end + str = str:gsub('^ +', ''):gsub('\n *$', '\n') -- trim leading/trailing space local prefix = max_common_indent(str) - return (str:gsub("\n" .. prefix, "\n"):gsub("\n$", "")) + return str:gsub('\n' .. prefix, '\n') end function M.load_mappings(mappings, buffer) diff --git a/lua/lean/infoview/components.lua b/lua/lean/infoview/components.lua index f2de6d63..f4bab3e4 100644 --- a/lua/lean/infoview/components.lua +++ b/lua/lean/infoview/components.lua @@ -70,7 +70,7 @@ function components.term_goal(term_goal) return { Element:new{ - text = H(string.format('expected type (%s)', range_to_string(term_goal.range)) .. "\n" .. term_goal.goal), + text = H(('expected type (%s)'):format(range_to_string(term_goal.range)) .. '\n' .. term_goal.goal), name = 'term-goal' } } @@ -308,7 +308,7 @@ local function tagged_text_msg_embed(t, sess, parent_cls) local element = Element:new{ name = 'code-with-infos' } if t.text ~= nil then - element.text = t.text + element.text = t.text:gsub('\n$', '') elseif t.append ~= nil then for _, s in ipairs(t.append) do element:add_child(tagged_text_msg_embed(s, sess)) @@ -441,9 +441,9 @@ function components.interactive_diagnostics(diags, line, sess) text = H(string.format('%s: %s:\n', range_to_string(diag.range), util.DIAGNOSTIC_SEVERITY[diag.severity])), - name = 'diagnostic' + name = 'diagnostic', + children = { tagged_text_msg_embed(diag.message, sess) } } - element:add_child(tagged_text_msg_embed(diag.message, sess)) table.insert(elements, element) end end diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua index 0b8c4142..bdffe85b 100644 --- a/lua/tests/helpers.lua +++ b/lua/tests/helpers.lua @@ -140,9 +140,14 @@ end -- -- Yes c(lean) may be a double entendre, and no I don't feel bad. function helpers.clean_buffer(contents, callback) + local lines + + -- Support a 1-arg version where we assume the contents is an empty buffer. if callback == nil then callback = contents - contents = '' + lines = {} + else + lines = vim.split(util.dedent(contents:gsub('^\n', '')):gsub('\n$', ''), '\n') end return function() @@ -154,7 +159,7 @@ function helpers.clean_buffer(contents, callback) vim.opt_local.swapfile = false vim.opt.filetype = 'lean' - vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, vim.split(contents, '\n')) + vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, lines) vim.api.nvim_buf_call(bufnr, function() callback{ source_file = { bufnr = bufnr } } end) end end @@ -206,20 +211,28 @@ local function has_current_window(_, arguments) end assert:register('assertion', 'current_window', has_current_window) +local function _expected(arguments) + local expected = arguments[1][1] or arguments[1] + -- Handle cases where we're indeed checking for a real trailing newline. + local dedented = util.dedent(expected) + if dedented ~= expected then + expected = dedented:gsub('\n$', '') + end + return expected +end + --- Assert about the entire buffer contents. local function has_buf_contents(_, arguments) - local expected = arguments[1][1] or arguments[1] local bufnr = arguments[1].bufnr or 0 local got = table.concat(vim.api.nvim_buf_get_lines(bufnr, 0, -1, false), '\n') - assert.is.equal(expected, got) + assert.is.equal(_expected(arguments), got) return true end - assert:register('assertion', 'contents', has_buf_contents) --- Assert about the current infoview contents. local function has_infoview_contents(_, arguments) - local expected = util.dedent(arguments[1][1] or arguments[1]) + local expected = _expected(arguments) 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. @@ -227,8 +240,8 @@ local function has_infoview_contents(_, arguments) -- To address this, we assume that we'll only assert -- nonempty contents in the Lean 3 tests, and retry updating the current pin -- until we get something. - if vim.opt.filetype:get() == "lean3" then - assert.are_not.same(expected, "") + if vim.opt.filetype:get() == 'lean3' then + assert.are_not.same(expected, '') local succeeded, _ = pcall(helpers.wait_for_loading_pins, target_infoview) local curr_pin = target_infoview.info.pin @@ -243,30 +256,28 @@ local function has_infoview_contents(_, arguments) end end - assert.message("never got Lean 3 data").is_true(succeeded and #got ~= 0) + assert.message('never got Lean 3 data').is_true(succeeded and #got ~= 0) else helpers.wait_for_loading_pins(target_infoview) end - local got = table.concat(target_infoview:get_lines(), '\n') - assert.are.same(expected, got) + local got = table.concat(target_infoview:get_lines(), '\n'):gsub('\n$', '') + assert.is.equal(expected, got) return true end --- Assert about the current infoview contents without waiting for the pins to load. local function has_infoview_contents_nowait(_, arguments) - 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) + assert.are.same(_expected(arguments), got) return true end local function has_diff_contents(_, arguments) - 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) + assert.are.same(_expected(arguments), got) return true end diff --git a/lua/tests/helpers_spec.lua b/lua/tests/helpers_spec.lua new file mode 100644 index 00000000..15bc0a34 --- /dev/null +++ b/lua/tests/helpers_spec.lua @@ -0,0 +1,34 @@ +---@brief [[ +--- Tests for our own testing helpers. +---@brief ]] + +local helpers = require('tests.helpers') + +describe('clean_buffer <-> assert.contents', function() + it('creates single line buffers', helpers.clean_buffer('foo bar', function() + assert.are.same( + vim.api.nvim_buf_get_lines(0, 0, -1, false), { 'foo bar' } + ) + assert.contents.are('foo bar') + end)) + + it('creates multiline buffers', helpers.clean_buffer([[ + foo + bar + ]], function() + assert.are.same( + vim.api.nvim_buf_get_lines(0, 0, -1, false), { 'foo', 'bar' } + ) + assert.contents.are[[ + foo + bar + ]] + end)) + + it('detects actual intended trailing newlines', helpers.clean_buffer('foo\n\n', function() + assert.are.same( + vim.api.nvim_buf_get_lines(0, 0, -1, false), { 'foo', '' } + ) + assert.contents.are('foo\n') + end)) +end) diff --git a/lua/tests/infoview/contents_spec.lua b/lua/tests/infoview/contents_spec.lua index c274120a..bc1f1355 100644 --- a/lua/tests/infoview/contents_spec.lua +++ b/lua/tests/infoview/contents_spec.lua @@ -37,21 +37,17 @@ describe('infoview content (auto-)update', function() -- In theory we don't care where we are, but the right answer changes assert.are.same(vim.api.nvim_win_get_cursor(0), {1, 0}) - -- FIXME: Trailing extra newline. assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] end) it('updates when the cursor moves', function() helpers.move_cursor{ to = {3, 0} } - -- FIXME: Trailing extra newline. assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] end) @@ -64,14 +60,12 @@ describe('infoview content (auto-)update', function() assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] helpers.move_cursor{ to = {1, 0} } assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] -- Now switch back to the other window and we see the original location... @@ -80,7 +74,6 @@ describe('infoview content (auto-)update', function() assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] vim.api.nvim_win_close(second_window, false) @@ -111,14 +104,12 @@ describe('infoview content (auto-)update', function() assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] helpers.move_cursor{ to = {3, 0} } assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] end) @@ -144,7 +135,6 @@ describe('infoview content (auto-)update', function() assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] vim.cmd.tabnew(fixtures.project.path .. '/Test/Squares.lean') @@ -152,7 +142,6 @@ describe('infoview content (auto-)update', function() assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] -- But the first tab's contents are unchanged even without re-entering. @@ -160,7 +149,6 @@ describe('infoview content (auto-)update', function() [[ ▶ 1:1-1:6: information: 1 - ]], infoview = tab1_infoview } @@ -177,14 +165,12 @@ describe('infoview content (auto-)update', function() assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] helpers.move_cursor{ to = {1, 0} } assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] vim.cmd(tab2 .. 'tabclose') diff --git a/lua/tests/infoview/pause_spec.lua b/lua/tests/infoview/pause_spec.lua index d8b53cca..d27fcf43 100644 --- a/lua/tests/infoview/pause_spec.lua +++ b/lua/tests/infoview/pause_spec.lua @@ -16,19 +16,15 @@ describe('infoview pause/unpause', function() it("can pause and unpause updates", function(_) vim.cmd('edit! ' .. fixtures.project.path .. '/Test/Squares.lean') helpers.move_cursor{ to = {3, 0} } - -- FIXME: Trailing extra newline. assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] helpers.move_cursor{ to = {1, 0} } - -- FIXME: Trailing extra newline. assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] -- FIXME: Demeter is angry. @@ -45,25 +41,20 @@ describe('infoview pause/unpause', function() assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] -- Unpausing triggers an update. pin:unpause() - -- FIXME: Trailing extra newline. assert.infoview_contents.are[[ ▶ 3:1-3:6: information: 9.000000 - ]] -- And continued movement continues updating. helpers.move_cursor{ to = {1, 0} } - -- FIXME: Trailing extra newline. assert.infoview_contents.are[[ ▶ 1:1-1:6: information: 1 - ]] end) diff --git a/lua/tests/infoview/pin_spec.lua b/lua/tests/infoview/pin_spec.lua index 6a76ab85..445f3496 100644 --- a/lua/tests/infoview/pin_spec.lua +++ b/lua/tests/infoview/pin_spec.lua @@ -1,13 +1,12 @@ ---@brief [[ --- Tests for the placing of infoview pins. ---@brief ]] -local dedent = require('lean._util').dedent local infoview = require('lean.infoview') local helpers = require('tests.helpers') require('lean').setup{ lsp = { enable = true } } -describe('infoview pins', helpers.clean_buffer(dedent[[ +describe('infoview pins', helpers.clean_buffer([[ theorem has_tactic_goal : p ∨ q → q ∨ p := by intro h cases h with diff --git a/lua/tests/language_support_spec.lua b/lua/tests/language_support_spec.lua index ced58b0d..04eccc08 100644 --- a/lua/tests/language_support_spec.lua +++ b/lua/tests/language_support_spec.lua @@ -2,7 +2,6 @@ --- Tests for basic Lean language support. ---@brief ]] -local dedent = require('lean._util').dedent local helpers = require('tests.helpers') require('lean').setup{} @@ -14,24 +13,26 @@ describe('commenting', function() end)) it('comments out multiple lines inline by default', helpers.clean_buffer([[ -def foo := 12 -def bar := 37]], function() + def foo := 12 + def bar := 37 + ]], function() vim.cmd(':% TComment') - assert.contents.are(dedent[[ + assert.contents.are[[ -- def foo := 12 -- def bar := 37 - ]]) + ]] end)) it('can comment out block comments', helpers.clean_buffer([[ -def foo := 12 -def bar := 37]], function() + def foo := 12 + def bar := 37 + ]], function() vim.cmd(':% TCommentBlock') - assert.contents.are(dedent[[ + assert.contents.are[[ /- def foo := 12 def bar := 37 -/ - ]]) + ]] end)) end) diff --git a/lua/tests/lean3/infoview/widgets_spec.lua b/lua/tests/lean3/infoview/widgets_spec.lua index 1192301e..e10e4b87 100644 --- a/lua/tests/lean3/infoview/widgets_spec.lua +++ b/lua/tests/lean3/infoview/widgets_spec.lua @@ -57,7 +57,6 @@ helpers.if_has_lean3('infoview widgets', clean_buffer('example : 2 = 2 := by ref infoview.enable_widgets() helpers.move_cursor{ to = {1, 22} } -- we're looking for `filter` as our widget - -- FIXME: Extra newline only with widgets enabled assert.infoview_contents.are[[ filter: no filter ▶ 1 goal diff --git a/lua/tests/lean3/language_support_spec.lua b/lua/tests/lean3/language_support_spec.lua index cf5aaef4..0c4f508c 100644 --- a/lua/tests/lean3/language_support_spec.lua +++ b/lua/tests/lean3/language_support_spec.lua @@ -3,7 +3,6 @@ ---@brief ]] local clean_buffer = require('tests.lean3.helpers').clean_buffer -local dedent = require('lean._util').dedent local helpers = require('tests.helpers') require('lean').setup{} @@ -15,24 +14,26 @@ helpers.if_has_lean3('commenting', function() end)) it('comments out multiple lines inline by default', clean_buffer([[ -def foo := 12 -def bar := 37]], function() + def foo := 12 + def bar := 37 + ]], function() vim.cmd(':% TComment') - assert.contents.are(dedent[[ + assert.contents.are[[ -- def foo := 12 -- def bar := 37 - ]]) + ]] end)) it('can comment out block comments', clean_buffer([[ -def foo := 12 -def bar := 37]], function() + def foo := 12 + def bar := 37 + ]], function() vim.cmd(':% TCommentBlock') - assert.contents.are(dedent[[ + assert.contents.are[[ /- def foo := 12 def bar := 37 -/ - ]]) + ]] end)) end) diff --git a/lua/tests/lean3/sorry_spec.lua b/lua/tests/lean3/sorry_spec.lua index af6ad8e3..199ba4ee 100644 --- a/lua/tests/lean3/sorry_spec.lua +++ b/lua/tests/lean3/sorry_spec.lua @@ -5,26 +5,29 @@ require('lean').setup {} helpers.if_has_lean3('sorry', function() it('inserts sorries for each remaining goal', clean_buffer([[ -def foo (n : nat) : n = n := begin - induction n with d hd, -end]], function() + def foo (n : nat) : n = n := begin + induction n with d hd, + end + ]], function() vim.cmd('normal! 3gg$') helpers.wait_for_line_diagnostics() vim.cmd('normal! 2gg$') require('lean.sorry').fill() assert.contents.are[[ -def foo (n : nat) : n = n := begin - induction n with d hd, - { sorry }, - { sorry }, -end]] + def foo (n : nat) : n = n := begin + induction n with d hd, + { sorry }, + { sorry }, + end + ]] end)) it('leaves the cursor in the first sorry', clean_buffer([[ -def foo (n : nat) : n = n := begin - induction n with d hd, -end]], function() + def foo (n : nat) : n = n := begin + induction n with d hd, + end + ]], function() vim.cmd('normal! 3gg$') helpers.wait_for_line_diagnostics() @@ -32,42 +35,47 @@ end]], function() require('lean.sorry').fill() vim.cmd('normal! cefoo') assert.contents.are[[ -def foo (n : nat) : n = n := begin - induction n with d hd, - { foo }, - { sorry }, -end]] + def foo (n : nat) : n = n := begin + induction n with d hd, + { foo }, + { sorry }, + end + ]] end)) it('indents sorry blocks when needed', clean_buffer([[ -def foo (n : nat) : n = n := begin - induction n with d hd, + def foo (n : nat) : n = n := begin + induction n with d hd, -end]], function() + end + ]], function() vim.cmd('normal! 4gg$') helpers.wait_for_line_diagnostics() vim.cmd('normal! 3gg0') require('lean.sorry').fill() assert.contents.are[[ -def foo (n : nat) : n = n := begin - induction n with d hd, + def foo (n : nat) : n = n := begin + induction n with d hd, - { sorry }, - { sorry }, -end]] + { sorry }, + { sorry }, + end + ]] end)) it('does nothing if there are no goals', clean_buffer([[ -def foo (n : nat) : n = n := begin - refl, -end]], function() + def foo (n : nat) : n = n := begin + refl, + end + ]], function() vim.cmd('normal! 2gg$') require('lean.sorry').fill() assert.contents.are[[ -def foo (n : nat) : n = n := begin - refl, -end]] + def foo (n : nat) : n = n := begin + refl, + end + ]] end)) end) diff --git a/lua/tests/sorry_spec.lua b/lua/tests/sorry_spec.lua index 418646e2..d23544e8 100644 --- a/lua/tests/sorry_spec.lua +++ b/lua/tests/sorry_spec.lua @@ -5,105 +5,115 @@ require('lean').setup {} describe('sorry', function() it('inserts sorries for each of multiple remaining goals', clean_buffer([[ -example (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor]], function() + example (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor + ]], function() helpers.wait_for_line_diagnostics() vim.cmd('normal! 2gg$') require('lean.sorry').fill() assert.contents.are[[ -example (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor - · sorry - · sorry]] + example (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor + · sorry + · sorry + ]] end)) it('inserts a sorry for the remaining goal', clean_buffer([[ -example (p : Prop) : p → p := by]], function() + example (p : Prop) : p → p := by + ]], function() helpers.wait_for_line_diagnostics() vim.cmd('normal! gg$') require('lean.sorry').fill() assert.contents.are[[ -example (p : Prop) : p → p := by -sorry]] + example (p : Prop) : p → p := by + sorry + ]] end)) it('leaves the cursor in the first sorry', clean_buffer([[ -def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor]], function() + def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor + ]], function() helpers.wait_for_line_diagnostics() vim.cmd('normal! 2gg$') require('lean.sorry').fill() vim.cmd('normal! cebar') assert.contents.are[[ -def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor - · bar - · sorry]] + def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor + · bar + · sorry + ]] end)) it('leaves the cursor in the only sorry', clean_buffer([[ -def foo (p q : Prop) : p ∧ q → q ∧ p := by - intro h]], function() + def foo (p q : Prop) : p ∧ q → q ∧ p := by + intro h + ]], function() helpers.wait_for_line_diagnostics() vim.cmd('normal! 2gg$') require('lean.sorry').fill() vim.cmd('normal! cebar') assert.contents.are[[ -def foo (p q : Prop) : p ∧ q → q ∧ p := by - intro h - bar]] + def foo (p q : Prop) : p ∧ q → q ∧ p := by + intro h + bar + ]] end)) it('indents sorry blocks when needed', clean_buffer([[ -def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor + def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor -]], function() + ]], function() vim.cmd('normal! gg$') helpers.wait_for_line_diagnostics() vim.cmd('normal! 3gg0') require('lean.sorry').fill() assert.contents.are[[ -def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor + def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor - · sorry - · sorry -]] + · sorry + · sorry + ]] end)) it('single goal within multiple goal block', clean_buffer([[ -def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor - · intro h - · sorry -]], function() + def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor + · intro h + · sorry + ]], function() vim.cmd('normal! 3gg$') helpers.wait_for_line_diagnostics() require('lean.sorry').fill() assert.contents.are[[ -def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor - · intro h - sorry - · sorry -]] + def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by + constructor + · intro h + sorry + · sorry + ]] end)) it('does nothing if there are no goals', clean_buffer([[ -def foo (n : Nat) : n = n := by - rfl]], function() + def foo (n : Nat) : n = n := by + rfl + ]], function() vim.cmd('normal! 2gg$') require('lean.sorry').fill() assert.contents.are[[ -def foo (n : Nat) : n = n := by - rfl]] + def foo (n : Nat) : n = n := by + rfl + ]] end)) end) diff --git a/lua/tests/util_spec.lua b/lua/tests/util_spec.lua new file mode 100644 index 00000000..98be22e8 --- /dev/null +++ b/lua/tests/util_spec.lua @@ -0,0 +1,35 @@ +local dedent = require('lean._util').dedent + +describe('dedent', function() + it('dedents multiline strings by their common prefix', function() + assert.is.equal( + dedent[[ + foo bar + baz quux + ]], 'foo bar\nbaz quux\n') + end) + + it('leaves dedented lines alone', function() + assert.is.equal('foo bar', dedent('foo bar')) + end) + + it('dedents indented single lines', function() + assert.is.equal('foo ', dedent(' foo ')) + end) + + it('ignores empty lines', function() + assert.is.equal( + '\nfoo bar\n\n\nbaz quux\n\n', dedent[[ + + foo bar + + + baz quux + + ]]) + end) + + it('leaves single lines with trailing whitespace alone', function() + assert.is.equal('foo ', dedent('foo ')) + end) +end)