User defined LSP extensions

Stream: lean4

[Patrick Massot]

@Marc Huisinga @Wojciech Nawrocki is there anyway to experiment adding LSP requests from user code? Is there any plan to add requests asking for the range of the current declaration or current section or current tactic? Or do they already exist? The closest thing I could find in the LSP spec is https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_selectionRange that doesn’t seem to be implemented in the Lean server (and doesn’t seem to allow labels to the returned ranges, so I don’t know how we would distinguish declarations from tactics for instance).

[Julian Berman]

This would be very useful for implementing text objects in editors for editing declarations (I think there's a previous thread where this was briefly discussed).

[Patrick Massot]

Yes, that's why I'm asking. Because I saw you seemed to be in a lean.nvim mood and I'd like to help.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yes, this is possible. The best worked example I know is Mac's Alloy: https://github.com/tydeu/lean4-alloy/blob/master/Alloy/C/Server.lean

[Patrick Massot]

Nice, I’ll take a look.

[Patrick Massot]

I didn’t manage to cargo-cult this. I tried

open Lean Server Lsp RequestM JsonRpc

structure CurDeclParams extends TextDocumentPositionParams
  deriving FromJson, ToJson

instance : FileSource CurDeclParams :=
  ⟨fun p => fileSource p.textDocument⟩

def handleCurDecl (p : CurDeclParams) :
    RequestM (RequestTask String) := do
  return (.pure "Yo")

initialize
  registerLspRequestHandler "textDocument/curDecl" CurDeclParams String handleCurDecl

in a file imported by a file where I send a textDocument/curDecl request, but the only answer I get from the server is Error: No request handler found for 'textDocument/curDecl' (-32601) (note that I’m able to request a definition in that file for instance).

[Julian Berman]

It doesn't work for me either and I'm not sure why, so just +1ing -- but a minor LSP note is that we shouldn't put non-"standard" requests on textDocument/ -- the convention in the Lean server is to use methods that are named like $/lean/currentDecl -- but yeah trying that locally doesn't change anything, and I barely know enough to even debug whether Lean.Server.Lsp.requestHandlers ends up actually containing the method added.

[Julian Berman]

(I'm sure you were messing around anyhow, just mentioning.)

[Patrick Massot]

The only way I know the handler is kind of registered is that if I try to register it twice then Lean complains the second time.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Patrick Massot what happens if you put that snippet in one module and then make the request in another module that imports the first one?

[Patrick Massot]

What do you mean by “make the request”? Do you mean from within Lean or through connection to the LSP server?

[Patrick Massot]

I don’t know how to do it from Lean.

[Patrick Massot]

Through the server I get the error message I posted above: No request handler found for 'textDocument/curDecl'

[Patrick Massot]

I will describe the way I’m testing this since it could create issues because I don’t know what I’m doing.

[Patrick Massot]

I googled to find a python lib to write LSP clients since hacking something with python is still the fastest way for me to test anything that is not purely within Lean.

[Patrick Massot]

I found https://github.com/microsoft/multilspy/

[Patrick Massot]

And I wrote https://gist.github.com/PatrickMassot/bc647630058d27ff38105b4157d110ef on top of it. This is 99% copy-paste from https://github.com/microsoft/multilspy/blob/main/src/multilspy/language_servers/jedi_language_server/jedi_server.py

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh, I thought you had a way to make custom requests from within nvim or another editor

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

What I was trying to suggest with my message is just that initialize blocks behave differently when imported, and you might need the intialize block to be in a different module than the one you are making the request on/to

[Patrick Massot]

The above gist, together with https://github.com/microsoft/multilspy/blob/main/src/multilspy/language_servers/jedi_language_server/initialize_params.json also taken from the jedi example is enough for me to require the definition of the token at a given position in a file.

[Patrick Massot]

Sure, the initialize is in a different Lean file.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ah, you even wrote that :man_facepalming:

[Patrick Massot]

That being said, I don’t insist on using python, this is only a prototyping thing.

[Patrick Massot]

If you know a way to test a new LSP request from within Lean then it works for me.

[Patrick Massot]

I was simply trying to separate the issue of learning Lua and registering a new LSP request.

[Patrick Massot]

My next plan is to hack on Lean itself to add more debug information than what is provided in https://github.com/leanprover/lean4/blob/master/src/Lean/Server/Requests.lean#L61

[Patrick Massot]

Actually I don’t know how to do this. I cloned the lean4 repo, then followed the instructions at https://lean-lang.org/lean4/doc/make/index.html and then typed elan toolchain link lean4-stage0 build/release/stage0 and created a Lean project using lake +lean4-stage0 new tmp but then lake build in the tmp folder says

error: ././lakefile.lean:2:5: error: unknown namespace 'Lake'
error: ././lakefile.lean:4:0: error: unexpected identifier; expected command
error: ././lakefile.lean:10:17: error: unexpected identifier; expected 'abbrev', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean: package configuration has errors

[Julian Berman]

Patrick I'm not at a comp but the way you make lsp requests in neovim is e.g. :lua vim.print(vim.lsp.get_active_clients()[1].request_sync('textDocument/curDecl', { foo = 37 })) which you run from within the buffer of a .lean file.

[Julian Berman]

The second arg is your params

[Julian Berman]

(also be aware I think there's a minor Lean bug that the server will crash if you send it nil (i.e. leave off the second arg) so if it seems like stuff is blowing up that's a reason why)

[Julian Berman]

But otherwise this is what I tried earlier and got the same message you did.

[Julian Berman]

OK and now that I'm back to a computer, I have something "working" if I hack it into the server

[Julian Berman]

Specifically

diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 9e5c7f42dd..2a09a363f2 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -229,6 +229,10 @@ def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
         locationLinksOfInfo kind infoWithCtx snap.infoTree
       else return #[]

+def handleCurrentDecl (p : TextDocumentPositionParams) :
+    RequestM (RequestTask String) := do
+      return (.pure "Yo")
+
 open RequestM in
 def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Widget.InteractiveGoals)) := do
   let doc ← readDoc
