LSP-based infoview #30

Vtec234 · 2021-06-25T02:59:40Z

This PR splits the infoview into a separate NPM package independent of VSCode, and based on a more general editor<->infoview API based on LSP. Changes include:

The new infoview API tries to provide more general functionality, basing most of it on LSP requests and the ability to listen in on incoming/outgoing LSP notifications from within the infoview. This is intended to allow using custom requests from widget code.
- This is not as nice to implement on the VSCode extension side as one might like. See here for why. This may be fixable in upstream vscode-jsonrpc.
- I expect the new API to be more easily implementable in any other text editor capable of displaying a webpage.
Fixes in various edge cases. For example, we now delete pins when the corresponding file is closed as the server cannot produce goal states for them any more.
We handle more stuff in the infoview. For example, pins are synced there without going through the extension by subscribing to textDocument/didChange.
Outsourced tachyons CSS and codicons to NPM packages. I took the artistic liberty of changing the codicon for copy-to-comment to "quote" (see it here) as I couldn't find the current one (and maybe "quote" is a little clearer?).
Some refactoring, primarily on info.tsx. UI code is difficult, but I tried to separate the concerns of pausing and fetching goals into different and maybe reusable components.
The repository is now organised into a "monorepo" containing two packages. We use Lerna to manage them.
Probably other things I forgot.

I apologise for making the development a bit hard to follow. I made commits to a separate repo before copying the files here. They can be browsed.

There are quite a lot of changes, and while I tried testing all functionality I expect there to be some breakage. Still to be fixed:

Re-send diagnostics to infoview on startup
Implement "copy-to-comment" (~~now a general "make text edit" API~~)

README.md

lean4-infoview/src/infoview/index.css

lean4-infoview/src/infoview/goal.tsx

lean4-infoview/src/infoview/infos.tsx

vscode-lean4/src/infoview.ts

vscode-lean4/src/leanclient.ts

vscode-lean4/src/rpc.ts

lean4-infoview/src/infoview/messages.tsx

lean4-infoview/src/infoview/info.tsx

Vtec234 · 2021-06-29T01:26:34Z

vscode-lean4/src/leanclient.ts

@@ -163,9 +160,6 @@ export class LeanClient implements Disposable {
                }
            },
        }
