Syntax pos to LSP pos

Stream: lean4

[Joachim Breitner]

Hmm, I am still banging my head against using the EditorApifor what I want to do; mostly about generating insertText()’s third parameter of type TextDocumentPositionParams. Currently I am using this code in lean to get my hands on a LSP-compatible position and pass it to JS

  | `(#edit $tm) => do
    let s ← match Lean.Syntax.reprint tm with
      | some s => pure s
      | none => throwUnsupportedSyntax
    let r ← match Lean.Syntax.getRange? tm with
      | some r => pure r
      | none => throwUnsupportedSyntax
    let fm := s.toFileMap
    let lp := String.Range.toLspRange fm r
    dbg_trace "lp: {toJson lp.start}"
    saveWidgetInfo `insertTextWidget (Json.mkObj [("pos", toJson lp.start)]) tm

but there are two problems

• TextDocumentPositionParams needs a uri. For a while I thought this pos actually included and uri field, but it somehow disappeared later… so not sure about that
• The toLspRange produces {"line": 1, "character": 1255}, i.e. does not take line counts into account, which is not really correct (i.e. if I manually specify the uri in the JS side of things, it does insert things but in the second column)

Is there a more principled way to connect lean’s Syntax markers with LSP’s TextDocumentPositionParams?
Or maybe easier to do it all from lean somehow, once there are functions exposed to the lean world that allow me to edit the text? (Pinging @Edward Ayers again if that's ok)

[Sebastian Ullrich]

Answering the parts I know about (i.e. nothing about widgets per se):

• The elaborator doesn't know about the document URI, yes. This information only exists in the server data structures. I'm not aware of a way to access it from an elaborator (which generally is oblivious to the potential existence of a server).
• You can however hackishly recover the document contents via

  let .original pre .. := stx.getHeadInfo | panic! "expected input syntax"
  let s := pre.str

This should give you correct output for toLspRange in contrast to reprint

[Sebastian Ullrich]

Doing anything document-related in a server handler would definitely be better, yeah

[Joachim Breitner]

Is “replace a range in the document with a given string” already a kind of “anything” that one can do from the server?

[Joachim Breitner]

Thanks for the code! Indeed now I get the right coordinates.

[Edward Ayers]

You can do that from the server by making an LSP request to workspace/applyEdit. The problem is that at the moment there is no api in Lean for making server → client editor requests.

[Edward Ayers]

So in order to do a text edit from a server you need to muck around piping lsp requests to an IO stream.

[Sebastian Ullrich]

Also /cc @Jakob von Raumer who just had a student working on that topic (but using client-side edits afair)

[Joachim Breitner]

I feel slightly crazy. I am very certain that with an earlier version of the code, I saw an uri argument in the data that I somehow extracted from the Syntax, but it disappeared.

[Sebastian Ullrich]

Edward Ayers said:

So in order to do a text edit from a server you need to muck around piping lsp requests to an IO stream.

writeLspRequest should just work from the server side as well, no? The server will crash on receiving unexpected responses from the client, but for a prototype I guess we can just discard them instead...

[Jakob von Raumer]

/cc @Robin Böhne

[Jakob von Raumer]

This is the code Robin wrote: https://github.com/leanprover/lean4/compare/master...KaseQuark:lean4:master

[Joachim Breitner]

Is that an interactive conv mode tatic assembler UI? Neat!

It looks like that needs a similar infrastructure than what I want to build right now. So if that still needs extra plumbing, maybe I’ll wait for that code to be merged and then build on top of that :-)

[Jakob von Raumer]

Joachim Breitner said:

Is that an interactive conv mode tatic assembler UI? Neat!

Yes! It's working perfectly, just needs a bit of clean-up and to be PRed

[Joachim Breitner]