@@ -753,5 +757,10 @@ builtin_initialize
     PlainTermGoalParams
     (Option PlainTermGoal)
     handlePlainTermGoal
+  registerLspRequestHandler
+    "$/lean/currentDecl"
+    TextDocumentPositionParams
+    String
+    handleCurrentDecl

then building lean (in my case HEAD does not seem to build because of some UInt issues? But using 4.11.0-rc2 does)

and then :lua vim.print(vim.lsp.get_active_clients()[1].request_sync('$/lean/currentDecl', vim.lsp.util.make_position_params()))

gives me

{
  result = "Yo"
}

[Patrick Massot]

How did you manage to make a project using your custom Lean build?

[Henrik Böving]

Patrick Massot said:

How did you manage to make a project using your custom Lean build?

If you registered your local build as a toolchain with elan you can just put it into a lean-toolchain file and work with it

[Matthew Ballard]

Or you can use elan override set my_custom_toolchain and not touch lean-toolchain

[Patrick Massot]

Do you see any mistake in my description at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/User.20defined.20LSP.20extensions/near/462165051?

[Patrick Massot]

Should I also have a stage1 somehow?

[Patrick Massot]

Ah yes, it seems I need to link stage1

[Henrik Böving]

https://lean-lang.org/lean4/doc/dev/index.html#dev-setup-using-elan

# in the Lean rootdir
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

[Patrick Massot]

I think I misread an old zulip message earlier. I can now use my custom toolchain. Thanks Henrik and Matthew!

[Patrick Massot]

I managed to get some extra info in the error message, but it is only telling me that, at the time the LSP request is processed, Lean indeed doesn’t know my handler. But it doesn’t tell me whether it forgot about it or didn’t come across it.

[Patrick Massot]

Does anyone underdstand how alloy manages to convince Lean that its extra handlers are worth using?

[Patrick Massot]

And indeed I can reproduce Julian’s success with adding the request handler inside the lean4 code base. At least I’ll be able to play with trying to make those request actually return something useful. It’s even semi-quick because the server file we are editing is so high in the build tree that compiling lean after modifying it is pretty fast.

[Julian Berman]

Patrick Massot said:

How did you manage to make a project using your custom Lean build?

(I just did PATH=$PWD/stage1/bin:$PATH and started nvim in my case)

[Julian Berman]

Patrick Massot said:

Does anyone underdstand how alloy manages to convince Lean that its extra handlers are worth using?

I think maybe someone should confirm alloy actually works just to be sure

[Julian Berman]

I didn't yet. But glad you have something temporarily useful

[Henrik Böving]

Julian Berman said:

Patrick Massot said:

Does anyone underdstand how alloy manages to convince Lean that its extra handlers are worth using?

I think maybe someone should confirm alloy actually works just to be sure

It does

[Patrick Massot]

New information from the FRO office hour: it looks like one cannot add a LSP request type from user space. What Alloy is doing is chaining request handlers that do their work after a builtin handler.

[Julian Berman]

Was there by any chance any alternative proposed (either a future ability to do this, or else any interest in the language server growing this capability)?

[Patrick Massot]

Yes, there is some hope. But we won't know for sure until Marc comes back from vacation since he is in charge of that corner of Lean.

[Patrick Massot]

Julian Berman said:

Patrick I'm not at a comp but the way you make lsp requests in neovim is e.g. :lua vim.print(vim.lsp.get_active_clients()[1].request_sync('textDocument/curDecl', { foo = 37 })) which you run from within the buffer of a .lean file.

I was not able to get this to return anything. Can you get anything if you put in your Lean4 file that we were tweaking:

def handleCurrentDecl (p : TextDocumentPositionParams) :
    RequestM (RequestTask <| Option Range) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos)
    (notFoundX := pure none) fun snap => do
  let some rg := snap.stx.getRange? | return none
  return some <| rg.toLspRange text

builtin_initialize
  registerLspRequestHandler
    "$/lean/currentDecl"
    TextDocumentPositionParams
    (Option Range)
    handleCurrentDecl

[Patrick Massot]

