leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant

Lean 4 VSCode Extension

This extension provides VSCode editor support for the Lean 4 programming language. It uses the all new Language Server implemented in Lean.

See Quick Start Demo Video.

Installing the extension and Lean 4

1. Install the extension from the marketplace.

2. Create a new folder called foo and add a file named hello.lean containing the following:

   import Lake
   #eval Lake.versionString

3. Open this folder in VS Code using File/Open Folder.

4. Open your file hello.lean.

5. If Lean is not yet installed on your system you will see a prompt like this:

   

6. Click the Install Lean option and enter any default options that appear in the terminal window.

7. After this succeeds the correct version of Lean will be installed by elan and you should see something like this in the Lean: Editor output panel:

   info: downloading component 'lean'
   info: installing component 'lean'
   Lean (version 4.0.0, commit ec941735c80d, Release)
   

See Complete Setup for more information on how the lean version is determined for your VS Code workspace.

This version of the VS Code extension only works on Lean 4 source files and not Lean 3. There is a separate VS Code extension for Lean 3. You can have both extensions installed at the same time, they can live side by side.

Lake integration

Note that once the Lean toolchain is installed you can also turn your folder into a Lake project. Lake is a build system for Lean projects. The VS code extension will honor the Lean version specified in your lean-toolchain file.

Open a VS Code Terminal window in your foo folder and type the following:

lake init foo
lake build

This will add some package definition files to your project along with a Main.lean entry point and build an executable program. You can run the program ./build/bin/foo and you will see the expected output:

Hello, world!

Features

The extension supports the following features. For basic VS Code editor features, see the VS Code User Interface docs.

The extension provides:

• A set of handy Lean4: commands available with Ctrl+Shift+P
• Side-by-side compatibility with the Lean 3 VSCode extension
• Nice integration with the Lean Language Server as shown below.
• An Infoview panel showing interactive information about your Lean programs.

Lean language server features

• Automatic installation of Lean using elan.

• Incremental compilation and checking via the Lean server (*)

• Type information & documentation on hover

• Error messages and diagnostics

• Syntax highlighting with basic Lean 4 syntax rules

• Semantic highlighting

• Hover shows documentation, types:

  

• Auto-completion drop downs based on context and type via the Lean Server. For example, if you type "." after Array you will get:

  

• An Infoview displaying useful information about your current Lean program.

• Goto definition (F12) will work if the Lean source code is available. A standard elan install of the Lean toolchain provides Lean source code for all the Lean standard library, so you can go to the definition of any standard library symbol which is very useful when you want to learn more about how the library works. Note also that currently goto definition does not work if the cursor is at the very end of a symbol like Array.append|. Move the cursor one character to the left Array.appen|d and it will work. See open issue #767.

• Breadcrumbs

(*) Incremental updates do not yet work automatically across files, so after changing and rebuilding the dependency of a Lean 4 file, the language server needs to be manually informed that it should re-elaborate the full file, including the imports. This can be done using the Lean 4: Refresh File Dependencies command, which can be activated via Ctrl+Shift+X.

Lean editing features

• Support for completing abbreviations starting with a backslash (\). For example you type \alpha and the editor automatically replaces that with the nice Unicode character α. You can disable this feature using the lean4.input.enabled setting, see below.
• When you hover the mouse over a letter that has one or more abbreviations you will see a tooltip like this:
• Auto-completing of brackets like (), {}, [], ⟦ ⟧, ⦃ ⦄, ⟮ ⟯, ⦃ ⦄ and block comments /- ... -/.

Infoview panel

The Infoview panel is essential to working interactively with Lean. It shows:

• Tactic state widgets, with context information (hypotheses, goals) at each point in a proof / definition,
• Expected type widgets display the context for subterms.
• Types of sub-terms in the context can be inspected interactively using mouse hover.
• All Messages widget, which shows all info, warning, and error messages from the Lean server for the current file.

Suppose you have the following theorem:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p :=
  by apply And.intro
     exact hp
     apply And.intro
     exact hq
     exact hp

and you place the cursor at the end of the line by apply And.intro the Infoview will display the following information:

