From 71d7b70ee6fb5a5bfe984f33a78d316fe2f5a6c8 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Mon, 23 Oct 2023 20:15:44 -0400 Subject: [PATCH] Fix the infoview containing a trailing newline in one case. It was when interactive diagnostics are present. This is the main functional change of this commit -- but as part of it, the behavior of dedent as well as assert.contents and friends from the testing helpers have all changed to be what (to me) is more logical. This is the case even though there's still one "magic" behavior (in a new helper function _expected) which seems required to get a test in the abbreviations spec to pass. Also added here therefore are a bunch of tests for the testing helpers (and for dedent) which all pass and should help ensure that all this delicate code continues to work if it needs tweaking again. A secondary tweak to the testing helpers is that assert.contents and friends now automatically dedent their expected value, which makes the tests a bit more prettily indented. All the tests are then also refactored to use that "uniform" style for asserting against their contents, which is most of the whitespace change noise. --- lua/lean/_util.lua | 4 +- lua/lean/infoview/components.lua | 8 +- lua/tests/helpers.lua | 41 ++++--- lua/tests/helpers_spec.lua | 34 ++++++ lua/tests/infoview/contents_spec.lua | 14 --- lua/tests/infoview/pause_spec.lua | 9 -- lua/tests/infoview/pin_spec.lua | 3 +- lua/tests/language_support_spec.lua | 19 ++-- lua/tests/lean3/helpers.lua | 10 +- lua/tests/lean3/infoview/widgets_spec.lua | 1 - lua/tests/lean3/language_support_spec.lua | 19 ++-- lua/tests/lean3/sorry_spec.lua | 68 ++++++----- lua/tests/lean3/trythis_spec.lua | 131 ++++++++++++---------- lua/tests/sorry_spec.lua | 96 +++++++++------- lua/tests/util_spec.lua | 35 ++++++ 15 files changed, 294 insertions(+), 198 deletions(-) create mode 100644 lua/tests/helpers_spec.lua create mode 100644 lua/tests/util_spec.lua 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/helpers.lua b/lua/tests/lean3/helpers.lua index cb4139af..ca86275e 100644 --- a/lua/tests/lean3/helpers.lua +++ b/lua/tests/lean3/helpers.lua @@ -1,3 +1,4 @@ +local dedent = require('lean._util').dedent local helpers = { _clean_buffer_counter = 1 } -- Even though we can delete a buffer, so should be able to reuse names, @@ -15,9 +16,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(dedent(contents:gsub('^\n', '')):gsub('\n$', ''), '\n') end return function() @@ -29,7 +35,7 @@ function helpers.clean_buffer(contents, callback) vim.opt_local.swapfile = false vim.opt.filetype = 'lean3' - 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 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/lean3/trythis_spec.lua b/lua/tests/lean3/trythis_spec.lua index 030d0f0d..0567cda6 100644 --- a/lua/tests/lean3/trythis_spec.lua +++ b/lua/tests/lean3/trythis_spec.lua @@ -5,8 +5,9 @@ require('lean').setup {} helpers.if_has_lean3('trythis', function() it('replaces a single try this', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n") -example : ∃ n, n = 2 := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n") + example : ∃ n, n = 2 := by whatshouldIdo + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() @@ -15,8 +16,9 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() end)) it('replaces a single try this from by', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n") -example : ∃ n, n = 2 := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n") + example : ∃ n, n = 2 := by whatshouldIdo + ]], function() vim.cmd.normal('G$bb') helpers.wait_for_line_diagnostics() @@ -25,8 +27,9 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() end)) it('replaces a single try this from earlier in the line', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n") -example : ∃ n, n = 2 := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n") + example : ∃ n, n = 2 := by whatshouldIdo + ]], function() vim.cmd.normal('G0') helpers.wait_for_line_diagnostics() @@ -35,8 +38,9 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() end)) it('replaces a try this with even more unicode', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: existsi 0; intro m; refl") -example : ∃ n : nat, ∀ m : nat, m = m := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: existsi 0; intro m; refl") + example : ∃ n : nat, ∀ m : nat, m = m := by whatshouldIdo + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() @@ -47,8 +51,9 @@ example : ∃ n : nat, ∀ m : nat, m = m := by whatshouldIdo]], function() -- Emitted by e.g. hint -- luacheck: ignore it('replaces squashed together try this messages', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "the following tactics solve the goal\n---\nTry this: finish\nTry this: tauto\n") -example : ∃ n, n = 2 := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "the following tactics solve the goal\n---\nTry this: finish\nTry this: tauto\n") + example : ∃ n, n = 2 := by whatshouldIdo + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() @@ -58,26 +63,28 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() -- Emitted by e.g. pretty_cases it('replaces multiline try this messages', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2,\n refl,\n") -example : ∃ n, n = 2 := by { - whatshouldIdo -}]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2,\n refl,\n") + example : ∃ n, n = 2 := by { + whatshouldIdo + } + ]], function() vim.cmd.normal('3gg$') helpers.wait_for_line_diagnostics() require('lean.trythis').swap() assert.contents.are[[ -meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2,\n refl,\n") -example : ∃ n, n = 2 := by { - existsi 2, - refl, -}]] + meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2,\n refl,\n") + example : ∃ n, n = 2 := by { + existsi 2, + refl, + }]] end)) -- Emitted by e.g. library_search it('trims by exact foo to just foo', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: exact rfl") -example {n : nat} : n = n := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: exact rfl") + example {n : nat} : n = n := by whatshouldIdo + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() @@ -87,10 +94,11 @@ example {n : nat} : n = n := by whatshouldIdo]], function() -- Also emitted by e.g. library_search it('trims by exact foo to just foo', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: exact rfl") -structure foo := -(bar (n : nat) : n = n) -example : foo := ⟨by whatshouldIdo⟩]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: exact rfl") + structure foo := + (bar (n : nat) : n = n) + example : foo := ⟨by whatshouldIdo⟩ + ]], function() vim.cmd.normal('G$h') helpers.wait_for_line_diagnostics() @@ -101,8 +109,9 @@ example : foo := ⟨by whatshouldIdo⟩]], function() -- A line containing `squeeze_simp at bar` will re-suggest `at bar`, so -- ensure it doesn't appear twice it('trims simp at foo when it will be duplicated', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: simp [foo] at bar") -example {n : nat} : n = n := by whatshouldIdo at bar]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: simp [foo] at bar") + example {n : nat} : n = n := by whatshouldIdo at bar + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() @@ -112,10 +121,10 @@ example {n : nat} : n = n := by whatshouldIdo at bar]], function() -- Handle `squeeze_simp [foo]` similarly. it('trims simp [foo] when it will be duplicated', clean_buffer([[ -meta def whatshouldIdo (L : list name) := (do tactic.trace "Try this: simp [foo, baz]") -example {n : nat} : n = n := by whatshouldIdo [`nat] -]], function() - vim.cmd.normal('G$k') + meta def whatshouldIdo (L : list name) := (do tactic.trace "Try this: simp [foo, baz]") + example {n : nat} : n = n := by whatshouldIdo [`nat] + ]], function() + vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() require('lean.trythis').swap() @@ -124,8 +133,9 @@ example {n : nat} : n = n := by whatshouldIdo [`nat] -- Handle `squeeze_simp [foo] at bar` similarly. it('trims simp [foo] at bar when it will be duplicated', clean_buffer([[ -meta def whatshouldIdo (L : list name) := (do tactic.trace "Try this: simp [foo, baz] at bar") -example {n : nat} : n = n := by whatshouldIdo [`nat] at bar]], function() + meta def whatshouldIdo (L : list name) := (do tactic.trace "Try this: simp [foo, baz] at bar") + example {n : nat} : n = n := by whatshouldIdo [`nat] at bar + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() @@ -135,8 +145,9 @@ example {n : nat} : n = n := by whatshouldIdo [`nat] at bar]], function() -- Handle `squeeze_simp [foo] at *` similarly. it('trims simp [foo] at * when it will be duplicated', clean_buffer([[ -meta def whatshouldIdo (L : list name) := (do tactic.trace "Try this: simp [foo, baz] at *") -example {n : nat} : n = n := by whatshouldIdo [`nat] at *]], function() + meta def whatshouldIdo (L : list name) := (do tactic.trace "Try this: simp [foo, baz] at *") + example {n : nat} : n = n := by whatshouldIdo [`nat] at * + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() @@ -145,8 +156,9 @@ example {n : nat} : n = n := by whatshouldIdo [`nat] at *]], function() end)) it('replaces squashed suggestions from earlier in the line', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: exact rfl") -example {n : nat} : n = n := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: exact rfl") + example {n : nat} : n = n := by whatshouldIdo + ]], function() vim.cmd.normal('G0') helpers.wait_for_line_diagnostics() @@ -156,18 +168,19 @@ example {n : nat} : n = n := by whatshouldIdo]], function() -- Emitted by e.g. show_term it('replaces redundant brace-delimited term and tactic mode', clean_buffer([[ -meta def tactic.interactive.foo (t: tactic.interactive.itactic) : tactic.interactive.itactic := - (do tactic.trace "Try this: exact λ x y hxy, hf (hg hxy)\n") - -example {X Y Z : Type} {f : X → Y} {g : Y → Z} (hf : function.injective f) (hg : function.injective g) : function.injective (g ∘ f) := -begin - foo { - intros x y hxy, - apply hf, - apply hg, - apply hxy, - } -end]], function() + meta def tactic.interactive.foo (t: tactic.interactive.itactic) : tactic.interactive.itactic := + (do tactic.trace "Try this: exact λ x y hxy, hf (hg hxy)\n") + + example {X Y Z : Type} {f : X → Y} {g : Y → Z} (hf : function.injective f) (hg : function.injective g) : function.injective (g ∘ f) := + begin + foo { + intros x y hxy, + apply hf, + apply hg, + apply hxy, + } + end + ]], function() vim.cmd.normal('6gg3|') helpers.wait_for_line_diagnostics() @@ -175,18 +188,20 @@ end]], function() -- FIXME: With a bit more tweaking this should really trim the begin/exact/end assert.contents.are[[ -meta def tactic.interactive.foo (t: tactic.interactive.itactic) : tactic.interactive.itactic := - (do tactic.trace "Try this: exact λ x y hxy, hf (hg hxy)\n") - -example {X Y Z : Type} {f : X → Y} {g : Y → Z} (hf : function.injective f) (hg : function.injective g) : function.injective (g ∘ f) := -begin - exact λ x y hxy, hf (hg hxy) -end]] + meta def tactic.interactive.foo (t: tactic.interactive.itactic) : tactic.interactive.itactic := + (do tactic.trace "Try this: exact λ x y hxy, hf (hg hxy)\n") + + example {X Y Z : Type} {f : X → Y} {g : Y → Z} (hf : function.injective f) (hg : function.injective g) : function.injective (g ∘ f) := + begin + exact λ x y hxy, hf (hg hxy) + end + ]] end)) it('handles suggestions with quotes', clean_buffer([[ -meta def whatshouldIdo := (do tactic.trace "Try this: \"hi") -example : true := by whatshouldIdo]], function() + meta def whatshouldIdo := (do tactic.trace "Try this: \"hi") + example : true := by whatshouldIdo + ]], function() vim.cmd.normal('G$') helpers.wait_for_line_diagnostics() 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)