I try to call it replacing your {foo = 37} with { textDocument = { uri = "file:///home/pmassot/lean/tmp/Tmp/Basic.lean" }, position = { line = 0, character = 17 } } where the file Tmp/Basic.lean indeed exists and my python code gets an answer. But vim always report an empty result.

[Patrick Massot]

@Julian Berman any idea here?

[Julian Berman]

Sorry, missed that -- yes @Patrick Massot I do get something here, if I try it on some file with def foo := 12 I get the expected response:

{
  result = {
    ["end"] = {
      character = 13,
      line = 0
    },
    start = {
      character = 0,
      line = 0
    }
  }
}

[Julian Berman]

You tried using vim.lsp.util.make_position_params() as the parameter instead of manually passing them just to be sure of no typos? Even though I don't see any there presuming that's the file path and it's at least 17 chars long...

[Julian Berman]

Oh, also use :LspInfo in your lean file and check that for you it says something similar to what it says for me, namely that my Lean is... cmd: /Users/julian/Development/lean4/build/release/stage1/bin/lake serve -- /Users/julian/Development/lean4 /Users/julian/Development/lean4/src and not that you're talking to the non-custom Lean

[Patrick Massot]

:LspInfo says it called elan, but I know elan its doing its job, otherwise lean would complain about an unknown request.

[Patrick Massot]

Oh, today it works!

[Patrick Massot]

I really don’t understand what happened the other day.

[Patrick Massot]

I am still interested in learning more about your mysterious hint: “using vim.lsp.util.make_position_params() as the parameter instead of manually passing them just to be sure of no typos”. I don’t know how to do that.

[Patrick Massot]

I tried :lua vim.lsp.util.make_position_params() but I get a mysterious table: 0x733ce1788760.

[Patrick Massot]

I would be really nice to call a lsp request with the current cursor position as argument.

[Julian Berman]

Do :lua vim.print(vim.lsp.util.make_position_params())

[Julian Berman]

You are spoiled Patrick

[Julian Berman]

Lua is a silly little language

[Julian Berman]

It does not know how to print its own tables (dictionaries)

[Julian Berman]

So unlike in Python when you print {"foo": 12, "bar": 37} you see what you expect to see

[Julian Berman]

In Lua you see nothing but that memory address, it has no way of printing that table, and you get to write it yourself if you wish by writing for k, v in pairs(yourtable) print(k, v) end and handling all the recursive cases, and etc. -- but neovim has a version of that function which does work to print anything, it's vim.print.

[Julian Berman]

So vim.lsp.util.make_position_params() is indeed a function which builds exactly those TextDocumentPositionParams that you wrote by hand, but it does it automatically using the current cursor position, as you want.

[Julian Berman]

(So even more explicitly, you can write :lua vim.print(vim.lsp.get_active_clients()[1].request_sync('$/lean/currentDecl', vim.lsp.util.make_position_params())))

[Patrick Massot]

This memory address thing is what I suspected. Thanks.

[Patrick Massot]

I'm away from my computer but I will try later.

[Patrick Massot]

@Julian Berman I wasn’t able to use your trick because I don’t know how to merge two tables in Lua (and internet seems to say there is no library function doing that)! I mean doing what the python dictionary update method does.

[Patrick Massot]

But anyway, I went back to this tonight, and I think I’ve reached a stage where I’ll need your help.

[Patrick Massot]

Here is how you can play. In your copy of Lean 4, in https://github.com/leanprover/lean4/blob/master/src/Lean/Server/FileWorker/RequestHandling.lean, right before the registrations at the end, paste:

structure TextDocumentCustomQueryAtParams extends TextDocumentPositionParams where
  /-- The kind of elements we are looking for. -/
  kind : String
  deriving ToJson, FromJson

instance : FileSource TextDocumentCustomQueryAtParams := ⟨fun p ↦ fileSource p.textDocument⟩

/-- Placeholder for requesting some LSP range at the current cursor position.
This placeholder will always return `none`. It is expected to be
chained by some user-defined handler.
-/
def handleQueryRangeAt (_p : TextDocumentCustomQueryAtParams) :
    RequestM (RequestTask <| Option Range) := do
  return .pure none

/-- Placeholder for requesting some LSP position at the current cursor position.
This placeholder will always return `none`. It is expected to be
chained by some user-defined handler.
-/
def handleQueryPositionAt (_p : TextDocumentCustomQueryAtParams) :
    RequestM (RequestTask <| Option Lsp.Position) := do
  return .pure none

/-- Placeholder for requesting some string at the current cursor position.
This placeholder will always return `none`. It is expected to be
chained by some user-defined handler.
-/
def handleQueryStringAt (_p : TextDocumentCustomQueryAtParams) :
    RequestM (RequestTask <| Option String) := do
  return .pure none

and then start the builtin_initialize block at the end with

builtin_initialize
  registerLspRequestHandler
    "$/lean/rangeAt"
    TextDocumentCustomQueryAtParams
    (Option Range)
    handleQueryRangeAt
  registerLspRequestHandler
    "$/lean/positionAt"
    TextDocumentCustomQueryAtParams
    (Option Lsp.Position)
    handleQueryPositionAt
  registerLspRequestHandler
    "$/lean/stringAt"
    TextDocumentCustomQueryAtParams
    (Option String)
    handleQueryStringAt

