Zulip Chat Archive

Stream: lean4

Topic: Syntax pos to LSP pos


Joachim Breitner (Nov 17 2022 at 14:49):

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 (Nov 17 2022 at 15:07):

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 (Nov 17 2022 at 15:08):

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

Joachim Breitner (Nov 17 2022 at 15:10):

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 (Nov 17 2022 at 15:13):

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

Edward Ayers (Nov 17 2022 at 15:16):

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 (Nov 17 2022 at 15:17):

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 (Nov 17 2022 at 15:17):

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

Joachim Breitner (Nov 17 2022 at 15:20):

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 (Nov 17 2022 at 15:21):

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 (Nov 17 2022 at 15:23):

/cc @Robin Böhne

Jakob von Raumer (Nov 17 2022 at 15:23):

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

Joachim Breitner (Nov 17 2022 at 15:25):

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 (Nov 17 2022 at 15:30):

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 (Nov 17 2022 at 16:09):

@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 (Nov 17 2022 at 16:10):

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

Joachim Breitner (Nov 17 2022 at 16:11):

Let me create a repo…

Joachim Breitner (Nov 17 2022 at 16:13):

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

Joachim Breitner (Nov 17 2022 at 16:13):

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

Wojciech Nawrocki (Nov 17 2022 at 16:15):

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

Sebastian Ullrich (Nov 17 2022 at 16:22):

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

Wojciech Nawrocki (Nov 17 2022 at 16:44):

Joachim Breitner said:

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

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

Wojciech Nawrocki (Nov 17 2022 at 16:49):

@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 (Nov 17 2022 at 17:04):

@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 (Nov 17 2022 at 17:04):

And we can write

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

to ignore the type error.

Joachim Breitner (Nov 17 2022 at 18:41):

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 (Nov 17 2022 at 18:42):

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

Fixed, sorry.

Joachim Breitner (Nov 17 2022 at 19:40):

@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 (Nov 17 2022 at 19:42):

The example I posted in the PR was inside RequestM afair

Joachim Breitner (Nov 17 2022 at 19:45):

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 (Nov 17 2022 at 19:51):

unit looks suspicious :)

Wojciech Nawrocki (Nov 17 2022 at 20:29):

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 (Nov 18 2022 at 09:29):

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 (Nov 18 2022 at 09:39):

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

Joachim Breitner (Nov 18 2022 at 10:37):

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

Any hint what I might be doing wrong here?

Joachim Breitner (Nov 18 2022 at 10:38):

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

Edward Ayers (Nov 18 2022 at 10:41):

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

Edward Ayers (Nov 18 2022 at 10:41):

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

Joachim Breitner (Nov 18 2022 at 10:42):

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

Edward Ayers (Nov 18 2022 at 10:42):

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

Edward Ayers (Nov 18 2022 at 10:44):

Something like:

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

But then probably also memoise myLazyCode.

Joachim Breitner (Nov 18 2022 at 10:45):

React.lazy works, yay!

Joachim Breitner (Nov 18 2022 at 10:46):

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 (Nov 18 2022 at 10:46):

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 (Nov 18 2022 at 10:49):

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

Wojciech Nawrocki (Nov 18 2022 at 17:56):

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

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 (Nov 18 2022 at 18:25):

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 :-)


Last updated: Dec 20 2023 at 11:08 UTC