(1). The Infoview will activate automatically when a Lean file is opened, but you can also reopen it any time using the icon in the top right of the text editor window or the Ctrl+Shift+P Lean 4: Infoview: Display Goal command or the key that is bound to the command, which is Ctrl+Shift+Enter by default. You can also disable auto-opening behavior using the setting lean4.infoViewAutoOpen described below.

(2) through (6):

Symbol	Description
	Copy the contents of the widget to a comment in the active text editor.
	Remove a pinned widget from the Infoview.
	Split off a "pinned" tactic state widget, which tracks the tactic state at a fixed position, even if you move your cursor away. When pinned you will see the unpin and reveal file location icons appear.
	Move the cursor in the editor to the pinned location in the file.
	Prevent the tactic state widget from updating when the file is edited. When paused you will see the following addition icons show up.
	Once paused you can then click this icon to resume updates.
	Refresh the tactic state of the pinned widget.
	Reverse the order of the lists under Tactic State.

(7). Types in the context can be examined in the tactic state widget using mouse hover:

(8). The "All Messages" widget can be expanded by clicking on it (or hitting the keybind for lean4.displayList, which is Ctrl+Shift+Alt by default)

Extension Settings

This extension contributes the following settings (for a complete list, open the VS Code Settings and type Lean4 in the search box):

Server settings

• lean4.toolchainPath: specifies the location of the Lean toolchain to be used when starting the Lean language server. Most users (i.e. those using elan) should not ever need to change this. If you are bundling Lean and vscode-lean with Portable mode VS Code, you might find it useful to specify a relative path to Lean. This can be done by starting this setting string with %extensionPath%; the extension will replace this with the absolute path of the extension folder. For example, with the default directory setup in Portable mode, %extensionPath%/../../../lean will point to lean in the same folder as the VS Code executable / application.

• lean4.lakePath: specifies the location of the Lake executable to be used when starting the Lean language server (when possible). If left unspecified, the extension defaults to the Lake executable bundled with the Lean toolchain. Most users thus do not need to use this setting. It is only really helpful if you are building a Lake executable from the source and wish to use it with this extension.

• lean4.serverEnv: specifies any Environment variables to add to the Lean 4 language server environment. Note that when opening a remote folder using VS Code the Lean 4 language server will be running on that remote machine.

• lean4.serverEnvPaths: specifies any additional paths to add to the Lean 4 language server environment PATH variable.

• lean4.serverArgs: specifies any additional arguments to pass on the lean --server command line.

• lean4.serverLogging.enabled: specifies whether to do additional logging of commands sent to the Lean 4 language server. The default is false.

• lean4.serverLogging.path: if serverLogging.enabled is true this provides the name of the relative path to the store the logs.

• lean4.autofocusOutput: if true, automatically show the Output panel when the Lean 4 server prints a new message.

• lean4.elaborationDelay: Time (in milliseconds) which must pass since latest edit until elaboration begins. Lower values may make editing feel faster at the cost of higher CPU usage. The default is 200.

Input / editing settings

• lean4.input.enabled: enables abbreviation input completion mode. For example, it allows you to type \alpha and have that be replaced with the greek letter (α).

• lean4.input.eagerReplacementEnabled: enables/disables eager replacement as soon as the abbreviation is unique (true by default)

• lean4.input.leader: character to type to trigger abbreviation input completion input mode (\ by default).

• lean4.input.languages: specifies which VS Code programming languages the abbreviation input completion will be used in. The default is [lean4, lean].

• lean4.input.customTranslations: add additional input Unicode translations. Example: {"foo": "☺"} will correct \foo to ☺ (assuming the lean.input.leader has its default value \).

• lean4.typesInCompletionList: controls whether the types of all items in the list of completions are displayed. By default, only the type of the highlighted item is shown.

• lean4.fallBackToStringOccurrenceHighlighting: controls whether the editor should fall back to string-based occurrence highlighting when there are no symbol occurrences found.

Infoview settings