@Edward Ayers Trying to use [applyEdit](https://github.com/leanprover/vscode-lean4/blob/1edd92230c7630627f18dbe76cd139903a4cbcee/lean4-infoview-api/src/infoviewApi.ts#L55] instead of insertText now, but I get this.methods[i] is not a function with

TypeError: this.methods[i] is not a function
    at t.Rpc.<anonymous> (/home/jojo/.vscode/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:497315)
    at Generator.next (<anonymous>)
    at /home/jojo/.vscode/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:496341
    at new Promise (<anonymous>)
    at n (/home/jojo/.vscode/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:496086)
    at /home/jojo/.vscode/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:497222
    at t.Rpc.messageReceived (/home/jojo/.vscode/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:497382)
    at /home/jojo/.vscode/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:479116
    at w.invoke (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:145)
    at v.deliver (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:2266)
    at p.fire (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:1844)
    at d.$onMessage (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:87:186534)
    at s._doInvokeHandler (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:95:13708)
    at s._invokeHandler (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:95:13390)
    at s._receiveRequest (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:95:12159)
    at s._receiveOneMessage (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:95:11056)
    at /nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:95:8957
    at w.invoke (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:145)
    at v.deliver (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:2266)
    at p.fire (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:1844)
    at a.fire (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:69:18976)
    at /nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:111:34679
    at w.invoke (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:145)
    at v.deliver (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:2266)
    at p.fire (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:1844)
    at a.fire (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:69:18976)
    at r._receiveMessage (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:69:23563)
    at /nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:69:21097
    at w.invoke (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:145)
    at v.deliver (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:2266)
    at p.fire (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:61:1844)
    at p.acceptChunk (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:69:15807)
    at /nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:69:14937
    at Socket.R (/nix/store/8ybggqbzhpmj6ax299x7kz9b53861frx-vscode-1.69.2/lib/vscode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:111:13763)
    at Socket.emit (node:events:390:28)
    at addChunk (node:internal/streams/readable:315:12)
    at readableAddChunk (node:internal/streams/readable:289:9)
    at Socket.Readable.push (node:internal/streams/readable:228:10)
    at Pipe.onStreamRead (node:internal/stream_base_commons:199:23)

so does this mean that this function isn’t fully implemented yet, or am I doing something stupid?

[Wojciech Nawrocki]

@Joachim Breitner could you by any chance share your widget code?

[Joachim Breitner]

Let me create a repo…

[Joachim Breitner]

https://github.com/nomeata/lean4-interactive-tactic

[Joachim Breitner]

The URL to the edited file is hardcoded in the .ts code :-)

[Wojciech Nawrocki]

Give me a few minutes, i will try to reproduce the error

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/1846

[Wojciech Nawrocki]

Joachim Breitner said:

https://github.com/nomeata/lean4-interactive-tactic

(The pushed version might be missing rollup.config.js)

[Wojciech Nawrocki]

@Joachim Breitner aha, I see what happened. Your link to applyEdit is for the current master branch of the infoview api, but it had not been published yet. If you look at the .d.ts that TypeScript gives you for EditorApi, that function is not there. We will need to make a new API release very soon, which will include this.

[Wojciech Nawrocki]

@Joachim Breitner okay, while the applyEdit interface not-yet-having-been-published does result in type errors, secretly you can still use it because the vscode-lean4 already includes the new code. The reason for that error was not a missing interface, it was a type error in your changes code :) Here is a version that works for me:

    const te : TextEdit = { range: props.range, newText : "hello" }
    var changes: { [_: DocumentUri]: TextEdit[] } = {}
    changes[uri] = [ te ]
    const we : WorkspaceEdit = { changes }

[Wojciech Nawrocki]

And we can write

    // @ts-ignore
    editorConnection.api.applyEdit(we);

to ignore the type error.

[Joachim Breitner]

I should probably figure out how to use a git version of the infoview.
I assume I need it both in ~/.vscode somewhere, and also in my projects package.json so that TypeScript can typecheck it (which somehow didn’t work here)

[Joachim Breitner]

(The pushed version might be missing rollup.config.js)

Fixed, sorry.

[Joachim Breitner]

@Sebastian Ullrich , trying your PR, but I am unsure how to call applyWorkspaceEdit from a RequestM (or if that’s even what I should do)
(Can wait until tomorrow of course :-))

[Sebastian Ullrich]

The example I posted in the PR was inside RequestM afair

[Joachim Breitner]

Ah, I was thrown off by the IO type and the error message

type mismatch
  applyWorkspaceEdit { label? := none, edit := ?m.1743 } ctxt.hOut
has type
  IO Unit : Type
but is expected to have type
  RequestM unit : Type

Lean beginner here :-)

