From 5cb855fb722fe0fe69f50628dc39b5354355b3aa Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Tue, 8 Oct 2024 15:23:13 -0400 Subject: [PATCH] Add support for GoToModuleLinks from ImportGraph. This makes #find_home and friends work interactively. I'm not thrilled with depending on import graph in the test suite, and clearly there are a few places that could be cleaned up further here. --- lua/lean/widgets.lua | 36 +++++++++++++++++++ spec/current_search_paths_spec.lua | 6 +++- spec/fixtures/example-project/foo.lean | 2 ++ .../example-project/lake-manifest.json | 30 ++++++++++++++++ spec/fixtures/example-project/lakefile.toml | 5 +++ spec/infoview/widgets_spec.lua | 32 +++++++++++++++++ 6 files changed, 110 insertions(+), 1 deletion(-) create mode 100644 spec/fixtures/example-project/foo.lean diff --git a/lua/lean/widgets.lua b/lua/lean/widgets.lua index 2b02665e..44c385ab 100644 --- a/lua/lean/widgets.lua +++ b/lua/lean/widgets.lua @@ -102,6 +102,42 @@ implement('Lean.Meta.Tactic.TryThis.tryThisWidget', function(_, props) } end) +--- @class GoToModuleLinkParams +--- @field modName string the module to jump to + +---A "jump to a module" which comes from `import-graph`. +---@param props GoToModuleLinkParams +implement('GoToModuleLink', function(_, props) + return Element:new { + text = props.modName, + events = { + go_to_def = function(_) + local this_infoview = require('lean.infoview').get_current_infoview() + local this_info = this_infoview and this_infoview.info + local this_window = this_info and this_info.last_window + if not this_window then + return + end + + vim.api.nvim_set_current_win(this_window) + -- FIXME: Clearly we need to be able to get a session without touching + -- internals... Probably this should be a method on ctx. + local sess = require('lean.rpc').open(0, this_info.pin.__position_params) + local uri, err = sess:call('getModuleUri', props.modName) + if err then + return -- FIXME: Yeah, this should go somewhere clearly. + end + ---@type lsp.Position + local start = { line = 0, character = 0 } + vim.lsp.util.jump_to_location( + { uri = uri, range = { start = start, ['end'] = start } }, + 'utf-16' + ) + end, + }, + } +end) + return { Widget = Widget, implement = implement, diff --git a/spec/current_search_paths_spec.lua b/spec/current_search_paths_spec.lua index 8c09e3f3..d0c560c7 100644 --- a/spec/current_search_paths_spec.lua +++ b/spec/current_search_paths_spec.lua @@ -10,7 +10,11 @@ describe('lean.current_search_paths', function() helpers.wait_for_ready_lsp() local paths = require('lean').current_search_paths() - assert.are.equal(3, #paths) + -- Sigh. We depend on import graph for another test, so now we can't + -- really say exactly how many paths should appear here. I guess that's + -- not too big of a loss, so eventually we can just delete this + -- assertion. + -- assert.message(vim.inspect(paths)).are.equal(3, #paths) assert.has_all(table.concat(paths, '\n') .. '\n', { '/lib/lean\n', -- standard library project.root .. '\n', -- the project itself diff --git a/spec/fixtures/example-project/foo.lean b/spec/fixtures/example-project/foo.lean new file mode 100644 index 00000000..ecb9d497 --- /dev/null +++ b/spec/fixtures/example-project/foo.lean @@ -0,0 +1,2 @@ +import ImportGraph.Imports +#find_home Nat.add_one diff --git a/spec/fixtures/example-project/lake-manifest.json b/spec/fixtures/example-project/lake-manifest.json index 5a895e02..11c5f0e4 100644 --- a/spec/fixtures/example-project/lake-manifest.json +++ b/spec/fixtures/example-project/lake-manifest.json @@ -7,6 +7,36 @@ "manifestFile": "lake-manifest.json", "inherited": false, "dir": "./foo", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fc871f7039ac6d8ab993335bb35aba43286004a0", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "", + "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, "configFile": "lakefile.toml"}], "name": "test", "lakeDir": ".lake"} diff --git a/spec/fixtures/example-project/lakefile.toml b/spec/fixtures/example-project/lakefile.toml index 06024701..f0e008f6 100644 --- a/spec/fixtures/example-project/lakefile.toml +++ b/spec/fixtures/example-project/lakefile.toml @@ -5,5 +5,10 @@ defaultTargets = ["Test"] name = "foo" path = "foo" +[[require]] +name = "importGraph" +git = "https://github.com/leanprover-community/import-graph" +rev = "main" + [[lean_lib]] name = "Test" diff --git a/spec/infoview/widgets_spec.lua b/spec/infoview/widgets_spec.lua index d08f797e..f9775c3d 100644 --- a/spec/infoview/widgets_spec.lua +++ b/spec/infoview/widgets_spec.lua @@ -4,6 +4,7 @@ local Element = require('lean.tui').Element local helpers = require 'spec.helpers' +local infoview = require 'lean.infoview' local widgets = require 'lean.widgets' require('lean').setup {} @@ -107,4 +108,35 @@ describe('widgets', function() end ) ) + + it( + 'supports import-graph GoToModule links', + helpers.clean_buffer( + [[ + import ImportGraph.Imports + #find_home Nat.add_one + ]], + function() + local lean_window = vim.api.nvim_get_current_win() + local initial_path = vim.api.nvim_buf_get_name(vim.api.nvim_get_current_buf()) + + helpers.move_cursor { to = { 2, 2 } } + assert.infoview_contents.are [[ + ▶ 2:1-2:11: information: + [Init.Prelude] + ]] + + infoview.go_to() + helpers.move_cursor { to = { 2, 2 } } + helpers.feed 'gd' + + assert.is_truthy(vim.wait(15000, function() + return vim.api.nvim_buf_get_name(0) ~= initial_path + end)) + + local path = vim.api.nvim_buf_get_name(vim.api.nvim_win_get_buf(lean_window)) + assert.is_truthy(path:match 'Init/Prelude.lean') + end + ) + ) end)