• lean4.infoview.autoOpen: controls whether the Infoview is automatically displayed when the Lean extension is activated for the first time in a given VS Code workspace(true by default). If you manually close the Infoview it will stay closed for that workspace until. You can then open it again using the Ctrl+Shift+P Lean 4: Infoview: Display Goal command.

• lean4.infoview.autoOpenShowsGoal: auto open shows goal and messages for the current line (instead of all messages for the whole file). In this mode the Infoview updates often every time you move the cursor to a different position so it can show context sensitive information. Default is true.

• lean4.infoview.allErrorsOnLine: show all errors on the current line, instead of just the ones to the right of the cursor, default true.

• lean4.infoview.debounceTime: how long (in milliseconds) the infoview waits before displaying new information after the cursor has stopped moving. The optimal value depends on your machine - try experimenting. The default is 50.

• lean4.infoview.showExpectedType: show the expected type by default. This display can then be toggled by clicking on the title or using the Ctrl+Alt+e Lean 4: Infoview: Show Expected Type command. The default is true.

• lean4.infoview.showGoalNames: show goal names (e.g. case inl in the infoview). The default is true.

• lean4.infoview.emphasizeFirstGoal: emphasize the first goal by displaying the other goals with reduced size and opacity. The default is false.

• lean4.infoview.reverseTacticState: show each goal above its local context by default. This can also be toggled by clicking a button (see the Infoview panel description above). The default is false.

Colors

These colors are used to display proof states in the infoview:

• lean4.infoView.hypothesisName: accessible hypothesis names
• lean4.infoView.inaccessibleHypothesisName: inaccessible hypothesis names
• lean4.infoView.goalCount: the number of goals
• lean4.infoView.turnstile: the turnstile (⊢) that separates the hypotheses from the goal
• lean4.infoView.caseLabel: case labels (e.g. case zero)

They can be set in a color theme, or under workbench.colorCustomizations in the settings file.

Extension commands

This extension also contributes the following commands, which can be bound to keys if desired using the VS Code keyboard bindings.

The format below is: "lean4.commandName (command name): description", where lean.commandName represents the name used in settings.json and "command name" is the name found in the command palette (accessed by hitting Ctrl+Shift+P).

Server commands

• lean4.restartServer (Lean 4: Restart Server): restart the Lean 4 Language Server. Useful if you built new .olean files in your workspace.

• lean4.stopServer (Lean 4: Stop Server): stop the Lean 4 Language Server.

• lean4.restartFile (Lean 4: Restart File): restarts the Lean server for a single file. Useful if the server crashes. As a side-effect this command will also recompile all dependencies. This command has a default keyboard binding of Ctrl+Shift+X.

• lean4.refreshFileDependencies (Lean 4: Refresh File Dependencies): An alias for lean4.restartFile. The Lean server does not automatically update a file when one of its dependencies is changed. So after changing a dependency, the server for the file needs to be restarted to pick up the changed dependency.

Editing commands

• lean4.input.convert (Lean 4: Input: Convert Current Abbreviation): converts the current abbreviation (bound to tab by default)

Infoview commands

• lean4.displayGoal (Lean 4: Infoview: Display Goal): open the Infoview panel (bound to Ctrl+Shift+Enter by default)

• lean4.displayList (Lean 4: Infoview: Toggle "All Messages"): toggles the "All messages" widget in the Infoview (bound to ctrl+alt+shift+enter by default)