[Sebastian Ullrich]

unit looks suspicious :)

[Wojciech Nawrocki]

Joachim Breitner said:

I should probably figure out how to use a git version of the infoview.
I assume I need it both in ~/.vscode somewhere, and also in my projects package.json so that TypeScript can typecheck it (which somehow didn’t work here)

Do you mean using the a local copy of @leanprover/infoview? That would give you types for the new API but not much else, in particular it is unlikely to solve any TypeScript-not-compiling woes. I'm not sure what you mean about ~/.vscode, but you shouldn't have to mess with that directory pretty much ever.

[Joachim Breitner]

I'm not sure what you mean about ~/.vscode, but you shouldn't have to mess with that directory pretty much ever.

What about ~/.vscode/extensions/leanprover.lean4-0.0.95/? Is there no logic there that may be too old for some of these things we are trying to do here?

[Joachim Breitner]

Yay, I just updated a piece of source code from the InfoView! (still hard-coded file uri, but hey :-))

[Joachim Breitner]

Ok, next issue is that I kinda need to define a React component and pass it to the JS world. I am trying the very naive thing of passing JS code in the props to a generic widget, that tries to instantiate it, cargo-culting your code in
https://github.com/nomeata/lean4-interactive-tactic/blob/30c7377899b1b0d4ce6e6203964db85f245ce65b/widget/src/widget.tsx#L17-L24
(but no caching etc.)
I get errors, though, in the import line, namely

• https://reactjs.org/docs/error-decoder.html/?invariant=31&args[]=%5Bobject%20Promise%5D
• https://reactjs.org/docs/error-decoder.html/?invariant=321
  although I do get a module out it seems.

Any hint what I might be doing wrong here?

[Joachim Breitner]

And is there an easy way to run the widget code (or all of code?) with a non-minimized React?

[Edward Ayers]

Can you try replacing fun({}) with e(fun, {})?

[Edward Ayers]

Also you can't have a react component be an async function

[Joachim Breitner]

Tried e(… but the errors already happen at import time.
Ah, that’s useful information. I’ll try to not do that.

[Edward Ayers]

You should wrap the async importing code in a React.lazy https://reactjs.org/docs/code-splitting.html#reactlazy

[Edward Ayers]

Something like:

function myLazyCode(code) {
  return React.lazy(async () ⇒ {
    const file = ...
    ...
    return module.default
  }
}

But then probably also memoise myLazyCode.

[Joachim Breitner]

React.lazy works, yay!

[Joachim Breitner]

I’ll worry about memoisation etc. at some later point, I first want to get to a state where I can show how great this all is (once someone reimplements it properly ;-))

[Edward Ayers]

the memoising is important so that it only loads the module once and you don't get multiple copies of the same component

[Edward Ayers]

Maybe we should expose the dynamic component loading stuff in @leanprover/infoview

[Wojciech Nawrocki]

Joachim Breitner said:

Ok, next issue is that I kinda need to define a React component and pass it to the JS world. I am trying the very naive thing of passing JS code in the props to a generic widget, that tries to instantiate it, cargo-culting your code in
https://github.com/nomeata/lean4-interactive-tactic/blob/30c7377899b1b0d4ce6e6203964db85f245ce65b/widget/src/widget.tsx#L17-L24
(but no caching etc.)
I get errors, though, in the import line, namely

• https://reactjs.org/docs/error-decoder.html/?invariant=31&args[]=%5Bobject%20Promise%5D
• https://reactjs.org/docs/error-decoder.html/?invariant=321
  although I do get a module out it seems.

Any hint what I might be doing wrong here?

I think this is a bit of an #xy problem. I would hope that you wouldn't actually need to do any of the dynamic import tricks. Looking at your other thread, it sounds like you want a widget per instance of Interactive α. Why not associate a UserWidgetDefinition with each such instance and then make the interactive tactic store the ID of the particular widget found by instance resolution in the infotree?

[Joachim Breitner]

That's what I tried, butI didn't immediately see how to look up the widget code by Id from JavaScript. (I need to wrap them with some common code!). So instead o cargo culted what the user widget code is doing.

But this was just the path of least resistance, and cleanup is still needed. I'm calling it a day for now, but PRs are welcome :-)