-        this.setProgress(Object.assign({}, ...workspace.textDocuments


Removing this changes the semantics slightly in that yellow bars only appear when the server actually begins compiling the header. I think this is nice, as visually indicates things are working.

I don't have extremely strong feelings about this, but it was very much intentional. When opening a Lean file, I'm interested in whether there are errors or not. The progress bars allow me to distinguish the states of "no errors because Lean hasn't compiled this part yet" and "no errors because the proof is fine".

This is the same reason why I said that the fileProgress notification should be sent before processing is started (in leanprover/lean4#503). The important information is not that Lean is still running, but that it is not finished yet.

I see your point. The only real difference is that with this change, if the server fails to start the gutters won't appear, whereas before they'd be there even though nothing is actually being processed. You still know that the lack of errors is due to server failure because there will be the "server failed to start" popup. IMO this way it's clearer when things have failed, and when things are actually compiling (where we do send server notifs before starting compilation as you note), and you can still clearly tell why there are no errors. But if you still disagree, I'm happy to revert this change.

Ah, if this only happens with a dead server then it's a non-issue. In that case you already get a lot of errors anyhow.

Well, there are also no gutters between exec lean --server and "lean --worker sends progress @ 0". This is a few ms right now, but I suppose it could be a problem with a bad plugin which takes long to initialize. We could show progress then.

Vtec234 · 2021-06-29T02:15:36Z

lean4-infoview/src/infoviewApi.ts

-  /** Apply edits to the workspace. */
-  applyEdits(edits: TextDocumentEdit[]): Promise<void>
+  /** Insert text into a document. When `pos` is not present, write at the current cursor location. */
+  insertText(text: string, kind: TextInsertKind, pos?: TextDocumentPositionParams): Promise<void>


Sadly the range of things which can be done with TextEdit without knowing the file contents (and for now we don't really need to track them in the infoview) is quite small, so reinstated this API.

gebner · 2021-06-29T17:46:08Z

I've tried it out a bit now. Some comments:

The LICENSE file should go back into the root directory.
The release.sh script should also go back into the root directory, and run npm run build after npm i. (Ideally, there'd be a github action which uploads the release when a tag is pushed, but we can do that another time.)
There's quite a bit of flickering when you move the cursor through a file (it switches between "No info found." and something else). This might be related to https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/Auto.20completion/near/233509746 and eafe2e1
I'm not sure what I think about the grayed-out identifiers. Graying out the hypothesis name foo✝ in foo✝ : Nat is a positive change in my eyes (since you can easily spot the accessible hypotheses). But graying them out in the rest of the term looks very distracting (since it's the only highlighting so it sticks out like a sore thumb).
The pinned info shows Loading... for a short time every time you type something.
Copy-to-comment produces an extra newline.
vscode now uses 230% CPU (with 4 processes)

Kha · 2021-06-29T19:27:01Z

* But graying them out in the rest of the term looks very distracting (since it's the only highlighting so it sticks out like a sore thumb).

In Emacs I quickly got used to it, and I believe @leodemoura liked them as well. I haven't seen this PR in action yet though, it might be a case of color schemes. Here is what it looks like in Emacs for me currently:

leodemoura · 2021-06-29T19:35:30Z

* But graying them out in the rest of the term looks very distracting (since it's the only highlighting so it sticks out like a sore thumb).
In Emacs I quickly got used to it, and I believe @leodemoura liked them as well. I haven't seen this PR in action yet though, it might be a case of color schemes. Here is what it looks like in Emacs for me currently:

I get something very similar on my machine, and yes I like it too :)

gebner · 2021-06-29T19:37:23Z

It's a much lighter gray here:

With #777 as the gray color for the light theme it looks better for me.

Vtec234 · 2021-06-29T19:41:40Z

The LICENSE file should go back into the root directory.
vscode now uses 230% CPU (with 4 processes)

fixed

The release.sh script should also go back into the root directory, and run npm run build after npm i. (Ideally, there'd be a github action which uploads the release when a tag is pushed, but we can do that another time.)

I made an attempt at how this should work but cannot test it without the PAT, so feel free to change things. Note the slightly weird --scope=lean4 because the extension package is named lean4. Ideally we'd rename it to something like @lean4/vscode-extension but not necessary if it would cause trouble with the extension marketplace.

Vtec234 · 2021-06-29T20:10:55Z

Copy-to-comment produces an extra newline

This is also the current behaviour, but I removed the newline.

There's quite a bit of flickering when you move the cursor through a file

The pinned info shows Loading... for a short time every time you type something.

I removed the Loading... indicator, I think it is nicer this way. In particular we still get a gold font on the status line when things are loading so no information is lost.

gebner · 2021-06-29T20:23:53Z

Copy-to-comment produces an extra newline

This is also the current behaviour, but I removed the newline.

Oops, I didn't notice that. You're right of course.

There's quite a bit of flickering when you move the cursor through a file

The pinned info shows Loading... for a short time every time you type something.

I removed the Loading... indicator, I think it is nicer this way. In particular we still get a gold font on the status line when things are loading so no information is lost.

I think that was a different bug. I mean the following:

#eval 1 + Nat.zero

Put the cursor on Nat, and pin the info.
Insert spaces before 1.

Every space increases the position of the pin by two!
On every keystroke, the expected type briefly disappears.

After some spaces, the pin is beyond the end of the line.

Vtec234 · 2021-06-30T01:37:45Z

I fixed the type disappearing. As for the double-move, I also observed that before but can't anymore. I will wishfully think it disappeared along with one of the recent changes, but let me know if it's still buggy. Also the pin movement is still incorrect if you insert a newline before 1 and then immediately remove it, but that also seems broken in the current code so is no regression.

gebner · 2021-06-30T17:46:19Z

I still get the double-moves.

Vtec234 · 2021-06-30T23:15:20Z

Fixed now, hopefully. This was only observable on development builds because it was (intentionally, to catch this kind of bug) triggered by React.StrictMode.

Vtec234 · 2021-07-13T20:14:34Z

@gebner I've been test-driving this since the PR and it seems to work fine. I think it's good to go. Though I probably wouldn't release a new version until there are actually new features (WIP) using the LSP API.

gebner · 2021-07-14T12:35:21Z

Great! I'll make a release so that we get some free testing!

gebner · 2021-10-20T18:23:25Z

vscode-lean4/package.json

+	"version": "0.0.31",
+	"publisher": "leanprover",
+	"engines": {
+		"vscode": "^1.57.0"


@Vtec234 Do you remember why you had to bump the vscode minimum version requirement here? Does this PR use any new vscode feature?

I wanna say it was something to do with the webview API, but I honestly don't remember, sorry.

No problem. We just run into an issue where the vscode-languageclient library has a hard requirement on the latest vscode version, and then I checked out the version requirement we had in package.json.

In any case, please don't bump this version unnecessarily. Old vscode versions won't install extensions that are not compatible with them.

Vtec234 added 8 commits June 24, 2021 19:41

chore: remove infoview folder

f4c8889

feat: new infoview package

1978e04

chore: just let me comment stuff out

9a52dcf

chore: misc fixes

dfac62d

feat: adapt extension to infoview package

ab0f6f8

chore: move extension into subfolder

7a1bb55

chore: add README

d839cbb

chore: monorepo setup

44a9bf3

gebner reviewed Jun 27, 2021

View reviewed changes

Vtec234 added 2 commits June 28, 2021 11:14

chore: dev setup

cd18e41

fix: misc review fixes

bf12ceb

gebner reviewed Jun 28, 2021

View reviewed changes

lean4-infoview/src/infoview/info.tsx Outdated Show resolved Hide resolved

Vtec234 added 8 commits June 28, 2021 11:46

fix: remember collapsing state

9bd108b

fix: use default handler for custom notifications

c2978ac

fix: use global progress state in infoview

91375d8

chore: revert error stringification

fc9be1d

chore: adapt READMEs

7d40214

chore: fold optional state into one variable

781ced4

feat: send state on infoview startup

885e9c7

fix: prevent invoking RPC methods until other side is ready

e4a7cdc

Vtec234 commented Jun 29, 2021

View reviewed changes

chore: reinstate copyToComment

3ea8be4

Vtec234 marked this pull request as ready for review June 29, 2021 02:13

Vtec234 commented Jun 29, 2021

View reviewed changes

Vtec234 and others added 4 commits June 28, 2021 23:57

fix: misc and packaging fixes

15dcbc4

chore: no gutters on server failure

ba9ed30

chore: fix exclude directories

67a33ab

chore: also exclude the dist folder

d37c9a6

fix: initialization loop

4c1cdbc

chore: move license

c3a17e4

Vtec234 force-pushed the lsp-infoview branch from 6d20e6e to e3b93fa Compare June 29, 2021 19:40

chore: release script

6f15d9e

Vtec234 force-pushed the lsp-infoview branch from e3b93fa to 6f15d9e Compare June 29, 2021 19:44

chore: misc ux

9a24e2b

fix: pin type flickering

edbad96

Vtec234 force-pushed the lsp-infoview branch from de1d20f to edbad96 Compare June 30, 2021 01:30

fix: impure state update

4bec2d3

Vtec234 added 2 commits July 9, 2021 11:55

fix: convert fullRange and misc fixes

8010e34

feat: send notifications from infoview

6e188d6

gebner merged commit 0dd38a7 into leanprover:master Jul 14, 2021

rish987 mentioned this pull request Aug 5, 2021

Support pinnable infoview messages Julian/lean.nvim#84

Closed

gebner reviewed Oct 20, 2021

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

LSP-based infoview #30

LSP-based infoview #30

Vtec234 commented Jun 25, 2021 •

edited

Loading

Vtec234 Jun 29, 2021

gebner Jun 29, 2021

Vtec234 Jun 29, 2021

gebner Jun 29, 2021

Vtec234 Jun 29, 2021

Vtec234 Jun 29, 2021

gebner commented Jun 29, 2021

Kha commented Jun 29, 2021

leodemoura commented Jun 29, 2021

gebner commented Jun 29, 2021

Vtec234 commented Jun 29, 2021

Vtec234 commented Jun 29, 2021

gebner commented Jun 29, 2021

Vtec234 commented Jun 30, 2021

gebner commented Jun 30, 2021

Vtec234 commented Jun 30, 2021

Vtec234 commented Jul 13, 2021

gebner commented Jul 14, 2021

gebner Oct 20, 2021

Vtec234 Oct 20, 2021

gebner Oct 20, 2021

LSP-based infoview #30

LSP-based infoview #30

Conversation

Vtec234 commented Jun 25, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gebner commented Jun 29, 2021

Kha commented Jun 29, 2021

leodemoura commented Jun 29, 2021

gebner commented Jun 29, 2021

Vtec234 commented Jun 29, 2021

Vtec234 commented Jun 29, 2021

gebner commented Jun 29, 2021

Vtec234 commented Jun 30, 2021

gebner commented Jun 30, 2021

Vtec234 commented Jun 30, 2021

Vtec234 commented Jul 13, 2021

gebner commented Jul 14, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Vtec234 commented Jun 25, 2021 •

edited

Loading