From 5d628888e7e075afd6b8c8e6818e172d4c8612a8 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Sun, 22 Oct 2023 11:59:11 -0400 Subject: [PATCH] Split the clean_buffer helper for lean3, simplifying it. --- .luacheckrc | 1 - .../abbreviations/abbreviations_spec.lua | 22 +++++------ lua/tests/diagnostics_spec.lua | 4 +- lua/tests/helpers.lua | 19 ++++++---- lua/tests/infoview/contents_spec.lua | 4 +- lua/tests/infoview/pin_spec.lua | 2 +- lua/tests/infoview/widgets_spec.lua | 2 +- lua/tests/language_support_spec.lua | 6 +-- lua/tests/lean3/abbreviations_spec.lua | 23 ++++++------ lua/tests/lean3/diagnostics_spec.lua | 4 +- lua/tests/lean3/helpers.lua | 37 +++++++++++++++++++ lua/tests/lean3/infoview/contents_spec.lua | 3 +- lua/tests/lean3/infoview/widgets_spec.lua | 3 +- lua/tests/lean3/language_support_spec.lua | 7 ++-- lua/tests/lean3/mappings_spec.lua | 7 ++-- lua/tests/lean3/sorry_spec.lua | 13 +++---- lua/tests/lean3/switch_spec.lua | 25 ++++++------- lua/tests/lean3/trythis_spec.lua | 31 ++++++++-------- lua/tests/mappings_spec.lua | 2 +- lua/tests/sorry_spec.lua | 20 +++++----- lua/tests/switch_spec.lua | 19 +++++----- lua/tests/trythis_spec.lua | 2 +- 22 files changed, 147 insertions(+), 109 deletions(-) create mode 100644 lua/tests/lean3/helpers.lua diff --git a/.luacheckrc b/.luacheckrc index 7535c8c5..d8413191 100644 --- a/.luacheckrc +++ b/.luacheckrc @@ -1,5 +1,4 @@ globals = { - "_clean_buffer_count", "vim", "lean_nvim_default_filetype", "describe", diff --git a/lua/tests/abbreviations/abbreviations_spec.lua b/lua/tests/abbreviations/abbreviations_spec.lua index 0f0f49d9..5e6b56ab 100644 --- a/lua/tests/abbreviations/abbreviations_spec.lua +++ b/lua/tests/abbreviations/abbreviations_spec.lua @@ -12,44 +12,44 @@ end require('lean').setup {} describe('unicode abbreviation expansion', function() - it('autoexpands abbreviations', helpers.clean_buffer('lean', '', function() + it('autoexpands abbreviations', helpers.clean_buffer(function() helpers.insert[[\a]] assert.contents.are[[α]] end)) describe('explicit triggers', function() - it('inserts a space on ', helpers.clean_buffer('lean', '', function() + it('inserts a space on ', helpers.clean_buffer(function() helpers.insert[[\e]] wait_for_expansion() assert.contents.are[[ε ]] end)) - it('inserts a newline on ', helpers.clean_buffer('lean', '', function() + it('inserts a newline on ', helpers.clean_buffer(function() helpers.insert[[\e]] wait_for_expansion() assert.contents.are('ε\n') end)) - it('inserts nothing on ', helpers.clean_buffer('lean', '', function() + it('inserts nothing on ', helpers.clean_buffer(function() helpers.insert[[\e]] wait_for_expansion() assert.contents.are[[ε]] end)) - it('leaves the cursor in the right spot on ', helpers.clean_buffer('lean', '', function() + it('leaves the cursor in the right spot on ', helpers.clean_buffer(function() helpers.insert[[\<abc]] wait_for_expansion() assert.contents.are[[⟨abc]] end)) - it('inserts nothing on mid-line', helpers.clean_buffer('lean', 'foo bar baz quux,', function() + it('inserts nothing on mid-line', helpers.clean_buffer('foo bar baz quux,', function() vim.cmd.normal('$') helpers.insert[[ \comp spam]] wait_for_expansion() assert.contents.are[[foo bar baz quux ∘ spam,]] end)) - it('does not interfere with existing mappings', helpers.clean_buffer('lean', '', function() + it('does not interfere with existing mappings', helpers.clean_buffer(function() vim.api.nvim_buf_set_keymap( 0, 'i', @@ -68,7 +68,7 @@ describe('unicode abbreviation expansion', function() vim.api.nvim_buf_del_keymap(0, 'i', '') end)) - it('does not interfere with existing lua mappings', helpers.clean_buffer('lean', '', function() + it('does not interfere with existing lua mappings', helpers.clean_buffer(function() vim.b.foo = 0 local inc = function() vim.b.foo = vim.b.foo + 1 end @@ -92,17 +92,17 @@ describe('unicode abbreviation expansion', function() end) -- Really this needs to place the cursor too, but for now we just strip - it('handles placing the $CURSOR', helpers.clean_buffer('lean', '', function() + it('handles placing the $CURSOR', helpers.clean_buffer(function() helpers.insert[[foo \<>bar, baz]] assert.current_line.is('foo ⟨bar, baz⟩') end)) - it('expands mid-word', helpers.clean_buffer('lean', '', function() + it('expands mid-word', helpers.clean_buffer(function() helpers.insert[[(\a]] assert.contents.are[[(α]] end)) - it('expands abbreviations in command mode', helpers.clean_buffer('lean', '', function() + it('expands abbreviations in command mode', helpers.clean_buffer(function() helpers.insert[[foo ε bar]] vim.cmd.normal('$') helpers.feed[[q/a\eibaz]] diff --git a/lua/tests/diagnostics_spec.lua b/lua/tests/diagnostics_spec.lua index 124934c7..398b29fe 100644 --- a/lua/tests/diagnostics_spec.lua +++ b/lua/tests/diagnostics_spec.lua @@ -4,9 +4,7 @@ local lean_lsp_diagnostics = require('lean._util').lean_lsp_diagnostics require('lean').setup { lsp = { enable = true } } describe('diagnostics', function() - it('are retrieved from the server', helpers.clean_buffer('lean', - [[ example : False := by trivial ]], - function() + it('are retrieved from the server', helpers.clean_buffer([[ example : False := by trivial ]], function() helpers.wait_for_line_diagnostics() local diags = lean_lsp_diagnostics() assert.are_equal(1, #diags) diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua index 2ad949e4..e1f39584 100644 --- a/lua/tests/helpers.lua +++ b/lua/tests/helpers.lua @@ -119,29 +119,32 @@ end -- Even though we can delete a buffer, so should be able to reuse names, -- we do this to ensure if a test fails, future ones still get new "files". -local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr, ft) +local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr) local counter = helpers._clean_buffer_counter helpers._clean_buffer_counter = helpers._clean_buffer_counter + 1 - local unique_name = - ft == 'lean3' and string.format('unittest-%d.lean', counter) - or string.format('%s/unittest-%d.lean', fixtures.lean_project.path, counter) + local unique_name = string.format('%s/unittest-%d.lean', fixtures.lean_project.path, counter) vim.api.nvim_buf_set_name(bufnr, unique_name) end ---- Create a clean Lean buffer of the given filetype with the given contents. +--- Create a clean Lean buffer with the given contents. -- -- Waits for the LSP to be ready before proceeding with a given callback. -- -- Yes c(lean) may be a double entendre, and no I don't feel bad. -function helpers.clean_buffer(ft, contents, callback) +function helpers.clean_buffer(contents, callback) + if callback == nil then + callback = contents + contents = '' + end + return function() local bufnr = vim.api.nvim_create_buf(false, false) - set_unique_name_so_we_always_have_a_separate_fake_file(bufnr, ft) + set_unique_name_so_we_always_have_a_separate_fake_file(bufnr) -- apparently necessary to trigger BufWinEnter vim.api.nvim_set_current_buf(bufnr) vim.opt_local.bufhidden = "hide" vim.opt_local.swapfile = false - vim.opt.filetype = ft + vim.opt.filetype = 'lean' vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, vim.split(contents, '\n')) vim.api.nvim_buf_call(bufnr, function() callback{ source_file = { bufnr = bufnr } } end) diff --git a/lua/tests/infoview/contents_spec.lua b/lua/tests/infoview/contents_spec.lua index 9a001c58..a76794a8 100644 --- a/lua/tests/infoview/contents_spec.lua +++ b/lua/tests/infoview/contents_spec.lua @@ -281,7 +281,7 @@ describe('infoview content (auto-)update', function() end) end) - describe('cursor position', helpers.clean_buffer('lean', '', function() + describe('cursor position', helpers.clean_buffer(function() it('is set to the goal line', function() local lines = { 'example ' } for i=1, 100 do @@ -301,7 +301,7 @@ describe('infoview content (auto-)update', function() end) end)) - describe('processing message', helpers.clean_buffer('lean', '#eval IO.sleep 5000', function() + describe('processing message', helpers.clean_buffer('#eval IO.sleep 5000', function() it('is shown while a file is processing', function() local uri = vim.uri_from_fname(vim.api.nvim_buf_get_name(0)) local result = vim.wait(15000, function() return require('lean.progress').is_processing(uri) end) diff --git a/lua/tests/infoview/pin_spec.lua b/lua/tests/infoview/pin_spec.lua index 4dd8f904..6a76ab85 100644 --- a/lua/tests/infoview/pin_spec.lua +++ b/lua/tests/infoview/pin_spec.lua @@ -7,7 +7,7 @@ local helpers = require('tests.helpers') require('lean').setup{ lsp = { enable = true } } -describe('infoview pins', helpers.clean_buffer('lean', dedent[[ +describe('infoview pins', helpers.clean_buffer(dedent[[ theorem has_tactic_goal : p ∨ q → q ∨ p := by intro h cases h with diff --git a/lua/tests/infoview/widgets_spec.lua b/lua/tests/infoview/widgets_spec.lua index bc72ee26..3f8d4e25 100644 --- a/lua/tests/infoview/widgets_spec.lua +++ b/lua/tests/infoview/widgets_spec.lua @@ -7,7 +7,7 @@ local helpers = require('tests.helpers') require('lean').setup{} -describe('infoview widgets', helpers.clean_buffer('lean', '#check Nat', function() +describe('infoview widgets', helpers.clean_buffer('#check Nat', function() local lean_window = vim.api.nvim_get_current_win() local current_infoview = infoview.get_current_infoview() diff --git a/lua/tests/language_support_spec.lua b/lua/tests/language_support_spec.lua index 5c6d33fc..ced58b0d 100644 --- a/lua/tests/language_support_spec.lua +++ b/lua/tests/language_support_spec.lua @@ -8,12 +8,12 @@ local helpers = require('tests.helpers') require('lean').setup{} describe('commenting', function() - it('comments out single lines', helpers.clean_buffer('lean', 'def best := 37', function() + it('comments out single lines', helpers.clean_buffer('def best := 37', function() vim.cmd.TComment() assert.contents.are('-- def best := 37') end)) - it('comments out multiple lines inline by default', helpers.clean_buffer('lean', [[ + it('comments out multiple lines inline by default', helpers.clean_buffer([[ def foo := 12 def bar := 37]], function() vim.cmd(':% TComment') @@ -23,7 +23,7 @@ def bar := 37]], function() ]]) end)) - it('can comment out block comments', helpers.clean_buffer('lean', [[ + it('can comment out block comments', helpers.clean_buffer([[ def foo := 12 def bar := 37]], function() vim.cmd(':% TCommentBlock') diff --git a/lua/tests/lean3/abbreviations_spec.lua b/lua/tests/lean3/abbreviations_spec.lua index c81ce42d..a6c9652c 100644 --- a/lua/tests/lean3/abbreviations_spec.lua +++ b/lua/tests/lean3/abbreviations_spec.lua @@ -1,4 +1,5 @@ local helpers = require('tests.helpers') +local clean_buffer = require('tests.lean3.helpers').clean_buffer -- Wait some time for the abbreviation to have been expanded. -- This is very naive, it just ensures the line contains no `\`. @@ -12,44 +13,44 @@ end require('lean').setup {} helpers.if_has_lean3('unicode abbreviation expansion', function() - it('autoexpands abbreviations', helpers.clean_buffer('lean3', '', function() + it('autoexpands abbreviations', clean_buffer(function() helpers.insert[[\a]] assert.contents.are[[α]] end)) describe('explicit triggers', function() - it('inserts a space on ', helpers.clean_buffer('lean3', '', function() + it('inserts a space on ', clean_buffer(function() helpers.insert[[\e]] wait_for_expansion() assert.contents.are[[ε ]] end)) - it('inserts a newline on ', helpers.clean_buffer('lean3', '', function() + it('inserts a newline on ', clean_buffer(function() helpers.insert[[\e]] wait_for_expansion() assert.contents.are('ε\n') end)) - it('inserts nothing on ', helpers.clean_buffer('lean3', '', function() + it('inserts nothing on ', clean_buffer(function() helpers.insert[[\e]] wait_for_expansion() assert.contents.are[[ε]] end)) - it('leaves the cursor in the right spot on ', helpers.clean_buffer('lean3', '', function() + it('leaves the cursor in the right spot on ', clean_buffer(function() helpers.insert[[\<abc]] wait_for_expansion() assert.contents.are[[⟨abc]] end)) - it('inserts nothing on mid-line', helpers.clean_buffer('lean3', 'foo bar baz quux,', function() + it('inserts nothing on mid-line', clean_buffer('foo bar baz quux,', function() vim.cmd.normal('$') helpers.insert[[ \comp spam]] wait_for_expansion() assert.contents.are[[foo bar baz quux ∘ spam,]] end)) - it('does not interfere with existing mappings', helpers.clean_buffer('lean3', '', function() + it('does not interfere with existing mappings', clean_buffer(function() vim.api.nvim_buf_set_keymap( 0, 'i', @@ -68,7 +69,7 @@ helpers.if_has_lean3('unicode abbreviation expansion', function() vim.api.nvim_buf_del_keymap(0, 'i', '') end)) - it('does not interfere with existing lua mappings', helpers.clean_buffer('lean3', '', function() + it('does not interfere with existing lua mappings', clean_buffer(function() vim.b.foo = 0 local inc = function() vim.b.foo = vim.b.foo + 1 end @@ -92,17 +93,17 @@ helpers.if_has_lean3('unicode abbreviation expansion', function() end) -- Really this needs to place the cursor too, but for now we just strip - it('handles placing the $CURSOR', helpers.clean_buffer('lean3', '', function() + it('handles placing the $CURSOR', clean_buffer(function() helpers.insert[[foo \<>bar, baz]] assert.current_line.is('foo ⟨bar, baz⟩') end)) - it('expands mid-word', helpers.clean_buffer('lean3', '', function() + it('expands mid-word', clean_buffer(function() helpers.insert[[(\a]] assert.contents.are[[(α]] end)) - it('expands abbreviations in command mode', helpers.clean_buffer('lean3', '', function() + it('expands abbreviations in command mode', clean_buffer(function() helpers.insert[[foo ε bar]] vim.cmd.normal('$') helpers.feed[[q/a\eibaz]] diff --git a/lua/tests/lean3/diagnostics_spec.lua b/lua/tests/lean3/diagnostics_spec.lua index e1ab7fbe..6e670f6f 100644 --- a/lua/tests/lean3/diagnostics_spec.lua +++ b/lua/tests/lean3/diagnostics_spec.lua @@ -1,11 +1,11 @@ +local clean_buffer = require('tests.lean3.helpers').clean_buffer local helpers = require('tests.helpers') local lean_lsp_diagnostics = require('lean._util').lean_lsp_diagnostics require('lean').setup { lsp3 = { enable = true } } helpers.if_has_lean3('diagnostics', function() - it('are retrieved from the server', helpers.clean_buffer('lean3', - [[ example : false := by trivial ]], + it('are retrieved from the server', clean_buffer([[ example : false := by trivial ]], function() helpers.wait_for_line_diagnostics() local diags = lean_lsp_diagnostics() diff --git a/lua/tests/lean3/helpers.lua b/lua/tests/lean3/helpers.lua new file mode 100644 index 00000000..cb4139af --- /dev/null +++ b/lua/tests/lean3/helpers.lua @@ -0,0 +1,37 @@ +local helpers = { _clean_buffer_counter = 1 } + +-- Even though we can delete a buffer, so should be able to reuse names, +-- we do this to ensure if a test fails, future ones still get new "files". +local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr) + local counter = helpers._clean_buffer_counter + helpers._clean_buffer_counter = helpers._clean_buffer_counter + 1 + local unique_name = string.format('unittest-%d.lean', counter) + vim.api.nvim_buf_set_name(bufnr, unique_name) +end + +--- Create a clean Lean buffer with the given contents. +-- +-- Waits for the LSP to be ready before proceeding with a given callback. +-- +-- Yes c(lean) may be a double entendre, and no I don't feel bad. +function helpers.clean_buffer(contents, callback) + if callback == nil then + callback = contents + contents = '' + end + + return function() + local bufnr = vim.api.nvim_create_buf(false, false) + set_unique_name_so_we_always_have_a_separate_fake_file(bufnr) + -- apparently necessary to trigger BufWinEnter + vim.api.nvim_set_current_buf(bufnr) + vim.opt_local.bufhidden = 'hide' + 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_call(bufnr, function() callback{ source_file = { bufnr = bufnr } } end) + end +end + +return helpers diff --git a/lua/tests/lean3/infoview/contents_spec.lua b/lua/tests/lean3/infoview/contents_spec.lua index 6d200c26..9316d449 100644 --- a/lua/tests/lean3/infoview/contents_spec.lua +++ b/lua/tests/lean3/infoview/contents_spec.lua @@ -1,3 +1,4 @@ +local clean_buffer = require('tests.lean3.helpers').clean_buffer local infoview = require('lean.infoview') local fixtures = require('tests.fixtures') local helpers = require('tests.helpers') @@ -63,7 +64,7 @@ helpers.if_has_lean3('components', function() end) end - describe('cursor position', helpers.clean_buffer('lean3', '', function() + describe('cursor position', clean_buffer(function() it('is set to the goal line', function() local lines = { 'example ' } for i=1, 100 do diff --git a/lua/tests/lean3/infoview/widgets_spec.lua b/lua/tests/lean3/infoview/widgets_spec.lua index 796cc786..7d7d2e4d 100644 --- a/lua/tests/lean3/infoview/widgets_spec.lua +++ b/lua/tests/lean3/infoview/widgets_spec.lua @@ -1,9 +1,10 @@ +local clean_buffer = require('tests.lean3.helpers').clean_buffer local helpers = require('tests.helpers') local infoview = require('lean.infoview') require('lean').setup {} -helpers.if_has_lean3('infoview widgets', helpers.clean_buffer('lean3', 'example : 2 = 2 := by refl', function() +helpers.if_has_lean3('infoview widgets', clean_buffer('example : 2 = 2 := by refl', function() local lean_window = vim.api.nvim_get_current_win() local current_infoview = infoview.get_current_infoview() diff --git a/lua/tests/lean3/language_support_spec.lua b/lua/tests/lean3/language_support_spec.lua index e8a2005b..cf5aaef4 100644 --- a/lua/tests/lean3/language_support_spec.lua +++ b/lua/tests/lean3/language_support_spec.lua @@ -2,18 +2,19 @@ --- Tests for basic Lean language support. ---@brief ]] +local clean_buffer = require('tests.lean3.helpers').clean_buffer local dedent = require('lean._util').dedent local helpers = require('tests.helpers') require('lean').setup{} helpers.if_has_lean3('commenting', function() - it('comments out single lines', helpers.clean_buffer('lean3', 'def best := 37', function() + it('comments out single lines', clean_buffer('def best := 37', function() vim.cmd.TComment() assert.contents.are('-- def best := 37') end)) - it('comments out multiple lines inline by default', helpers.clean_buffer('lean3', [[ + it('comments out multiple lines inline by default', clean_buffer([[ def foo := 12 def bar := 37]], function() vim.cmd(':% TComment') @@ -23,7 +24,7 @@ def bar := 37]], function() ]]) end)) - it('can comment out block comments', helpers.clean_buffer('lean3', [[ + it('can comment out block comments', clean_buffer([[ def foo := 12 def bar := 37]], function() vim.cmd(':% TCommentBlock') diff --git a/lua/tests/lean3/mappings_spec.lua b/lua/tests/lean3/mappings_spec.lua index 2b2c368a..60ce18aa 100644 --- a/lua/tests/lean3/mappings_spec.lua +++ b/lua/tests/lean3/mappings_spec.lua @@ -1,10 +1,11 @@ local lean = require('lean') -local helpers = require('tests.helpers') +local if_has_lean3 = require('tests.helpers').if_has_lean3 +local clean_buffer = require('tests.lean3.helpers').clean_buffer require('lean').setup {} -helpers.if_has_lean3('mappings', function() - it('are bound the current buffer and not others', helpers.clean_buffer('lean3', '', function() +if_has_lean3('mappings', function() + it('are bound the current buffer and not others', clean_buffer(function() lean.use_suggested_mappings(true) assert.is.same( lean.mappings.n['i'], diff --git a/lua/tests/lean3/sorry_spec.lua b/lua/tests/lean3/sorry_spec.lua index f42faf29..173c338a 100644 --- a/lua/tests/lean3/sorry_spec.lua +++ b/lua/tests/lean3/sorry_spec.lua @@ -1,11 +1,10 @@ local helpers = require('tests.helpers') -local clean_buffer = helpers.clean_buffer -local if_has_lean3 = require('tests.helpers').if_has_lean3 +local clean_buffer = require('tests.lean3.helpers').clean_buffer require('lean').setup {} -if_has_lean3('sorry', function() - it('inserts sorries for each remaining goal', clean_buffer('lean3', [[ +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() @@ -22,7 +21,7 @@ def foo (n : nat) : n = n := begin end]] end)) - it('leaves the cursor in the first sorry', clean_buffer('lean3', [[ + it('leaves the cursor in the first sorry', clean_buffer([[ def foo (n : nat) : n = n := begin induction n with d hd, end]], function() @@ -40,7 +39,7 @@ def foo (n : nat) : n = n := begin end]] end)) - it('indents sorry blocks when needed', clean_buffer('lean3', [[ + it('indents sorry blocks when needed', clean_buffer([[ def foo (n : nat) : n = n := begin induction n with d hd, @@ -59,7 +58,7 @@ def foo (n : nat) : n = n := begin end]] end)) - it('does nothing if there are no goals', clean_buffer('lean3', [[ + it('does nothing if there are no goals', clean_buffer([[ def foo (n : nat) : n = n := begin refl, end]], function() diff --git a/lua/tests/lean3/switch_spec.lua b/lua/tests/lean3/switch_spec.lua index d1aa48e3..b1528ffb 100644 --- a/lua/tests/lean3/switch_spec.lua +++ b/lua/tests/lean3/switch_spec.lua @@ -1,12 +1,11 @@ -local helpers = require('tests.helpers') -local clean_buffer = helpers.clean_buffer +local clean_buffer = require('tests.lean3.helpers').clean_buffer local if_has_lean3 = require('tests.helpers').if_has_lean3 require('lean').setup{} if_has_lean3('switch', function() it('switches between left and right', - clean_buffer('lean3', [[#check mul_right_comm]], function() + clean_buffer([[#check mul_right_comm]], function() vim.cmd('normal! 1gg12|') vim.cmd.Switch() assert.contents.are[[#check mul_left_comm]] @@ -16,7 +15,7 @@ if_has_lean3('switch', function() end)) it('switches between top and bot', - clean_buffer('lean3', [[#check with_top]], function() + clean_buffer([[#check with_top]], function() vim.cmd('normal! 1gg$') vim.cmd.Switch() assert.contents.are[[#check with_bot]] @@ -26,21 +25,21 @@ if_has_lean3('switch', function() end)) it('does not switch between top and bot prefix', - clean_buffer('lean3', [[#check tops]], function() + clean_buffer([[#check tops]], function() vim.cmd('normal! 1gg$hh') vim.cmd.Switch() assert.contents.are[[#check tops]] end)) it('does not switch between top and bot suffix', - clean_buffer('lean3', [[#check stop]], function() + clean_buffer([[#check stop]], function() vim.cmd('normal! 1gg$') vim.cmd.Switch() assert.contents.are[[#check stop]] end)) it('switches between mul and add', - clean_buffer('lean3', [[#check add_one]], function() + clean_buffer([[#check add_one]], function() vim.cmd('normal! 1gg9|') vim.cmd.Switch() assert.contents.are[[#check mul_one]] @@ -50,7 +49,7 @@ if_has_lean3('switch', function() end)) it('switches between zero and one', - clean_buffer('lean3', [[#check mul_one]], function() + clean_buffer([[#check mul_one]], function() vim.cmd('normal! 1gg$') vim.cmd.Switch() assert.contents.are[[#check mul_zero]] @@ -60,35 +59,35 @@ if_has_lean3('switch', function() end)) it('switches between exact <> and refine <>', - clean_buffer('lean3', [[exact ⟨foo, bar⟩]], function() + clean_buffer([[exact ⟨foo, bar⟩]], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[refine ⟨foo, bar⟩]] end)) it('does not switch between exact foo and refine foo', - clean_buffer('lean3', [[exact foo]], function() + clean_buffer([[exact foo]], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[exact foo]] end)) it('switches between simp only [foo] and simp', - clean_buffer("lean3", [=[simp only [foo, bar, baz]]=], function() + clean_buffer([=[simp only [foo, bar, baz]]=], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[simp]] end)) it('switches between simp and squeeze_simp', - clean_buffer("lean3", [[simp]], function() + clean_buffer([[simp]], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[squeeze_simp]] end)) it('switches between simp [foo] and squeeze_simp [foo]', - clean_buffer("lean3", [=[simp [foo, bar, baz]]=], function() + clean_buffer([=[simp [foo, bar, baz]]=], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[=[squeeze_simp [foo, bar, baz]]=] diff --git a/lua/tests/lean3/trythis_spec.lua b/lua/tests/lean3/trythis_spec.lua index ada23c40..7e526b25 100644 --- a/lua/tests/lean3/trythis_spec.lua +++ b/lua/tests/lean3/trythis_spec.lua @@ -1,9 +1,10 @@ local helpers = require('tests.helpers') +local clean_buffer = require('tests.lean3.helpers').clean_buffer require('lean').setup {} helpers.if_has_lean3('trythis', function() - it('replaces a single try this', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$') @@ -13,7 +14,7 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() assert.current_line.is('example : ∃ n, n = 2 := by existsi 2; refl') end)) - it('replaces a single try this from by', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$bb') @@ -23,7 +24,7 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() assert.current_line.is('example : ∃ n, n = 2 := by existsi 2; refl') end)) - it('replaces a single try this from earlier in the line', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G0') @@ -33,7 +34,7 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() assert.current_line.is('example : ∃ n, n = 2 := by existsi 2; refl') end)) - it('replaces a try this with even more unicode', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$') @@ -45,7 +46,7 @@ example : ∃ n : nat, ∀ m : nat, m = m := by whatshouldIdo]], function() -- Emitted by e.g. hint -- luacheck: ignore - it('replaces squashed together try this messages', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$') @@ -56,7 +57,7 @@ example : ∃ n, n = 2 := by whatshouldIdo]], function() end)) -- Emitted by e.g. pretty_cases - it('replaces multiline try this messages', helpers.clean_buffer('lean3', [[ + 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 @@ -74,7 +75,7 @@ example : ∃ n, n = 2 := by { end)) -- Emitted by e.g. library_search - it('trims by exact foo to just foo', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$') @@ -85,7 +86,7 @@ example {n : nat} : n = n := by whatshouldIdo]], function() end)) -- Also emitted by e.g. library_search - it('trims by exact foo to just foo', helpers.clean_buffer('lean3', [[ + 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) @@ -99,7 +100,7 @@ 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', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$') @@ -110,7 +111,7 @@ example {n : nat} : n = n := by whatshouldIdo at bar]], function() end)) -- Handle `squeeze_simp [foo]` similarly. - it('trims simp [foo] when it will be duplicated', helpers.clean_buffer('lean3', [[ + 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() @@ -122,7 +123,7 @@ example {n : nat} : n = n := by whatshouldIdo [`nat] end)) -- Handle `squeeze_simp [foo] at bar` similarly. - it('trims simp [foo] at bar when it will be duplicated', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$') @@ -133,7 +134,7 @@ example {n : nat} : n = n := by whatshouldIdo [`nat] at bar]], function() end)) -- Handle `squeeze_simp [foo] at *` similarly. - it('trims simp [foo] at * when it will be duplicated', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G$') @@ -143,7 +144,7 @@ example {n : nat} : n = n := by whatshouldIdo [`nat] at *]], function() assert.current_line.is('example {n : nat} : n = n := by simp [foo, baz] at *') end)) - it('replaces squashed suggestions from earlier in the line', helpers.clean_buffer('lean3', [[ + 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() vim.api.nvim_command('normal G0') @@ -154,7 +155,7 @@ example {n : nat} : n = n := by whatshouldIdo]], function() end)) -- Emitted by e.g. show_term - it('replaces redundant brace-delimited term and tactic mode', helpers.clean_buffer('lean3', [[ + 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") @@ -183,7 +184,7 @@ begin end]] end)) - it('handles suggestions with quotes', helpers.clean_buffer('lean3', [[ + it('handles suggestions with quotes', clean_buffer([[ meta def whatshouldIdo := (do tactic.trace "Try this: \"hi") example : true := by whatshouldIdo]], function() vim.api.nvim_command('normal G$') diff --git a/lua/tests/mappings_spec.lua b/lua/tests/mappings_spec.lua index 51313fbf..9ba2a0c7 100644 --- a/lua/tests/mappings_spec.lua +++ b/lua/tests/mappings_spec.lua @@ -4,7 +4,7 @@ local clean_buffer = require('tests.helpers').clean_buffer require('lean').setup{} describe('mappings', function() - it('are bound in the current buffer and not others', clean_buffer('lean', '', function() + it('are bound in the current buffer and not others', clean_buffer(function() lean.use_suggested_mappings(true) assert.is.same( lean.mappings.n['i'], diff --git a/lua/tests/sorry_spec.lua b/lua/tests/sorry_spec.lua index 7a5c482b..1a4bf690 100644 --- a/lua/tests/sorry_spec.lua +++ b/lua/tests/sorry_spec.lua @@ -4,10 +4,9 @@ local clean_buffer = helpers.clean_buffer require('lean').setup {} describe('sorry', function() - it('inserts sorries for each of multiple remaining goals', clean_buffer('lean', [[ + it('inserts sorries for each of multiple remaining goals', clean_buffer([[ example (p q : Prop) : p ∧ q ↔ q ∧ p := by - constructor]], - function() + constructor]], function() helpers.wait_for_line_diagnostics() vim.api.nvim_command('normal! 2gg$') @@ -19,9 +18,8 @@ example (p q : Prop) : p ∧ q ↔ q ∧ p := by · sorry]] end)) - it('inserts a sorry for the remaining goal', clean_buffer('lean', [[ -example (p : Prop) : p → p := by]], - function() + it('inserts a sorry for the remaining goal', clean_buffer([[ +example (p : Prop) : p → p := by]], function() helpers.wait_for_line_diagnostics() vim.api.nvim_command('normal! gg$') @@ -31,7 +29,7 @@ example (p : Prop) : p → p := by sorry]] end)) - it('leaves the cursor in the first sorry', clean_buffer('lean', [[ + it('leaves the cursor in the first sorry', clean_buffer([[ def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by constructor]], function() helpers.wait_for_line_diagnostics() @@ -46,7 +44,7 @@ def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by · sorry]] end)) - it('leaves the cursor in the only sorry', clean_buffer('lean', [[ + it('leaves the cursor in the only sorry', clean_buffer([[ def foo (p q : Prop) : p ∧ q → q ∧ p := by intro h]], function() helpers.wait_for_line_diagnostics() @@ -60,7 +58,7 @@ def foo (p q : Prop) : p ∧ q → q ∧ p := by bar]] end)) - it('indents sorry blocks when needed', clean_buffer('lean', [[ + it('indents sorry blocks when needed', clean_buffer([[ def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by constructor @@ -79,7 +77,7 @@ def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by ]] end)) - it('single goal within multiple goal block', clean_buffer('lean', [[ + it('single goal within multiple goal block', clean_buffer([[ def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by constructor · intro h @@ -99,7 +97,7 @@ def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by end)) - it('does nothing if there are no goals', clean_buffer('lean', [[ + it('does nothing if there are no goals', clean_buffer([[ def foo (n : Nat) : n = n := by rfl]], function() vim.api.nvim_command('normal! 2gg$') diff --git a/lua/tests/switch_spec.lua b/lua/tests/switch_spec.lua index 3d7cd9bc..fb7a03bd 100644 --- a/lua/tests/switch_spec.lua +++ b/lua/tests/switch_spec.lua @@ -1,11 +1,10 @@ -local helpers = require('tests.helpers') -local clean_buffer = helpers.clean_buffer +local clean_buffer = require('tests.helpers').clean_buffer require('lean').setup{} describe('switch', function() it('switches between left and right', - clean_buffer('lean', [[#check Nat.mul_le_mul_right]], function() + clean_buffer([[#check Nat.mul_le_mul_right]], function() vim.cmd('normal! 1gg23|') vim.cmd.Switch() assert.contents.are[[#check Nat.mul_le_mul_left]] @@ -15,7 +14,7 @@ describe('switch', function() end)) it('switches between mul and add', - clean_buffer('lean', [[#check Nat.add_one]], function() + clean_buffer([[#check Nat.add_one]], function() vim.cmd('normal! 1gg13|') vim.cmd.Switch() assert.contents.are[[#check Nat.mul_one]] @@ -25,7 +24,7 @@ describe('switch', function() end)) it('switches between zero and one', - clean_buffer('lean', [[#check Nat.mul_one]], function() + clean_buffer([[#check Nat.mul_one]], function() vim.cmd('normal! 1gg$') vim.cmd.Switch() assert.contents.are[[#check Nat.mul_zero]] @@ -35,28 +34,28 @@ describe('switch', function() end)) it('switches between exact <> and refine <>', - clean_buffer('lean', [[exact ⟨foo, bar⟩]], function() + clean_buffer([[exact ⟨foo, bar⟩]], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[refine ⟨foo, bar⟩]] end)) it('does not switch between exact foo and refine foo', - clean_buffer('lean', [[exact foo]], function() + clean_buffer([[exact foo]], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[exact foo]] end)) it('switches between simp only [foo] and simp', - clean_buffer('lean', [=[simp only [foo, bar, baz]]=], function() + clean_buffer([=[simp only [foo, bar, baz]]=], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[simp]] end)) it('switches between simp and simp?', - clean_buffer('lean', [[simp]], function() + clean_buffer([[simp]], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[[simp?]] @@ -66,7 +65,7 @@ describe('switch', function() end)) it('switches between simp [foo] and simp? [foo]', - clean_buffer('lean', [=[simp [foo, bar, baz]]=], function() + clean_buffer([=[simp [foo, bar, baz]]=], function() vim.cmd('normal! 1gg0') vim.cmd.Switch() assert.contents.are[=[simp? [foo, bar, baz]]=] diff --git a/lua/tests/trythis_spec.lua b/lua/tests/trythis_spec.lua index b5206909..c072271a 100644 --- a/lua/tests/trythis_spec.lua +++ b/lua/tests/trythis_spec.lua @@ -3,7 +3,7 @@ local helpers = require('tests.helpers') require('lean').setup {} describe('trythis', function() - it('replaces a single try this', helpers.clean_buffer('lean', [[ + it('replaces a single try this', helpers.clean_buffer([[ macro "whatshouldIdo?" : tactic => `(tactic| trace "Try this: rfl") example : 2 = 2 := by whatshouldIdo?]], function() vim.api.nvim_command('normal G$')