• lean4.infoView.copyToComment (Lean 4: Infoview: Copy Contents to Comment"): if there is a valid value in the Infoview marked with the icon that can be copied to a comment, this command invokes that action in the editor.

• lean4.infoView.toggleStickyPosition (Lean 4: Infoview: Toggle Pin): enable / disable "sticky" mode. On enable, a tactic state widget will be created and pinned to this position, reporting the goal from this point even as the cursor moves and edits are made to the file. On disable the pinned widget will be removed. (same as clicking on the or icon on the tactic state widget closest to the cursor.)

• lean4.infoView.toggleUpdating (Lean 4: Infoview: Toggle Updating): pause / continue live updates of the main (unpinned) tactic state widget (same as clicking on the or icon on the main tactic state widget.)

• lean4.infoView.toggleExpectedType (Lean 4: Infoview: Toggle Expected Type): toggles the "Expected Type" widget in the Infoview (bound to ctrl+alt+e by default)

Documentation commands

• lean4.docView.open (Lean 4: Open Documentation View): Open documentation found in local 'html' folder in a separate web view panel.

• lean4.docView.showAllAbbreviations (Lean 4: Show all abbreviations): Show help page containing all abbreviations and the Unicode characters they map to. This makes it easy to then search for the abbreviation for a given symbol you have in mind using Ctrl+F.

Complete Setup

The complete flow chart for determining how elan and lean are installed is shown below:

The start state is when you have opened a folder in VS Code and opened a .lean file to activate this extension.

If the extension finds that elan is not in your path and is not installed in the default location then it will prompt you to install lean via elan. If the folder contains a lean-toolchain version it will install that version otherwise it will install leanprover/lean4:stable. You can override this default version by setting an DEFAULT_LEAN_TOOLCHAIN environment variable.

Otherwise, if there is a lean-toolchain in the workspace folder or in a parent folder then it will use the version specified in the specified version.

Then with the selected version it runs lean --version to check if that version is installed yet. If this version is not yet installed lean --version will install it.

For VSCode extension developers

See Development.

vscode-lean4's Issues

Sometimes the copy to comment feature from infoview doesn't work

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');

Make use of fullRange when selecting messages in info view

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.

Bootstrap could prompt user with known good releases

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.

infoview crashes every type error and crashes if multiple files opened

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.
..........

Inconsistent naming

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

Uses of inaccessible hypotheses not distinguishable from accessible ones

Compare

with Emacs:

Too many errors during bootstrap is confusing

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

RPC session expires after a few minutes

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

Update readme from https://github.com/leanprover/vscode-lean

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

Imports fail with 'no such file or directoy'

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.

server crashes if I set "lean4.serverLogging.path": ""

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.

Local toolchain setting is intransparent and can't be reset

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.

import Foo.αβγ doesn't work on Windows

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.

Start lean server using `lake serve`

Related to #61.

"Watchdog error: Got unknown document URI"

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.

"reveal file location" should move the keyboard focus to the text editor

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

Go to definition not working in Lean 4 repository

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.

Proof state not shown

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?

Initialization bug in info view

See attached video for explanation and repro:

InfoviewBug.mp4

Documentation view with "Try This" to run code snippets locally.

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.

Code actions, to "fill holes" with suggestions from Lean Language Server

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?

Search for declarations in open files (ctrl+t)

lean4 server needs to add this.

Help setup Lake build/clean tasks

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"
        }
    ]
}

Port automatic elan installation

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?

Should start a fresh server per folder

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

Better line wrapping of long snippets in the InfoView

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.

Lean --server not working on "Untitled-1" unsaved files.

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...

InfoView font size

how can the user customize the InfoView font size?

Opening files causes `Watchdog error: Got unknown document URI`

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.

LSP stack overflow

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)

Autocompletion after inputting an underscore

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.

Sometimes elan setup fails

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

Extension watches lean-toolchain files in subdirectories

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.

Resurrect tactic state filters

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.

Keyboard accessibility warnings from Tippy

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
"

Yellow bar doesn't disappear when there are invalid imports.

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!

Multiple 'Lean 4' output channels created

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

Pretty exports

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 👍

Use Prettier for formatting

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

Output channel is opened when vscode is started

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.

Support "untrusted workspaces"

microsoft/vscode#106488

Had to remove extension from ~/.vscode to restore lean-community functionality

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.

Syntax highlighting bugs

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

Hovering over an expression inserts a newline

Use the new lineRange parameter of the interactive diagnostics command.

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

InfoView stops updating afer "Lean 4: Resstart Server" command

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

Infoview doesn't show errors when lake fails

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").

Sometimes the rpc session is released when it shouldn't be.

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:

Add Lake support

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.

lean4: 'lean --version' returned incorrect version string 'Lean (version 4.0.0, Release) '

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