leanprover / vscode-lean4 Goto Github PK

The extension not only watches the lean-toolchain file in the workspace directory, but also in subdirectories. If a lean-toolchain file in a subdirectory changes, the extension shows a popup prompting the user to restart Lean.

Only the lean-toolchain in the workspace should be considered however, because this is the one which determines the server version.

This is an issue with every project that has dependencies (e.g. core lean and the lake subdirectory). When the dependency is upgraded, we show an unnecessary notification.

repro:

1. get hover tooltip for a type like UInt32, follow that tooltip to Type2, Type3 for a bit.
2. go do some email for a minute or 2 while the tips are removed
3. go back to infoview and repeat step 1.

Sometimes you get:

Fun : IO UInt32
Error: Cannot decode params in RPC call 'Lean.Widget.InteractiveDiagnostics.infoToInteractive({"p":"36"})'
RPC reference '36' is not valid

and sometimes:

Error: already connecting or connected at 'file:///d%3A/Temp/lean_examples/slides/temp.lean'

and sometimes you get: Outdated RPC session from Lean.

This seems to happen often with the popup tips, with the following code paths:

Compare

with Emacs:

Repro is not easy, but some combination of window activations causes window.visibleTextEditors[0] to fail. The solution seems to be to use window.visibleTextEditors.find(e => e.document.languageId === 'lean4');

Related to #61.

I noticed that the autocompletion box opens whenever I want to input a placeholder _, which is pretty annoying. It offers me to complete to _law, of which I have no idea where it comes from.

Opening this issue to document some syntax highlighting bugs. Issues found so far:

• deriving instance <...> for <...> or the empty inductive inductive <...> tags the rest of the file as a declaration name
• Code blocks within comments tag the rest of the file as a comment

See discussion at leanprover/lean4#300 (comment). I hope it does work that way...

The long horizontal scrolling in this example is annoying, we should line wrap:

In Lean 3 we had some fancy CSS that did the formatting (i.e., indenting and inserting newlines at the appropriate places). We also used it for the docs: https://leanprover-community.github.io/mathlib_docs/measure_theory/covering/besicovitch_vector_space.html#besicovitch.exists_good_%CE%B4 (try resizing the browser window).

This webpage is perfect, as it provides client side live resizing (rather than formatting to some fixed width in the LSP). Notice the block {τ : ℝ} wraps as a chunk, and even much bigger things wrap as a block like [normed_group E] and so on. We should copy this nice CSS implementation to the InfoView.

The tab says "Lean Infoview", but the commands say "Info View" :)

To work on the Lean 4 repository in VSCode, we have to run elan override set to point to an appropriate toolchain.

This allows editing .lean files with server support, and go-to-definition (F12) works within a file.

Depending on which toolchain we use, go-to-definition may or may not work for definitions in imported files.
If we use a nightly, then go-to-definition works, but the .lean files that it jumps to are taken from .elan/toolchains, rather than the local build.

If we use a toolchain pointing to the local build, per the instructions

elan toolchain link lean4 build/release/stage1
elan override set lean4

then go-to-definition does not work at all across files.

open a lean file
create a type error
-> shows the type error and
-> (> 50% chance) infoview crashes
-> if infoview didn't crash
-> fix the type errors
->(very likely) infoview hangs indefinitely

I have to restart the infoview, to step through code every time I fix an error.

Infoview either hangs of crashes (without recovering even if I restart)

with following error in the output console

