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

@@ -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,

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

spec/fixtures/example-project/foo.lean

@@ -0,0 +1,2 @@
+import ImportGraph.Imports
+#find_home Nat.add_one

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"}

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"

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)