[Patrick Massot]

This creates three place-holders custom LSP requests. They each take a position (that should be the cursor position) and a string which is meant to indicate what kind of element we are requesting. Then the server should return an optional range, position or string (the string case is mostly meant for debugging).

[Patrick Massot]

Now the nice thing is that you only need to compile Lean once. Then you’ll be able to implement handlers in user space.

[Patrick Massot]

For instance, you can start a new Lean project using our custom toolchain and have a file there containing:

import Lean

open Lean Server Lsp FileWorker RequestM

/-- Is this the `SyntaxNodeKind` of a tactic syntax? Currently a very crude heuristic. -/
def Lean.SyntaxNodeKind.isTactic (kind : SyntaxNodeKind) : Bool :=
  Name.isPrefixOf `Lean.Parser.Tactic kind

/-- In the given syntax stack, find the first item satisfying the condition `cond`
and run `code` on it. Return `none` if no such item exists.  -/
def Lean.Syntax.Stack.find? (stack : Syntax.Stack) (cond : Lean.Syntax → Bool) {m : Type → Type} [Monad m] {α : Type}
    (code : Lean.Syntax → m (Option α)) : m (Option α) := do
  for (stx, _) in stack do
    if cond stx then
      return ← code stx
  return none

/-- In the given syntax stack, find the first item satisfying the condition `cond`
and return its LSP range (using the given `FileMap`). Return `none` if no such item exists.  -/
def Lean.Syntax.Stack.findRange? (stack : Syntax.Stack) (cond : Lean.Syntax → Bool)
    {m : Type → Type} [Monad m] (map : FileMap) : m (Option Lsp.Range) :=
  stack.find? cond fun stx ↦ return stx.getRange?.map fun rg ↦ rg.toLspRange map

def handleRangeAt  (p : TextDocumentCustomQueryAtParams) (_prev : RequestTask (Option Range)):
    RequestM (RequestTask <| Option Range) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos) (notFoundX := pure none) fun snap => do
  let some stack := snap.stx.findStack? (·.getRange?.any (·.contains hoverPos)) | return none
  match p.kind with
  | "declaration" =>
    stack.findRange? (·.getKind = `Lean.Parser.Command.declaration) text
  | "tactic" =>
    stack.findRange? (·.getKind.isTactic) text
  | "tacticSeq"  =>
    stack.findRange? (·.getKind = `Lean.Parser.Tactic.tacticSeq) text
  | "binder" =>
    stack.findRange? (·.getKind ∈ [`Lean.Parser.Term.explicitBinder,`Lean.Parser.Term.implicitBinder]) text
  | _ => return none


deriving instance Repr for Lsp.Position
deriving instance Repr for Lsp.Range

def handleStringAt  (p : TextDocumentCustomQueryAtParams) (_prev : RequestTask (Option String)):
    RequestM (RequestTask <| Option String) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos) (notFoundX := pure none) fun snap => do
  if p.kind == "printStack" then
    let some stack := snap.stx.findStack? (·.getRange?.any (·.contains hoverPos)) | return none
    let mut res := ""
    for (stx, _) in stack do
      let some rg := stx.getRange? | continue
      res := s!"{res}\n\n{stx.getKind}\n{stx}\n{repr <| rg.toLspRange text}"
    return some res
  else
    return none

initialize
  chainLspRequestHandler "$/lean/rangeAt"
    TextDocumentCustomQueryAtParams (Option Range) handleRangeAt

initialize
  chainLspRequestHandler "$/lean/stringAt"
    TextDocumentCustomQueryAtParams (Option String) handleStringAt

[Julian Berman]

vim.tbl_extend is the functional versión of update -- it takes some funny options -- you use it like vim.tbl_extend('keep', t1, t2) where the keep option (which can also be 2 other values) means keep the value from t1 when there are dupes -- and it returns the merged table.
I'm away from a computer now but you've obviously got my help, so will look at your instructions later tonight my time.

[Patrick Massot]

Nice, it works! So you can call for instance lua vim.print(vim.lsp.get_active_clients()[1].request_sync('$/lean/rangeAt', vim.tbl_extend('keep',vim.lsp.util.make_position_params(), { kind = "tactic"})).result) to get the range of the current tactic syntax. Replace "tactic" with "declaration" to get the current declaration (I mean the declaration surrounding the cursor) or "tacticSeq" to get the current tactic sequence.

[Patrick Massot]

The next step needs you. I’d like to learn how to extend the lean.nvim extension to take this information and make it into a text object etc.

[Patrick Massot]

Note the above Lean code is really a proof of concept, it is not meant to be robust and complete.

[Patrick Massot]

I was starting to refine my proof of concept code from yesterday. My idea was to replace my three placeholders requests and my match on the kind parameter by a single custom LSP request taking arbitrary Json as input and outputting arbitrary json, with proper environment extension and attribute to register handlers. But as I started to think about the implementation, which means thinking about where I could see similar functionality to copy-paste code, I realized I may be reinventing the server_rpc_method attribute and surrounding framework. @Wojciech Nawrocki, is that correct? Could I simply user this existing framework and have lean.nvim directly calling the LSP request $/lean/rpc/call? @Julian Berman what do you think about this? Could you expose a Lua function that takes arbitrary Json input, add the RPC session id and call $/lean/rpc/call?

[Julian Berman]

I was just starting to work out similar questions myself to try to help on the next step.

[Julian Berman]

More specifically, lean.nvim's RPC code lives in lua/lean/rpc.lua.

[Julian Berman]

So yeah I am trying to recall whether your new handlers should be methods on what we call Subsession, which I think possibly yes.

[Julian Berman]

Here for instance is how we implemet goToLocation: https://github.com/Julian/lean.nvim/blob/7bb86aefab286c66c7f30f6ab51e7f235eea269b/lua/lean/rpc.lua#L363-L369

So I think your method will be similar to that (but yeah it's been <10 minutes since I happen to just start looking at this finally)

[Julian Berman]

Could you expose a Lua function that takes arbitrary Json input, add the RPC session id and call $/lean/rpc/call?

(So even more explicitly, this function exists, it's called session:call{yourstuff}!)

[Patrick Massot]

How would you call that session:call from the vim command mode?

[Julian Berman]

E.g. in a Lean buffer:

:lua local params = vim.lsp.util.make_position_params(); local sess = require'lean.rpc'.open(0, params); require'plenary.async'.void(function() vim.print(sess:call('Lean.Widget.getInteractiveTermGoal', params)) end)()

and then look at what you see in :messages for the printed response.

[Julian Berman]

(The async nonsense is some synchronous wrapping, I forget if we have a helper to do that more nicely) -- does that help at all as-is?

[Julian Berman]

I don't know anything about the Lean side of the framework (how you register new RPC calls) -- maybe you do. I'm trying to teach myself that now.

[Julian Berman]

Ah, it's registerRpcProcedure.

[Patrick Massot]

There is an attribute to register rpc methods.

[Patrick Massot]

It’s dinner time here, but I’ll try later.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Patrick Massot it would help to know what you are trying to achieve in the end, but yes, since it looks like custom LSP endpoints are not possible to register after all, using @[server_rpc_method] is another way of achieving the same effect. The one downside is that you need to have an RPC session running, but lean.nvim seems to have one already for some of its widget support.

[Patrick Massot]

I explained in this thread what I’m trying to do. One single example is to make a LSP request querying the range of the current declaration.

[Patrick Massot]

I am not able to make it work with rpc_method yet. I have

structure Params extends Lean.Lsp.TextDocumentPositionParams where
  /-- The kind of elements we are looking for. -/
  kind : String
  deriving ToJson, FromJson

@[server_rpc_method]
def rpcTest  (_p : Params) :
    RequestM (RequestTask String) := do
  return .pure "Test"

but then using Julian’s magic code lua local params = vim.tbl_extend('keep',vim.lsp.util.make_position_params(), { kind = "tacticSeq"}); local sess = require'lean.rpc'.open(0, params); require'plenary.async'.void(function() vim.print(sess:call('rpcTest', params)) end)() only returns nil.

[Julian Berman]

It I think will always return nil because of the async.void -- but it should print something (unless you mean it doesn't do that either) -- let me try your lines now.

[Patrick Massot]

I think it prints nil.

[Julian Berman]

It was not working, and now it's working here.

[Julian Berman]

This works for me: lua local params = vim.lsp.util.make_position_params(); local sess = require'lean.rpc'.open(0, params); require'plenary.async'.void(function() vim.notify(sess:call('rpcTest', vim.tbl_extend('keep', params, { kind = 'range' }))) end)()

[Julian Berman]

(I changed to vim.notify because it's more convenient for me than vim.print, I have vim.notify show me a popup with the message -- but that part doesn't matter) -- that line shows me Test

[Julian Berman]

Here is a full repository in case that's useful, I'm sure you already have one but just to see what I am running myself: https://github.com/Julian/lspfun -- I am just using one of your MIL files to test and the lines you showed here

[Patrick Massot]

Ok, this one works!

[Patrick Massot]

Now I really need to learn how to define function to compress that. Editing this line forever in command mode won’t be fun.

[Patrick Massot]

What you I read to avoid asking you help at every step?

[Patrick Massot]

Should I search for a neovim extension writing tutorial?

[Julian Berman]

Yeah so I really need to write you out some longer instructions, but let me write you something to get you started -- first step, get lean.nvim in "develop" mode so that you can clone the plugin and make changes to it and see those live. This is functionality that lazy.nvim gives you, you just need to tell it where you store your repositories. One second, I'll write up how to do that.

[Julian Berman]

These are the key lines: https://github.com/Julian/dotfiles/blob/main/.config/nvim/init.lua#L33-L37 -- in particular in my case I am telling lazy.nvim "when you see a plugin called Julian/<something>, go look at $DEVELOPMENT/something -- if that exists, load the plugin from there -- otherwise, load it from GitHub" -- and my $DEVELOPMENT environment variable is set to where I keep my git repositories. Add that to where you start lazy, and then either clone or fork + clone the repository into that location.

[Julian Berman]

Once you have that, go to lua/lean/rpc.lua in that repo and add print("HELLO") somewhere, and open a Lean file, and you should see neovim print HELLO to :messages.

[Julian Berman]

At this point you can now simply copy paste what you see in that file to add more methods to the session object.

[Julian Berman]

(I will want to write you up some instructions on how to run tests because that is useful instead of manually testing stuff, but it may have to wait until tomorrow).

[Patrick Massot]

Do you manage to get any output with the actually useful function

@[server_rpc_method]
def rpcRangeAt  (p : Params) :
    RequestM (RequestTask <| Option Range) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos) (notFoundX := pure none) fun snap => do
  let some stack := snap.stx.findStack? (·.getRange?.any (·.contains hoverPos)) | return none
  match p.kind with
  | "declaration" =>
    stack.findRange? (·.getKind = `Lean.Parser.Command.declaration) text
  | "tactic" =>
    stack.findRange? (·.getKind.isTactic) text
  | "tacticSeq"  =>
    stack.findRange? (·.getKind = `Lean.Parser.Tactic.tacticSeq) text
  | "binder" =>
    stack.findRange? (·.getKind ∈ [`Lean.Parser.Term.explicitBinder,`Lean.Parser.Term.implicitBinder]) text
  | _ => return none

I get a lua error message when I try to call it.

[Patrick Massot]

I try it with lua local params = vim.lsp.util.make_position_params(); local sess = require'lean.rpc'.open(0, params); require'plenary.async'.void(function() vim.notify(sess:call('rpcRangeAt', vim.tbl_extend('keep', params, { kind = 'tacticSeq' }))) end)()

[Julian Berman]

Can you tell me the imports

[Julian Berman]

Lean is confused about findRange?

[Patrick Massot]

Sorry about that.

import Lean

open Lean Server Lsp FileWorker RequestM

[Julian Berman]

Weird, that's the same imports as I had, but Lean still seems confused... one second.

[Patrick Massot]

/-- Is this the `SyntaxNodeKind` of a tactic syntax? Currently a very crude heuristic. -/
def Lean.SyntaxNodeKind.isTactic (kind : SyntaxNodeKind) : Bool :=
  Name.isPrefixOf `Lean.Parser.Tactic kind

/-- In the given syntax stack, find the first item satisfying the condition `cond`
and run `code` on it. Return `none` if no such item exists.  -/
def Lean.Syntax.Stack.find? (stack : Syntax.Stack) (cond : Lean.Syntax → Bool) {m : Type → Type} [Monad m] {α : Type}
    (code : Lean.Syntax → m (Option α)) : m (Option α) := do
  for (stx, _) in stack do
    if cond stx then
      return ← code stx
  return none

/-- In the given syntax stack, find the first item satisfying the condition `cond`
and return its LSP range (using the given `FileMap`). Return `none` if no such item exists.  -/
def Lean.Syntax.Stack.findRange? (stack : Syntax.Stack) (cond : Lean.Syntax → Bool)
    {m : Type → Type} [Monad m] (map : FileMap) : m (Option Lsp.Range) :=
  stack.find? cond fun stx ↦ return stx.getRange?.map fun rg ↦ rg.toLspRange map

[Patrick Massot]

Sorry, I thought you had the file I pasted yesterday.

[Julian Berman]

Ahh ok, yes sorry I just deleted it and replaced it all with the rpc thing but that clearly was deleting too much. OK let's see...

[Julian Berman]

(I see the error, trying to figure out where it's coming from.)

[Patrick Massot]

Julian Berman said:

These are the key lines: https://github.com/Julian/dotfiles/blob/main/.config/nvim/init.lua#L33-L37 -- in particular in my case I am telling lazy.nvim "when you see a plugin called Julian/<something>, go look at $DEVELOPMENT/something -- if that exists, load the plugin from there -- otherwise, load it from GitHub" -- and my $DEVELOPMENT environment variable is set to where I keep my git repositories. Add that to where you start lazy, and then either clone or fork + clone the repository into that location.

I was not able to make anything out of this, but I did the low-tech replacement of Julian/lean.nvim by dir=… and I can load my version.

[Patrick Massot]

I wrote in my hacked lean.nvim

function LeanRpc(method, extras)
    local params = vim.lsp.util.make_position_params();
    local sess = require'lean.rpc'.open(0, params);
    require'plenary.async'.void(function() vim.notify(sess:call(method, vim.tbl_extend('keep', params, extras))) end)()
  end

which is already useful, but of course it doesn’t get rid of the error message.

[Julian Berman]

Nor here yet, so I'm missing something obvious.

[Patrick Massot]

I think this error message is simply hiding any LSP error. Trying to call a non-existent rpc method gives exactly the same message.

[Julian Berman]

OK and now it works again after doing random stuff to clean up the code.

[Julian Berman]

It's really so unfun dealing with languages with nil and craziness.

[Julian Berman]

This is what I ended up with:

local bufnrs = vim.iter(vim.api.nvim_tabpage_list_wins(0))
  :map(function(win)
    local bufnr = vim.api.nvim_win_get_buf(win)
    if vim.bo[bufnr].filetype == 'lean' then
      return win, bufnr
    end
  end):totable()

local win, bufnr = unpack(bufnrs[1])

local pos = vim.lsp.util.make_position_params(win)
local sess = require'lean.rpc'.open(bufnr, pos)


require'plenary.async'.void(function()
  local params = vim.tbl_extend('keep', pos, { kind = 'declaration' })
  local result = sess:call('rpcRangeAt', params)
  vim.print(result)
end)()

I put this in some random foo.lua file in my case and then was running :source foo.lua over and over again to test -- because I thought it would be easier in case you didn't get lean.nvim editable -- but if you did you can just paste it wherever you want.

[Patrick Massot]

I’ll try this, but let me report that

@[server_rpc_method]
def rpcTestBis  (p : Params) :
    RequestM (RequestTask $ Option String) := do
  return .pure none

fails while

@[server_rpc_method]
def rpcTestBis  (p : Params) :
    RequestM (RequestTask $ Option String) := do
  return .pure (some "TestBis")

works.

[Julian Berman]

(You're right that something is simply hiding errors)

[Julian Berman]

Ahhhhh

[Julian Berman]

That's silly.

[Julian Berman]

The issue is that vim.notify takes a string, and we were passing it a table once you returned a table from your RPC method

[Julian Berman]

Use vim.notify(vim.inspect(result)) -- vim.inspect is like repr().

[Julian Berman]

(This fixes what you just sent as well -- it's all just the silly printing mistake.)

[Patrick Massot]

Great!

[Patrick Massot]

So I can stick with

function LeanRpc(method, extras)
    local params = vim.lsp.util.make_position_params();
    local sess = require'lean.rpc'.open(0, params);
    require'plenary.async'.void(function() vim.notify(vim.inspect(sess:call(method, vim.tbl_extend('keep', params, extras)))) end)()
  end

right?

[Patrick Massot]

Now we are back on track. We don’t even need a custom Lean toolchain. It turns out the existing extensibility through RPC method is enough for us.

[Julian Berman]

Yep that looks ok -- just beware that when you say 0 there you are referring to the current buffer (and same if you pass no argument to make_position_params), so you always need to run that from the Lean buffer. If you get tired of that you can use that 4 lines of filter code in my code block to "find any window that's open that's a lean buffer and run this in there".

[Julian Berman]

Yes, this is a very good find, and clearly I should have remembered we already had this before.

[Patrick Massot]

Oh, the vim.notify(vim.inspect( prints strings with \n instead of printing new lines. That’s a bit painful.

[Julian Berman]

vim.notify(type(result) == "string" and result or vim.inspect(result)) perhaps

[Patrick Massot]

This is not very robust but good enough for now, thanks!

[Patrick Massot]

Now I guess I’m back to learning how to make new text objects and motions.

[Julian Berman]

You can also go back to vim.print, it's whatever is least painful really.

[Julian Berman]

Patrick Massot said:

Now I guess I’m back to learning how to make new text objects and motions.

Here is an article on how to create text objects -- https://thevaluable.dev/vim-create-text-objects/ -- but it's both super long winded and a bit out of date it seems, you should do it with vim.keymap.set({'x', 'o'}, 'D -- or whatever letter you want to put it on', function() something end, {buffer = true}))

[Julian Berman]

I would actually possibly start by implementing ]m and [m -- this is an (existing) mapping which is supposed to move you to the start of methods/functions/whatever -- so you could start by taking your "find me where the declaration ends" and then use that to reimplement ]m properly for Lean

[Julian Berman]

That would be a normal mode mapping, rather than an operator pending one (i.e. a text object)

[Julian Berman]

Implementing ]t (that doesn't exist but we could invent) for "move me to the next tactic" would be similar and obviously super useful.

[Julian Berman]

Both of those will end up calling vim.api.nvim_win_set_cursor -- that's the function that lets you move the cursor to some arbitrary position (i.e. the one you get back from the lean server!)

[Patrick Massot]

Thanks! I need to sleep, so that will be for another day. Before going to sleep, I made sure to reimplement all my tests in the new style. The new full Lean file is:

import Lean

open Lean Server Lsp FileWorker RequestM

/-- Is this the `SyntaxNodeKind` of a tactic syntax? Currently a very crude heuristic. -/
def Lean.SyntaxNodeKind.isTactic (kind : SyntaxNodeKind) : Bool :=
  Name.isPrefixOf `Lean.Parser.Tactic kind

/-- In the given syntax stack, find the first item satisfying the condition `cond`
and run `code` on it. Return `none` if no such item exists.  -/
def Lean.Syntax.Stack.find? (stack : Syntax.Stack) (cond : Lean.Syntax → Bool) {m : Type → Type} [Monad m] {α : Type}
    (code : Lean.Syntax → m (Option α)) : m (Option α) := do
  for (stx, _) in stack do
    if cond stx then
      return ← code stx
  return none

def mkRpcAtMethod {α : Type} [RpcEncodable α] [Inhabited α]
    (cond : Lean.Syntax → Bool) (body : Syntax → (map : FileMap) → Option α) (params : TextDocumentPositionParams) :
    RequestM (RequestTask <| Option α) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos params.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos) (notFoundX := pure none) fun snap => do
  let some stack := snap.stx.findStack? (·.getRange?.any (·.contains hoverPos)) | return none
  stack.find? cond fun stx ↦ return body stx text


def mkRpcRangeAtMethod (cond : Lean.Syntax → Bool) :=
    mkRpcAtMethod cond fun stx map ↦ return stx.getRange?.map fun rg ↦ rg.toLspRange map

@[server_rpc_method]
def rpcDeclarationRangeAt := mkRpcRangeAtMethod (·.getKind = `Lean.Parser.Command.declaration)

@[server_rpc_method]
def rpcTacticRangeAt := mkRpcRangeAtMethod (·.getKind.isTactic)

@[server_rpc_method]
def rpcTacticSeqRangeAt := mkRpcRangeAtMethod (·.getKind = `Lean.Parser.Tactic.tacticSeq)


@[server_rpc_method]
def rpcBinderRangeAt :=
  mkRpcAtMethod (·.getKind ∈ [`Lean.Parser.Term.explicitBinder,`Lean.Parser.Term.implicitBinder]) fun stx map ↦ return stx.getRange?.map fun rg ↦ (stx.getKind, rg.toLspRange map)


deriving instance Repr for Lsp.Position
deriving instance Repr for Lsp.Range

@[server_rpc_method]
def syntaxStack  (p : TextDocumentPositionParams ) :
    RequestM (RequestTask <| Option String) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos) (notFoundX := pure none) fun snap => do
  let some stack := snap.stx.findStack? (·.getRange?.any (·.contains hoverPos)) | return none
  let mut res := ""
  for (stx, _) in stack do
    let some rg := stx.getRange? | continue
    res := s!"{res}\n\n{stx.getKind}\n{stx}\n{repr <| rg.toLspRange text}"
  return some res

[Patrick Massot]

Something disappointing is that I don’t get the expected result when the cursor is on a white space. I’ll need to investigate this.

[Patrick Massot]

But you can already play with those RPC methods if you want. Now that they are separated from each other, they don’t take any extra argument.

[Julian Berman]

Very nice, ok, thanks already for pushing this forward Patrick -- I would like to probably find a beer tonight rather than fight with more computers, but I'll poke at it again at some point myself too.

[Patrick Massot]

No problem, finding a beer is also a nice project!

[Patrick Massot]

If any Lean meta-programming expert is still reading this despite the wall of Lua-related question, I can minimize my white space issue to

import Lean

open Lean Server Lsp FileWorker RequestM

deriving instance Repr for Lsp.Position
deriving instance Repr for Lsp.Range

@[server_rpc_method]
def syntaxStack  (p : TextDocumentPositionParams ) :
    RequestM (RequestTask <| Option String) := do
  let doc ← readDoc
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos) (notFoundX := pure "No snapshot found") fun snap => do
  let some stack := snap.stx.findStack? (·.getRange?.any (·.contains hoverPos)) | return "No syntax stack found"
  let mut res := ""
  for (stx, _) in stack do
    let some rg := stx.getRange? | continue
    res := s!"{res}\n\n{stx.getKind}\n{stx}\n{repr <| rg.toLspRange text}"
  return some res

Calling the syntaxStack function with a position where there is white space in the middle of interesting Lean code returns "No syntax stack found" which is a bit disappointing.

[Patrick Massot]

(I know this function never return None, I just turned the None into debugging strings).

[Patrick Massot]

Julian, I made https://github.com/PatrickMassot/LspExperiments so that you can play with the code if you want.

[Patrick Massot]

The only lua code I added in the plugin is

local function ppresult(result)
  vim.notify(type(result) == "string" and result or vim.inspect(result))
end

function LeanRpc(method, extras)
    local params = vim.lsp.util.make_position_params();
    local sess = require'lean.rpc'.open(0, params);
    require'plenary.async'.void(function() ppresult(sess:call(method, vim.tbl_extend('keep', params, extras))) end)()
  end

[Patrick Massot]

Then I put my cursor in Test.lean and type things like lua LeanRpc("rpcDeclarationRangeAt", {})

[Patrick Massot]

And now I really need to go to bed.

[Patrick Massot]

I will probably have very little time during the week-end, but it’s in a state where it will be easy to resume work.

[Julian Berman]

Yeah it seems like we're not far from something at least useful to start.

[Julian Berman]

I couldn't resist playing at least a bit. Here's a branch (of lean.nvim) with a POC of ]m and [m to move to declaration start and end -- modulo your whitespace question it should work to move to beginning or end of a declaration using ]m / [m -- https://github.com/Julian/lean.nvim/tree/lsp-experiments

It's just an exclusive motion, so the cursor will move to the beginning of the declaration then stay there rather than moving further to the last one right now.

[Patrick Massot]

It works great!