Watchdog error: Got unknown document URI (file:////firstProg.lean)
[Info - 12:46:21 AM] Connection to server got closed. Server will restart.
[Error - 12:46:21 AM] Request textDocument/documentSymbol failed.
Error: Connection got disposed.
..........

For a lack of end, errors such as "unclosed goal" are shown on the initial token of a tactic block, e.g. by instead. However, we now set an additional diagnostic field fullRange to the whole range of the block and use it in lean4-mode to select messages for the current location: leanprover/lean4@3eb91d4
Now I have no idea if VS Code also just forwards the response objects without removing unexpected fields... if it does not, I suppose this could get tricky.

Move this beautiful readme over to vscode-lean4 and update as needed

Provide a way to filter out hypotheses in the tactic state / expected type. For example:

• Hide hidden assumptions (i.e., the ones with the dagger)
• Hide type class instances.
• Hide types (i.e., assumptions like α : Type).
• Hide the gigantenormous let-values inside do-notation.

Some of that may require additional server support though.

Steps to reproduce:

Create a new foo.lean file in VSCode, and import bar (without having created a bar.lean).

There is a red squiggle under import bar saying unknown package 'bar', but the yellow bar (and the pop-up message "busily processing") never disappears.

Expected:

The yellow bar should disappear if nothing further is going to change, regardless of how successful processing the file was!

We should format the whole repository with Prettier on pre-commit and forget about style from then on.

Whenever I open a new vscode instance, the nLean 4 extension opens the output channels and prints the Lean version. It is annoying to close it every time. I believe this is a regression from #35.

We should only show the Install Lean using Elan prompt and not the other 2:

If I leave vscode running in the background for a few minutes (one minute is not enough), then I get the following message (in the infoview hover) when I come back and try to hover over a term in the infoview:

Error: Cannot decode params in RPC call 'Lean.Widget.InteractiveDiagnostics.infoToInteractive({"p":"1"})'
RPC reference '1' is not valid

would be great to have Lake support here as well. Lake uses a simple lean-toolchain file that contains the version string and nothing else.

We are getting these warnings in while debugging when hovering over a type and getting the tooltip popups:

"Interactive tippy element may not be accessible via keyboard navigation because it is not directly after the reference element in the DOM source order. Using a wrapper <div> or <span> tag around the reference element solves this by creating a new parentNode context. Specifying appendTo: document.body silences this warning, but it assumes you are using a focus management solution to handle keyboard navigation. See: https://atomiks.github.io/tippyjs/v6/accessibility/#interactivity
"

Sometimes this dialog does not appear, it seems to be timing related, perhaps on slower laptops it fails:

how can the user customize the InfoView font size?

In the case there is no elan installed and no lean-toolchain file found in the workspace, we could prompt the user with a list of known good toolchains by doing an http query against https://github.com/leanprover/lean4-nightly/releases then prompt for them to select one of those, then install that version.

So I've just tried to debug why the Lean 4 extension used an old Lean 4 nightly for my Lean 3 checkout. Looking through the code, either localStorage.getLeanPath or storage.getLeanVersion must return some override, but I can't tell which.

This is honestly really bad and confusing. If this happened in a Lean 4 project then I would've gone crazy if a file broke in the editor but worked just fine on the command-line with no indication that the editor used some random lean version.

With vscode settings, I can look in the settings tab for the current setting (and it shows the value that I want.....). With elan overrides, I can see what's going on in the command line (I can also query the override with elan override list). But with these local storage settings, I have no idea what they're set to. They're stored in a sqlite database with the wonderfully descriptive name fdbe00b2e2eb8f3841860e8a590c4788/state.vscdb (where of course the json is stored in a string column.....), with no good way to view the contents.

If we want to keep the toolchain selection feature, then the chosen version needs to be transparent to the user and it must be possible to reset the override:

1. There should be a status bar element (like in the python extension) that shows the effective lean version and executable path.
2. The configuration setting description (lean.executablePath) should mention that it might be overridden.
3. The version selection command must be available even if the Lean 3 extension is active.
4. It should be possible to reset the override.

Feel free to nix this "experience/problem report".

I installed lean4 and this extension and used elan override set to set lean4 as the language for a small test project. It seemed to work. Problem was that once I returned to a lean-community-lean3 project, VS Code thought I was still working on a lean4 project. This remained the case even after I disabled this extension. And indeed opening settings and searching for lean showed a bunch of lean4 settings, even though I'd disabled the extension. I was able to restore functionality for editing Lean3 files (only) by manually deleting the lean4 extension directory from ~/.vscode/extensions. I'm no expert on extension engineering, but maybe some cleanup upon disabling the extension is needed -- or an option to remove and not just disable it?

I see in the latest documentation (GitHub) on the lean3 extension that it's meant to be able to co-exist with the lean4 extension, but I wasn't able to get everything working.

C:\Users\clovett\AppData\Roaming\Code\User\settings.json

    "lean4.serverLogging.enabled": true,
    "lean4.serverLogging.path": "",

Actual output:

Watchdog error: no such file or directory (error code: 2)
  file: 
[Info  - 2:35:57 PM] Connection to server got closed. Server will restart.
Watchdog error: no such file or directory (error code: 2)
  file: 
[Info  - 2:35:57 PM] Connection to server got closed. Server will restart.
Watchdog error: no such file or directory (error code: 2)
  file: 
[Info  - 2:35:57 PM] Connection to server got closed. Server will restart.
Watchdog error: no such file or directory (error code: 2)
  file: 
[Info  - 2:35:57 PM] Connection to server got closed. Server will restart.
Watchdog error: no such file or directory (error code: 2)
  file: 
[Error - 2:35:57 PM] Connection to server got closed. Server will not be restarted.

If I delete "lean4.serverLogging.path" it works, but puts the log files in my lean package folder. If I change it to "lean4.serverLogging.path": "logs" then it works.

Documentation view

The book "Theorem Proving in Lean" can be read by hitting ctrl+shift+p and searching for "Lean: Open Documentation View".

Any Lean project with an html/ folder can be displayed in this panel. For example, try out the book Mathematics in Lean.

microsoft/vscode#106488

Versions

lean: v4.0.0-nightly-2021-06-14
lean4 extension: v31
vs code: v1.57

Issue

Autocompleting the type in (at least) an enumerated type, for example

inductive Foo where 
 | bar : F

at F, causes

Stack overflow detected. Aborting.
[Error - 11:22:34 AM] Request textDocument/completion failed.
  Message: Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.
  Code: -32603 
[Error - 11:22:34 AM] Request textDocument/semanticTokens/full failed.
  Message: Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.
  Code: -32603 
[Error - 11:22:34 AM] Request textDocument/documentSymbol failed.
  Message: Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.
  Code: -32603 

The developer console tracks this to

ERR Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.: Error: Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.
	at /home/matt/.vscode/extensions/leanprover.lean4-0.0.31/out/extension.js:2:142328
	at /home/matt/.vscode/extensions/leanprover.lean4-0.0.31/out/extension.js:2:142622
	at Immediate.<anonymous> (/home/matt/.vscode/extensions/leanprover.lean4-0.0.31/out/extension.js:2:142987)
	at processImmediate (internal/timers.js:461:21)

Repro:

1. Launch VS code with no folder open
2. File/New File
3. Command Palette: Change Language Mode
4. select "Lean 4", wait for lean server to start
5. Now edit the new file and add #eval 4+5

No answer appears in the InfoView, in fact the infoview seems to always show nothing. In debugging some things are different in the LSP protocol - for example "didOpen" never fires...

The git commit hash information expected here https://github.com/leanprover-community/vscode-lean4/blob/850ed87ece95487e58eaaf211b296ef75a9e033c/src/extension.ts#L36
is unavailable when lean4 is built using Nix.

$ lean --version
Lean (version 4.0.0, Release)

$ lean -g
GITDIR-NOTFOUND

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Windows can't find the file named "αβγ .lean" in the folder named "Foo", so the utf-8 support needs to also be moved to vscode somehow and to leanpkg.exe...

Steps to Reproduce

bug.tar.gz

1. Load attached into vscode on windows

Expected behavior:

it should work fine, "leanpkg build" on Linux works fine.

Actual behavior:

leanpkg print-paths failed:

stderr:
configuring Foo 0.1
no such file or directory (error code: 2)
  file: .\Foo\a߿.lean

Reproduces how often:

100%

Versions

master c586f9d0b6cc519b8a96807c31435a6a8f0acb10

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Help users configure .vscode/tasks.json so it can do things like this, so the user can use Ctrl+Shift+B to build, and something to clean, and perhaps even run a compiled app, depending on the type of lake project, etc...

{
    // See https://go.microsoft.com/fwlink/?LinkId=733558
    // for the documentation about the tasks.json format
    "version": "2.0.0",
    "tasks": [
        {
            "label": "build",
            "type": "shell",
            "command": "lake build"
        },
        {
            "label": "clean",
            "type": "shell",
            "command": "lake clean"
        }
    ]
}

Steps:

1. install vscode lean4 extension v0.0.39
2. load a lean4 folder
3. check everything works fine, including the infoview.
4. run Lean 4: Resstart Server" command
5. now move caret around the .lean file and check the infoview still works.

Someones you see this output:

Watchdog error: cannot find open document 'file:///d%3A/Temp/lean_examples/Foo/Foo.lean'
[Error - 11:57:39 AM] Connection to server got closed. Server will not be restarted.

and the infoview stops updating.

I'm wondering if this needs to be re-initialized after client restart since the initializeResult will be different after server restart...

await webviewPanel.api.initialize(this.client.initializeResult, this.getLocation(editor))

If you have two files like this:

-- A.lean
does not compile

-- B.lean
import A

And put the cursor on the first line of B, then the infoview doesn't show the error diagnostic for the import error. (Presumably because we also request interactive diagnostics, and treat the resulting error as "no messages found").

lean4 server needs to add this.

The following is with Lean (version 4.0.0-nightly-2021-02-13, commit 172d47c468fb, Release) on macOS and vscode-lean4 0.0.6.

When I use go to definition on a declaration that leads to a different file, the server sometimes dies with after the following log messages. It also happens (rarely) when I start the extension.

[Trace - 9:07:02 PM] Sending notification 'textDocument/didOpen'.
[Error - 9:07:02 PM] Connection to server is erroring. Shutting down server.
[Error - 9:07:02 PM] Connection to server is erroring. Shutting down server.
[Trace - 9:07:02 PM] Sending request 'shutdown - (20)'.
[Error - 9:07:02 PM] Connection to server is erroring. Shutting down server.
[Error - 9:07:02 PM] Connection to server is erroring. Shutting down server.
Watchdog error: Got unknown document URI (file:///Users/bryan/.elan/toolchains/leanprover-lean4-nightly/lib/lean/src/Init/Data/String/Basic.lean)

(The file path there is perfectly valid; I can even cmd+click the link in VS Code and it opens the correct file.)

After this happens, I can't restart the server anymore with the "Lean 4: Restart server" command. I have to close and reopen the VS Code window.

Unfortunately, it doesn't seem very consistent, but I seem to be able to trigger it by using go to definition a few times.

After restarting the Lean server a few times, you will start to see multiple Lean 4 output windows appear. We should clean this up...

See attached video for explanation and repro:

On vscode-lean4 v0.0.23, when opening a file from the File Explorer (or with by following a link), the server dies with the following bug messages multiple times until it stops restarting. However, this does not happen when switching between open tabs.

Watchdog error: Got unknown document URI (file:///<foo.lean>)
[Error - <time>] Connection to server got closed. Server will not be restarted.
[Error - <time>] Request textDocument/documentSymbol failed.
Error: Connection got disposed.
	at Object.dispose (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:145554)
	at Object.dispose (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:225726)
	at C.handleConnectionClosed (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:225939)
	at C.handleConnectionClosed (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:286327)
	at t (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:224028)
	at invoke (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:147167)
	at o.fire (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:147928)
	at Y (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:134812)
	at invoke (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:147167)
	at o.fire (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:147928)
	at g.fireClose (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:155809)
	at Socket.<anonymous> (<home>\.vscode\extensions\leanprover.lean4-0.0.23\out\extension.js:2:157394)
	at Socket.emit (events.js:327:22)
	at Pipe.<anonymous> (net.js:674:12)

The file foo.lean is the file that was just open (and is thus a valid file). After manually restarting the server with the command Lean 4: Restart server everything works fine until I open another file.

Would be nice if when you click the reveal file location icon if it also switch to active editor back to the lean program.

This would fix this issue that's still present in the vscode extension: Julian/lean.nvim#165 (comment)

import Lean

open Lean Elab in
elab "slow" : command => do
  IO.sleep (ms := 1000)
  logInfo "I should be able to see this message in the infoview before the whole file is done."

slow
slow
slow
slow
slow
slow
slow
slow
slow
slow
slow
slow
slow
slow
slow
slow
slow

Need server to provide nice text spans so there's no regex hackery...
From the Lean3 vscode extension readme:

Fill in {! !} holes (also _ holes in Lean 3.16.0c and later) with the code actions menu (ctrl+.)
Tactic suggestions (tactics which suggest edits with a "Try this:" message) can be applied either with a keyboard shortcut (alt+v), by clicking on the info view message, or via code actions (ctrl+.)

the syntax is a bit weird though... (from idris) can we do it without magic syntax?

I have installed Lean 4 using Nix. Based on the source code I thought that there should be some window showing the proof goal but there isn't. Is this a bug or do I have to explicitly open it somehow?

We should set the default toolchain to lean4-nightly as in https://leanprover.github.io/lean4/doc/quickstart.html.
I also wonder if we can make the Windows installation better, e.g. by downloading, unpacking, and running the installer ourselves instead of depending on the bash script. Or maybe an equivalent Powershell script in the elan repo would be a better alternative?

When running Lean 4 nightly (commit 26dda3f63d88) with vscode-lean4 v0.0.24 on Windows, I am encountering the following error on any import:

`leanpkg print-paths` failed:

stderr:
configuring <package>
> sh -c "<home>\.elan\toolchains\leanprover-lean4-nightly\bin/leanmake" LEAN_OPTS="" LEAN_PATH="././build" "build\<Foo.olean>" >&2    # in directory .
uncaught exception: no such file or directory (error code: 2)

It seems to be failing because it is adding build both to LEAN_PATH and to the path of Foo.olean. Reopening VS Code, reloading the window, restarting the lean server, and/or refreshing the dependencies does not fix the issue.

Furthermore, running leanpkg print-paths myself in the directory works:

$ leanpkg print-paths
configuring <package>
././build
./.

So I am not quite sure what is going on.

However, I can report that this error is not present when using the stable build of Lean 4.

Feature suggestion: Add a button (or multiple buttons) that exports the lean file to beautifully formatted rst, md or html (maybe even latex or pdf?) files, depending on user choice.

Some formatting rules in the commentaries would create sections, subsections etc.

I know there's a Python lib for this, but it only has a branch specific for Lean 3. And if we can do it in JavaScript (or maybe even in Lean 4), it would be more straightforward for usage (no Python dependencies).

Do count on me if you need some hands 👍