This manual covers how to interact with the most recent version of Lean 4 using the most recent version of the VS Code extension.
- Setting up Lean 4
- Configuring settings
- Using commands
- Interacting with Lean files
- Navigating Lean projects
- Managing Lean projects
- Managing Lean versions
- Finding definitions and theorems
- Troubleshooting issues
The 'Setup Guide' of the Lean 4 VS Code extension covers how to set up Lean 4.
Settings of the Lean 4 VS Code extension and VS Code itself can be configured in the 'Settings' page of VS Code. It can be opened by navigating to 'File' > 'Preferences' > 'Settings' or by pressing Ctrl+, (Cmd+,). In the 'Settings' page, the settings of the Lean 4 VS Code extension can be found under 'Extensions' > 'Lean 4'.
The specific settings of the Lean 4 VS Code extension are described in detail in later sections.
The Lean 4 VS Code extensions sets a number of default settings for Lean 4 documents:
- 'Editor: Insert Spaces': true. Pressing
Tabwill insert spaces. - 'Editor: Tab Size': 2. Pressing
Tabwill insert two spaces. - 'Files: Encoding': UTF-8. Files use the UTF-8 encoding.
- 'Files: Eol': \n. All lines use
\nas the line break symbol for consistency between Windows and Unix based operating systems. - 'Files: Insert Final Newline': true. All files are terminated by an empty line.
- 'Files: Trim Final Newlines': true. There is only a single empty line at the end of each file.
- 'Files: Trim Trailing Whitespace': true. There is no redundant whitespace at the end of a line.
It is recommended to leave these settings at their default. Nonetheless, these default settings can be overriden in the 'Settings' page of VS Code by first entering @lang:lean4 into the settings search bar and then changing the respective setting.
 |
|---|
| VS Code 'Settings' page |
The Lean 4 VS Code extension provides several VS Code commands to interact both with the Lean 4 VS Code extension and Lean 4 itself.
When no Lean 4 document has been selected yet, only specific commands that do not need an associated Lean 4 document can be used. This includes creating Lean projects, opening Lean projects, displaying troubleshooting information, managing Lean versions and various documentation commands, like the command to open this manual.
When a Lean 4 document has been selected once, additional commands that can only operate in the context of a Lean 4 document become available. This includes restarting files, restarting Lean, toggling the InfoView and executing project actions in the Lean project associated with the given Lean 4 document. When executing one of these commands, the command will operate in the context of the last Lean 4 document that has been focused in VS Code.
The specific commands that are provided by the Lean 4 VS Code extension are described in detail in later sections.
When any text document is open, VS Code displays a ∀-symbol in the top right of the currently focused document. Clicking this symbol will open the command menu of the Lean 4 VS Code extension.
The command menu displays all commands that are provided by the Lean 4 VS Code extension and that can be applied in the current context. Specifically, when no Lean 4 document has been selected yet, it will only display commands that do not need an associated Lean 4 document, whereas it will display all commands once a Lean 4 document has been selected once.
To hide the ∀-symbol in the top right of the currently focused document when no Lean 4 document has been selected yet, the 'Lean 4: Always Show Title Bar Menu' setting can be disabled.
 |
|---|
| Lean 4 VS Code extension command menu |
All commands can be accessed using the command palette at 'View' > 'Command Palette…' or using Ctrl+Shift+P (Cmd+Shift+P). Typing in 'Lean 4' will display all commands of the Lean 4 VS Code extension. If no Lean 4 document has been selected yet, it will only display commands that do not need an associated Lean 4 document.
 |
|---|
| VS Code command palette |
Many commands in VS Code are bound to chord keyboard shortcuts where multiple keys must be pressed in succession to trigger the command. Chords in VS Code are typically of the form Ctrl+K Ctrl+<some other key> (Cmd+K Cmd+<some other key>), which can be triggered by holding Ctrl (Cmd), pressing K, releasing K and then pressing <some other key>.
The keyboard shortcuts for all commands can be configured by navigating to 'File' > 'Preferences' > 'Keyboard Shortcuts'. Typing in 'Lean 4' will display all commands of the Lean 4 VS Code extension.
 |
|---|
| VS Code keyboard shortcut settings |
This section describes how to use the Lean 4 VS Code extension to interact with, read and navigate individual Lean files.
When opening a Lean file, Lean must first process the file in order to provide most interactive features for it. Since Lean files can contain arbitrary automation that needs to be executed when processing the file, doing so can be potentially expensive.
The current progress for processing the file is displayed using an orange bar on the right side of the editor as part of the scroll bar. Areas of the file that are marked with the orange bar are still being processed, whereas areas of the file where the orange bar has already disappeared have finished processing. An orange bar on the left side of the editor displays which of the source code lines that are currently visible in the editor are still being processed.
When making a change to a file, Lean needs to re-process all declarations that can depend on the declaration that the change was made to. Currently, this means that all code below the point where the change occured needs to be re-processed.
For parts of the file that are currently still being processed, Lean cannot provide any interactive features that require file processing information yet. For example, in unprocessed parts of the file, errors, warnings and information are not displayed, the InfoView will not show the current goal state and hovers will not display a popup until file processing has progressed to the respective part of the file.
 |
|---|
| File processing progress. The orange bar on the right displays the progress for the whole file, whereas the one on the left displays the progress for the currently visible source code lines. |
VS Code displays so-called diagnostics of three severities directly in Lean files using squiggly lines underneath the affected code:
- Errors. A red squiggly line denotes an error that occured while processing this part of the file. For example, syntax errors are denoted using red squiggly lines.
- Warnings. An orange squiggly line denotes a potential issue in this part of the file. For example, unused variables are denoted using orange squiggly lines.
- Information. A blue squiggly line denotes additional information that was produced by this part of the file. For example,
#check 0will produce a blue squiggly line below#check.
Hovering over code that is underlined with a squiggly line will display the contents of the error, warning or information in a hover popup panel.
Positioning the text cursor on the source code line containing the squiggly line will also make an interactive version of the content of the diagnostic show up in the 'Messages' section of the InfoView. The 'All Messages' section displays all interactive diagnostic contents of the whole file.
To reduce visual clutter, for diagnostics that span multiple lines, only the first line of the diagnostic is underlined with a squiggly line. Nonetheless, the diagnostic will show up under 'Messages' whenever the cursor is in the full span of the diagnostic, not just when it is positioned on its first line.
In the scroll bar on the right of the editor, red / orange / blue areas denote that this part of the file contains a diagnostic with the respective severity.
The amount of diagnostics for all open files are displayed in the left portion of the status bar at the bottom of VS Code using error, warning and information symbols. Clicking this section of the status bar will open the 'Problems view' of VS Code that displays all diagnostics for all currently open files and that can be used to quickly navigate to the span of the diagnostic by clicking on an entry or by using the arrow keys and Enter. It can also be opened using the 'View: Show Problems' command or Ctrl+Shift+M (Cmd+Shift+M).
In addition to VS Code's diagnostic squigglies, the Lean 4 VS Code extension provides some additional editor decorations for diagnostics:
- Error and warning range decorations. On the left side of the editor, a circled cross or a warning sign are displayed on lines that contain an error or a warning, respectively. For errors that extend across multiple lines, a vertical red line extends from the circled cross to the last line of the error, where it bends to the right. These decorations can be disabled by unsetting the 'Lean 4 > Show Diagnostic Gutter Decorations' setting.
- 'Unsolved goals' decorations. On lines where an 'unsolved goals' error ends, a special work-in-progress marker is displayed. These decorations can be disabled by unsetting the 'Lean 4 > Show Unsolved Goals Decorations' setting. They can also be themed by using the 'Lean 4 > Unsolved Goals Decoration Light Theme Color' and 'Lean 4 > Unsolved Goals Decoration Dark Theme Color' settings.
- 'Goals accomplished' decorations. On the left side of the editor, a double checkmark is displayed next to theorems that contain no errors and no
sorrys anymore. The double checkmark icon can be disabled or replaced with another icon by changing the 'Lean 4 > Goals Accomplished Decoration Kind' setting.
Using the 'Error Lens' VS Code extension, the line that a diagnostic occurs in is highlighted and the message of the diagnostic is displayed inline in the editor.
 |
|---|
| Error, warning and information diagnostics with corresponding hover- and InfoView information. The red / orange / blue areas in the scroll bar denote the location of the area. The bottom left of the status bar at the bottom of VS Code displays the amount of diagnostics in all open files and clicking this section of the status bar will open the 'Problems view'. |
 |
|---|
| VS Code 'Problems view' |
When a file Module.lean imports another file Submodule.lean, changes in Submodule.lean do not automatically become visible in Module.lean. This is to prevent accidentally triggering expensive builds of all dependents of Submodule.lean.
Instead, the state of all dependencies of Module.lean needs to be updated manually using the 'Server: Restart File' command. This will trigger a build for all changed dependencies. The command can be called using Ctrl+Shift+X (Cmd+Shift+X), using the 'Restart File' button in the InfoView, using the command menu, using the command palette or by right clicking in the editor of a Lean file and selecting the 'Server: Restart File' entry in the context menu.
VS Code will display error- or information-level diagnostics whenever a dependency of a file is edited and saved. When initially opening a file and a dependency would need to be rebuilt to be up-to-date, it issues an error and refuses to process the rest of the file. When a dependency changes while the file is already open, it issues an information-level diagnostic, but will continue processing the file with the previous state of the dependency.
In order to automatically trigger rebuilds of all changed dependencies when opening a file instead of issuing an error, the 'Lean 4: Automatically Build Dependency' setting can be enabled.
 |
|---|
| 'Restart File' button in InfoView |
Lean code uses lots of Unicode symbols to aid readability. In Lean files, these Unicode symbols can be entered by typing a backslash followed by an abbreviation identifier referring to the symbol. As soon as the abbreviation identifier is complete, if the abbreviation identifier is not a prefix of any other abbreviation identifier, the abbreviation will be automatically replaced with the corresponding Unicode symbol - for example, \forall will yield ∀.
To replace an abbreviation early, before it is complete, Tab can be pressed to trigger the 'Input: Convert Current Abbreviation' command. This will yield the Unicode symbol with the shortest abbreviation identifier matching the identifier that was typed. Abbreviations are also replaced early when the text cursor is moved away from the abbreviation.
The full list of supported abbreviation identifiers and Unicode symbols can be viewed using the 'Docs: Show Unicode Input Abbreviations' command that can be found in the 'Documentation…' submenu of the command menu. When encountering a Unicode symbol in Lean code, hovering over the symbol will also provide all available abbreviation identifiers to input the symbol.
For some Unicode brackets, there are special abbreviation identifiers that also insert a matching closing Unicode bracket and ensure that the cursor is in-between the Unicode brackets after replacing the abbreviation. For example, \<> yields ⟨⟩, \[[]] yields ⟦⟧, \f<<>> yields «» and \norm yields ‖‖.
The Unicode input mechanism has several configuration options:
- 'Lean 4 > Input: Custom Translations'. Allows adding additional abbreviation identifiers. For example,
{"foo": "☺"}will add an abbreviation\foothat yields☺. Entries must be comma-separated. - 'Lean 4 > Input: Eager Replacement Enabled'. Unticking this option will disable automatic replacement of complete abbreviations, instead requiring that every abbreviation is replaced using
Tab. - 'Lean 4 > Input: Enabled'. Unticking this option will disable the entire Unicode input mechanism.
- 'Lean 4 > Input: Languages'. Allows adding VS Code language IDs for which the Unicode input mechanism should also be enabled.
- 'Lean 4 > Input: Leader'. Allows replacing the initial character of an abbreviation (
\) with something else.
 |
|---|
Incomplete abbreviation for ∀ |
 |
|---|
| Output when the 'Docs: Show Unicode Input Abbreviations' command is used |
 |
|---|
| Hover for Unicode symbol displaying all abbreviation identifiers |
To use Unicode symbols outside of text editors - for example in the search bar, find widget or settings - a symbol picker is available. The 'Input: Find Unicode Symbol...' command can be used from the command menu or the command palette. After selecting a symbol, a second dialog allows choosing between copying the symbol to the clipboard and inserting it into the active text editor.
There are also two direct commands that skip the second dialog:
- 'Input: Insert Unicode Symbol...' inserts the chosen symbol directly into the active text editor. It is bound to
Ctrl+Alt+\(Cmd+Alt+\) when a text editor is focused. - 'Input: Copy Unicode Symbol...' copies the chosen symbol directly to the clipboard. It is bound to
Ctrl+Alt+\(Cmd+Alt+\) when no text editor is focused.
Both direct commands display a button on each item for the other action, so that e.g. a symbol can be copied to the clipboard while using the insert command without having to reopen the dialog.
The search field in the symbol picker supports the same abbreviation identifiers as the regular abbreviation mechanism: typing an abbreviation like alpha will find the symbol α. The leader character (\) can optionally be included. Searching is also possible in reverse by typing or pasting a Unicode symbol to find the abbreviation identifiers that produce it.
The InfoView is the main interactive component of Lean. It can be used to inspect proof goals, expected types and diagnostics, as well as render arbitrary user interfaces called 'widgets' for Lean code.
When a Lean document is opened, the InfoView is automatically displayed next to the text document. It can always be toggled using the 'Infoview: Toggle Infoview' command or by using Ctrl+Shift+Enter (Cmd+Shift+Enter). To stop the InfoView from automatically opening, the 'Lean 4 > Infoview: Auto Open' setting can be disabled.
The InfoView can be moved into a seperate window for use on a second monitor by right-clicking the InfoView tab and clicking 'Move into New Window'.
The CSS style of the InfoView can be configured using the 'Lean 4 > Infoview: Style' setting.
The InfoView is subdivided into several sections, most of which are only displayed when the text cursor is positioned in a specific place:
- Tactic state. If the text cursor is positioned in a tactic proof, the InfoView will display the current proof state with all currently open proof goals at the position of the cursor. Each proof goal is identified by a name and clicking on the name will collapse the respective proof goal. Proof goal names can be hidden using the 'Lean 4 > Infoview: Show Goal Names' setting.
- Expected type. If the text cursor is positioned in a Lean term, the InfoView will display the current expected type at the position of the cursor.
- Widget sections. Widgets may add arbitrary additional sections to the InfoView that are only displayed when the respective widget is active.
- Messages. If the text cursor is positioned on a line of the span of a diagnostic, an interactive variant of the diagnostic is displayed. Disabling the 'Lean 4 > Infoview: All Errors On Line' option will only display errors that are to the right of the text cursor.
- All Messages. Always displayed. Contains interactive variants of all diagnostics present in the file, sorted by their proximity to the text cursor by default. The section header displays a tally of errors, warnings and informational messages separately. Can be paused by clicking the 'Pause 'All Messages'' button in the top right of the section. The sort order can be changed by clicking the 'Sort by message location' button, also in the top right of the section. The default sort order can be changed by setting the 'Lean 4 > Infoview: Message Order' option.
All sections can be collapsed by clicking on their title using the mouse, but the expected type and all messages sections can also be collapsed and uncollapsed using the 'Infoview: Toggle Expected Type' and 'Infoview: Toggle "All Messages"' commands, respectively. The expected type section can also be collapsed by default using the 'Lean 4: Infoview > Show Expected Type' setting.
Clicking on the 'Go to source location' button in the top right of any message in the InfoView will jump to the location in the code where the message was created.
Using the 'Lean 4 > Infoview: Debounce Time' setting, the InfoView can be made to update more or less quickly as the text cursor is moved around.
Disabling the 'Lean 4 > Infoview: Auto Open Shows Goal' setting will only display the 'All Messages' section when the InfoView is automatically opened.
 |
|---|
| InfoView with 'Tactic state', 'Messages' and 'All Messages' sections. |
Both the proof goals in the tactic state and the expected type display a list of assumptions and locally available identifiers in a <name> : <type> format. At the end of the list of assumptions, a ⊢ symbol indicates the proof goal or the expected type.
Inaccessible names, i.e. names that have been automatically generated and cannot be used in a Lean program, are marked with a tombstome symbol (✝) and greyed out.
When a proof goal changes as the result of a tactic operation, the corresponding part of the proof state that changes is highlighted using red or green depending on whether this part of the proof state is about to be removed or was just inserted.
In the top right of the tactic state and the expected type sections, there is a cog icon that provides settings for the given kind of state:
- Display target before assumptions. Displays the proof goal / expected type above the assumption list instead of at the bottom of it. The default of this setting can be flipped using the 'Lean 4 > Infoview: Reverse Tactic State' setting.
- Hide type assumptions. Removes types from the assumption list. The default of this setting can be flipped using the 'Lean 4 > Infoview: Hide Type Assumptions' setting.
- Hide instance assumptions. Removes instances from the assumption list. The default of this setting can be flipped using the 'Lean 4 > Infoview: Hide Instance Assumptions' setting.
- Hide inaccessible assumptions. Removes assumptions with inaccessible names from the assumption list. The default of this setting can be flipped using the 'Lean 4 > Infoview: Hide Inaccessible Assumptions' setting.
- Hide let-values. Removes the values of
letexpressions from the assumption list. The default of this setting can be flipped using the 'Lean 4 > Infoview: Hide Let Values' setting. - Hide goal names. Removes the name of each goal in the proof goal / expected type. The default of this setting can be flipped using the 'Lean 4 > Infoview: Hide Goal Names' setting.
- Emphasize first goal. Renders side goals with a smaller font size. The default of this setting can be flipped using the 'Lean 4 > Infoview: Emphasize First Goal' setting.
- Save current settings to default settings. Clicking this button if any of the settings above differ from their defaults will persist the current settings to the VS Code user settings.
All settings can also be accessed using the InfoView context menu.
In the very top right of the InfoView, there are two icon buttons:
- Pin. Takes the tactic state, expected type, messages and widget sections at the current cursor location and pins them to the top of the InfoView so that they are visible when inspecting the InfoView in other parts of the code. In pinned InfoView states, an additional Go to pinned location in file icon button can be used to navigate to the place in the code where the InfoView state was pinned and the 'Pin' button is replaced with an 'Unpin' button. Can also be called using the 'Infoview: Toggle Pin' command.
- Pause state. Freezes the tactic state, expected type, messages and widget sections. Can also be called using the 'Infoview: Toggle Updating' command. When frozen, the 'Pause state' button is replaced with a 'Unpause state' button and a 'Refresh paused state' button is also displayed.
All InfoView actions can also be accessed using the InfoView context menu.
Hovering over any non-local identifiers in the InfoView will open a hover popup panel that contains the type of the identifier, as well as the documentation for the identifier. This can be repeated recursively: Hovering over an identifier in the type displayed in the hover popup panel will also display the type and documentation of that identifier.
When clicking an identifier, its hover popup panel becomes pinned so that it remains open when moving the mouse away from the popup panel. This can be especially helpful when right-clicking to use the context menu inside of a hover popup panel.
InfoView hovers can be disabled using the 'Lean 4 > Infoview: Show Tooltip On Hover' setting, though clicking identifiers to open and pin the popup panel will still be possible even with this setting disabled.
 |
|---|
InfoView hover for Nat |
Right-clicking on any non-local identifier in the InfoView and selecting 'Go to Definition' will directly jump to the place in the code where the identifier was defined. Holding Ctrl (Cmd) and then clicking on the identifier will also directly jump to the place in the code where the identifier was defined.
 |
|---|
InfoView 'Go to Definition' on Nat |
User widgets allow for extending the InfoView with arbitrary interactive components. Widgets are typically registered to activate in certain contexts, for example when a tactic is called, and may provide additional functionality when holding Shift and clicking a subexpression in the InfoView to select it as an input to the widget, or by right-clicking on the subexpression and clicking the 'Select' entry.
For an example of a built-in widget, calling the simp? tactic in a proof will display a 'Suggestions' section in the InfoView with a link that executes a code action. The code action replaces the simp? tactic call with a simp only tactic invocation that lists all the theorems needed to simplify the expression.
When using Lean's math library, Mathlib, and importing Mathlib.Tactic.Widget.Conv, a conv? tactic can be called. Shift-clicking a subexpression in the proof goal will then generate a conv tactic invocation in place of conv? that focuses on that specific subexpression.
 |
|---|
simp? 'Try this' widget |
Some of the colors in the InfoView can be themed with a custom color theme or by configuring the 'Workbench: Color Customization' setting. The following components of the InfoView can be themed by setting one of the corresponding theme identifiers to the desired hex color code:
lean4.infoView.hypothesisName: Accessible hypothesis nameslean4.infoView.inaccessibleHypothesisName: Inaccessible hypothesis nameslean4.infoView.goalCount: Number of goalslean4.infoView.turnstile: Turnstile (⊢) that separates hypotheses from the goallean4.infoView.caseLabel: Case labels (e.g.case zero)
When a diagnostic message in the InfoView contains trace output (e.g. output produced by set_option trace.Meta.Tactic.simp true or other trace options), the InfoView displays a search icon in the header of that message. Clicking the search icon opens a search field at the top of the message. Typing a query and pressing Enter will search through the trace tree and display only the trace nodes that contain matches, with the matching text highlighted. This can be helpful for finding relevant entries in large trace outputs.
The search can be cleared by clicking the 'Collapse all' icon inside the search field. Clicking the search icon in the message header again will hide the search field entirely. The search can also be shown and hidden using the 'Show Search' and 'Hide Search' entries in the right-click context menu of a trace message.
When hovering over parts of the code with the mouse pointer, VS Code will display additional information for that piece of code in a popup panel. Specifically:
- Identifiers. When hovering over an identifier, VS Code will display the type of the identifier, the documentation of the identifier and which file it was imported from.
- Errors, warnings and information. When hovering over a piece of code that is underlined with a squiggly line, VS Code will display the error, warning or information associated with the squiggly line.
- Unicode symbols. When hovering over a unicode symbol, VS Code will provide all available abbreviation identifiers to input the symbol.
Automatic hovers can be disabled by un-ticking the 'Editor › Hover: Enabled' configuration option. This is especially helpful when presenting Lean 4 code to an audience.
Hovers can also be triggered at the current text cursor position using the keyboard with the Ctrl+K Ctrl+I (Cmd+K Cmd+I) chord or the 'Show or Focus Hover' command.
Moving the mouse away from the hover popup panel will immediately collapse it. Clicking on the hover popup panel will pin it so that it remains open when the mouse is moved away from the hover popup panel.
 |
|---|
| Pinned hover popup panel with error and identifier information |
Auto-completion is a mechanism that can be used to find identifiers that are available in the current context and to complete partial identifiers. The current context is determined by the current set of imports, as well as the set of available local declarations and variables. Auto-completion can always be triggered manually by using Ctrl+Space (Option+Esc) or the 'Trigger Suggest' command.
There are several different kinds of auto-completion in Lean 4:
- Dot completion. When typing a dot after a namespace (
Namespace.), after a term (x.or(x + 1).), after a pipe operator (|>.) or simply on its own (.), VS Code will display a complete list of identifiers that are available in the current context and that can be inserted after the dot. Specifically:- For namespaces, it will display all available sub-namespaces and identifiers that exist in the namespace (e.g.
Namespace.SubNamespaceorNamespace.someFunction). - For terms, it will display all available identifiers that exist in the namespace corresponding to the type of the term (e.g.
x.succforx : Nat). - On its own, it will display all available identifiers that exist in the namespace corresponding to the expected type at the position of the dot (e.g.
.zeroif the expected type isNat).
- For namespaces, it will display all available sub-namespaces and identifiers that exist in the namespace (e.g.
- Identifier completion. When typing an identifier and pausing for a moment, VS Code will display all identifiers that are available in the current context and match the identifier that has been typed so far. In most contexts, it is necessary to type at least the first character of the identifier for identifier completion to offer any options.
- Tactic completion. When pressing
Ctrl+Space(Option+Esc) in whitespace within a tactic proof, VS Code will display all available tactics along with their documentation. - Structure field completion. When pressing
Ctrl+Space(Option+Esc) inside{ }for a structure instance, VS Code will display the full list of fields that can be set for the structure. endname completion. When typing an identifier afterend, VS Code will display the available namespace and section names that can be closed.- Import completion. When triggering auto-completion at the very start of the file where the imports are denoted by pressing
Ctrl+Spaceor by typing the first characters of animportdeclaration, VS Code will display all files that can be imported. Since support for this feature by Lean's package manager Lake is still pending, in some Lean projects it will also display some files that are outside of the current Lean project and cannot actually be imported.
Next to the currently selected identifier in the completion menu, VS Code displays the type of the identifier and a small caret. Clicking this caret or hitting Ctrl+Space (Option+Esc) again will also display the documentation associated with the currently selected identifier. Deprecated declarations are shown with strikethrough text and include deprecation information in their documentation. Theorem completions are shown with a distinct icon to distinguish them from other kinds of declarations.
By default, VS Code will auto-complete the selected identifier when Enter or Tab are pressed. Since Enter is also used to move the cursor to a new line, some users find this behavior to be irritating. This behavior can be disabled by setting the 'Accept Suggestion On Enter' configuration option to 'off'.
Additionally, by default, VS Code will display so-called word auto-completions that are based on the text in all files that are currently open whenever Lean provides no auto-completions itself. Word auto-completions can be disabled by setting the 'Editor: Word Based Suggestions' configuration option to 'off'.
 |
|---|
Completion menu for dot completion on x : Nat |
Code actions are a mechanism for Lean to suggest changes to the code. When a code action is available at the current text cursor position, VS Code will display a light bulb icon. Clicking this icon or pressing Ctrl+. (Cmd+.) and then selecting one of the entries will apply the code action and make the suggested change to the code. In Lean, code actions can be defined in user code.
For example, the built-in #guard_msgs command can be used to test that a declaration produces a specific diagnostic, e.g. /-- info: 2 -/ #guard_msgs (info) in #eval 1 produces ❌️ Docstring on `#guard_msgs` does not match generated message: info: 1. When positioning the text cursor in the #guard_msgs line, a light bulb will pop up with an entry to replace the documentation above #guard_msgs with the actual output.
Similarly, when Lean displays an 'unknown identifier' error, code actions are provided to add an import that makes the given identifier available or to change the identifier to a similarly-named one from the environment. A source action is also available to import modules for all unambiguous unknown identifiers in the file at once.
The Batteries library also provides some additional useful code actions, for example:
- Typing
instance : <class> := _will offer to generate a skeleton to implement an instance for<class>. - Typing
def f : <type1> → <type2> := _will offer to generate a match on the value of<type1>. - Typing
induction xorcases xwill offer to generate the induction cases forx.
 |
|---|
Code action for #guard_msgs command |
When typing a function application, VS Code will automatically display a popup that designates the current remaining function type. This removes the need to remember the function signature while typing the function application, or having to constantly cycle between hovering over the function identifier and typing the application.
The signature help can be triggered by pressing Ctrl+Shift+Space (Cmd+Shift+Space) or by using the 'Trigger Parameter Hints' command.
Inlay hints are a mechanism for Lean to display greyed-out code snippets directly in the code to make some implicit information explicit. Lean will display inlay hints for implicit parameters that have been automatically inserted to make it more clear that these parameters have been added.
Hovering over an inlay hint for automatically-inserted implicit parameters will display a tooltip with the types of the parameters. Double-clicking the inlay hint will insert the greyed out snippet into the code.
 |
|---|
Inlay hint for automatically-inserted implicit parameter α |
Placing the text cursor on an identifier will highlight all occurrences of the identifier in the current file. For occurrence highlighting to work, the text cursor must be moved into the identifier from the left or by directly clicking into it, not from the right.
When placing the text cursor on a return statement in a do block, the do that the return belongs to will be highlighted.
 |
|---|
Occurrence highlighting on a parameter x. Usages of the second semantically distinct x that shadows the parameter x are not highlighted. |
By default, the Lean 4 VS Code extension will provide syntax highlighting for comments, built-in keywords, definition names, attributes, sorry, strings, numbers and booleans. However, due to the extensibility of Lean, the VS Code extension cannot provide syntax highlighting e.g. for user-defined keywords on its own. Because of this, Lean provides additional so-called semantic highlighting for Lean documents:
- Keywords. All keywords, including user-defined ones, are highlighted.
- Projections. Projection notation, e.g.
projinvalue.proj,(value + 1).projorvalue |>.proj, is highlighted. - Variables. Local variables, e.g.
xindef f (x : Nat) : Nat := x, are highlighted. - Function declarations. All function declaration names, e.g. the second occurrence of
gindef f : Nat := g 0 where g n := n, are highlighted.
Whether these different kinds of syntax and semantic highlighting are actually distinguishable in the editor depends on the color theme that is selected in the menu at 'File' > 'Preferences' > 'Theme' > 'Color Theme', which can also be opened by using the Ctrl+K Ctrl+T (Cmd+K Cmd+T) chord or the 'Preferences: Color Theme' command.
 |
|---|
| Semantic highlighting in a proof |
Using the 'Go to Symbol in Editor' command that can be called by pressing Ctrl+Shift+O (Cmd+Shift+O), all the declarations, namespaces and sections of the current Lean document can be displayed and navigated by typing in the name of the respective identifier, clicking or using the arrow keys. Typing : will group all declarations, all sections and all namespaces.
 |
|---|
| 'Go to symbol' panel with grouped declarations |
The document outline displays a brief overview of all the namespaces, sections and declarations of a Lean document. Clicking an entry will jump to the corresponding location in the code. It can be opened via 'View' > 'Open View' > 'Outline' or by using the 'Explorer: Focus on Outline View' command.
 |
|---|
| Document outline of a Lean 4 document |
When positioning the text cursor at any position in a Lean document, VS Code will display a 'breadcrumbs bar' at the top of the editor and just underneath the tab bar that display the full semantic location of the cursor. This includes the file path of the document, namespaces, sections and the declaration that the cursor is in.
Clicking on any entry of the breadcrumbs will display a list of all available alternatives at the given level of the location. For example, clicking on a declaration in a namespace will display all other declarations in that namespace in the same file. Selecting any of these entries will directly navigate to the selected piece of code or document.
The breadcrumbs bar can also be focused using Ctrl+Shift+; (Cmd+Shift+;) or the 'Focus Breadcrumbs' command and then navigated using the arrow keys and Enter.
 |
|---|
| Breadcrumbs bar with expanded namespace contents |
When hovering over the left column of a Lean document editor that contains the line numbers, VS Code will display a caret next to every namespace, section and declaration. Clicking this caret, using the Ctrl+K Ctrl+L (Cmd+K Cmd+L) chord or the 'Toggle Fold' command will collapse this part of the document. Clicking the caret again or using the same command as before will unfold this block of code again.
Similar to the document outline or the breadcrumbs bar, collapsible code blocks can be used to gain an overview over a Lean document and quickly navigate it, e.g. by using the 'Fold All' command or the Ctrl+K Ctrl+0 (Cmd+K Cmd+0) chord to collapse all code blocks and later using the 'Unfold All' command or the Ctrl+K Ctrl+J chord to unfold all code blocks again.
 |
|---|
| Lean 4 document with several folded code blocks |
When scrolling through a Lean document, at the top of the editor, VS Code will display source code lines corresponding to the surrounding namespaces, sections and declarations of the first line of code that is displayed in the editor. Clicking on one of these lines will immediately jump to the corresponding line in the source code.
Sticky scroll is also supported in the VS Code explorer and the VS Code terminal.
 |
|---|
| Sticky scroll of surrounding namespaces, sections and declaration at the top of the editor |
This section covers several essential tools to efficiently navigate Lean projects.
To jump to the place in the code where an identifier was defined, the 'Go to Definition' command can be used by positioning the text cursor on the identifier and pressing F12, by right clicking on the identifier and selecting 'Go to Definition' or by holding Shift and clicking on the identifier. When used on a type class projection or on a macro that produces a type class projection, 'Go to Definition' will provide several alternatives for both the type class itself, as well as its involved instances. For reducible definitions, 'Go to Definition' will also look through them to find the underlying declaration. 'Go to Definition' also works on import statements, jumping to the imported file.
The 'Go to Declaration' command that can be used via the context menu yields all alternatives provided by 'Go to Definition' in addition to the parser and elaborator of the given symbol.
The 'Go to Type Definition' command that can be used via the context menu jumps to the type of the identifier at the cursor position. For identifiers with compound types, it will show all constituent type constants.
 |
|---|
| Context menu when right-clicking on an identifier. Contains 'Go to Definition', 'Go to Declaration', 'Go to Type Definition', 'Find All References' and 'Show Call Hierarchy' entries. |
Using the 'Calls: Show Call Hierarchy' command by right clicking on an identifier and selecting 'Show Call Hierarchy' or by positioning the text cursor on the identifier and pressing Alt+Shift+H will display a list of all declarations that use this identifier in the entire Lean project. Clicking one of the carets next to a usage will also recursively display all usages of that usage. This makes it possible to quickly understand all the contexts that an identifier is used in. The call hierarchy can also be navigated using the arrow keys and Enter.
Clicking the phone icon button in the top right of the call hierarchy view or using the 'Calls: Show Outgoing Calls' command will instead switch the call hierarchy to display all the identifiers that are used in the declaration of a given identifier. This can be useful to quickly gain an overview for the different identifiers that a declaration depends on.
When going through a long list of usages and checking that a property holds for every single one of them, it can sometimes be helpful to delete individual entries from the usage list that have already been checked. This can be done by hovering over a call hierarchy entry and clicking the X icon button on the right side of the call hierarchy.
 |
|---|
| Call hierarchy view displaying all usages of an identifier |
 |
|---|
| Call hierarchy view displaying all identifiers used in the declaration of an identifier |
The 'References: Find All References' command can be called by right clicking on an identifier and selecting 'Find All References' or by positioning the text cursor on an identifier and pressing Alt+Shift+F12. It is similar to the 'Show Call Hierarchy' command, but organizes usages by files, not declarations, displays a short snippet of the code where the identifier is used and cannot walk through usages recursively.
 |
|---|
| 'Find references' view displaying all direct usages of an identifier |
Using the 'Go to Symbol in Workspace…' command that can be triggered using Ctrl+T (Cmd+T) or via Ctrl+P (Cmd+P) and then entering a # symbol will open a search panel. Typing identifiers into this search panel will perform a fuzzy search over all available identifiers in the current Lean project. Clicking an identifier or selecting one using the arrow keys and Enter will jump to the place in the code where the identifier was declared. Doing so is typically more efficient than using a plain-text search because it will not yield any false-positives.
 |
|---|
| Workspace symbol search |
The 'Search: Find in Files' command that can be triggered using Ctrl+Shift+F is useful when searching for portions of text in a Lean project. Typing a portion of text will display all matches in the project, grouped by the directory and file they occur in. Clicking on any entry will jump to the respective location in the code. To use this feature, the Lean project folder must first be opened in VS Code using the 'File: Open Folder…' command that can be accessed via 'File' > 'Open Folder' or using the Ctrl+K Ctrl+O (Cmd+K Cmd+O) chord.
Past search results can be accessed using the Up and Down arrow keys when the search input is focused.
There are several ways to refine the search in the form of icon buttons in the right of the search field:
- Match case. Limits the search results to case sensitive matches. For example,
wordwill not matchWordanymore. Can also be toggled using the 'Search Editor: Toggle Match Case' command orAlt+C. - Match whole world. Limits the search results to matches where the full word matches. For example,
wordwill not matchlargerwordanymore. Can also be toggled using the 'Search Editor: Toggle Match Whole Word' command orAlt+W. - Use regular expression. Instead of searching for a portion of text, search files using a regular expression. Can also be toggled using the 'Search Editor: Toggle Use Regular Expression' command or
Alt+R.
On the right below the search bar, there is an icon button with three dots. Clicking it will open two more text inputs that allow limiting the search to a set of files or excluding a set of files from the search. Clicking the book icon button in the 'Files to include' text input will additionally limit the search to only open files.
Search results can also be viewed in a more structured hierarchical view by clicking the fourth icon button in the top right of the search view that looks like a bunch of horizontal lines. This will display search results as they appear in the file structure of the project, making it easier to quickly collapse entire folders of search results that are not relevant.
Clicking the caret on the left of the text input will open the 'Replace' text field that can be used to replace all search results with another string. If the 'Use regular expressions' mode has been activated, capturing groups in the regex can be referred to using $1, $2, etc.
When going through a long list of search results, it can sometimes be helpful to delete individual entries from the search results that have already been checked. This can be done by hovering over a search result and clicking the 'X' icon button on the right side of the search view.
By clicking on the third icon button in the top right of the search view that contains the file icon or by using the 'Search Editor: New Seach Editor' command, an alternative search view is opened where search results are displayed directly in a text editor. Clicking in the text editor will navigate to the respective location in the code.
 |
|---|
| Search view with enabled hierarchical tree display option |
In a Lean file, pressing Alt+Shift+M to execute the 'Module Hierarchy: Show Imports' command will display a tree with the Lean module for the current file at its root and its imports as children of the root. The full import tree can be navigated using this view. Pressing Alt+Shift+N to execute the 'Module Hierarchy: Show Inverse Module Hierarchy' will instead display a tree with the Lean module for the current file at its root and all files where it is imported as children of the root. The full inverted import tree can be navigated using this view.
For Lean modules that use the module keyword, the module hierarchy will also display the various import modifiers that can be used together with the module keyword.
Clicking the 'Show Imports' or 'Show Imported By' buttons in the top right of the module hierarchy view will switch between the regular and the inverse module hierarchy. The state of the displayed hierarchy can be refreshed using the 'Refresh' icon and the entire tree can be collapsed using the 'Collapse All' icon.
 |
|---|
Module hierarchy showing the imports of a module Main |
The 'Copy Module Name' command copies the Lean module name of the current file to the clipboard. For example, a file at Mathlib/Tactic/Ring.lean would yield Mathlib.Tactic.Ring. This command is available in the command palette and in the right-click context menu of editor tabs for Lean files.
Using the 'Go to File' command by pressing Ctrl+P (Cmd+P) brings up a search prompt that allows for typing in a file name to open and focus. It can be used to quickly navigate files using the keyboard.
To use this feature, the Lean project folder must first be opened in VS Code using the 'File: Open Folder…' command that can be accessed via 'File' > 'Open Folder…' or using the Ctrl+K Ctrl+O (Cmd+K Cmd+O) chord.
 |
|---|
| 'Go to file' panel with a search for file names containing 'K' |
VS Code has a built-in file explorer that can be opened using the 'View: Show Explorer' command or Ctrl+Shift+E (Cmd+Shift+E). It can be navigated using the mouse, arrow keys and Enter or by typing in the name of the file or folder to jump to. Using the context menu that can be opened by right-clicking, the built-in file explorer also supports several basic file operations, like creating, deleting, copying or renaming files with their standard keyboard shortcuts.
By default, VS Code will always focus the file in the explorer for which an editor is currently being focused. This means that over time, VS Code will keep expanding folders. To re-gain a top-down hierarchical perspective of the file tree and collapse all folders, the fourth icon button in the top right of the explorer view can be pressed to call the 'Collapse Folders in Explorer' command.
Selecting two files by holding Ctrl (Cmd) and then clicking them presents a 'Compare Selected' entry in the context menu when right-clicking any of the files. This will open a diff-view displaying changes between the two files.
 |
|---|
| VS Code file explorer |
This section describes how to manage Lean projects using the Lean 4 VS Code extension. All of these commands provide a frontend for Lean's package manager Lake.
There are two project creation commands that can be accessed using the command palette or by navigating to the 'New Project…' submenu in the command menu:
- 'Project: Create Standalone Project…'. This command will create a new Lean 4 project with the name specified in the folder creation dialog and without any additional dependencies. It will use the
leanprover/lean4:stableLean release channel for the Lean version of the project, initialize a Git repository and create an initial commit with all the files in the fresh project. - 'Project: Create Project Using Mathlib…'. This command will create a new Lean 4 project with the name specified in the folder creation dialog that depends on Lean's math library, Mathlib. It will use Mathlib's Lean version for the project, download and install the current Mathlib build artifact cache, initialize a Git repository and create an initial commit with all the files in the fresh project.
There are two commands to open existing Lean projects that can be accessed using the command palette or by navigating to the 'Open Project…' submenu in the command menu:
- 'Project: Open Local Project…'. This command will open a Lean 4 project in the folder specified by a folder selection dialog. This command is mostly identical to VS Code's own 'Open Folder…' command, but will also immediately ensure that the opened folder is actually a Lean 4 project.
- 'Project: Download Project…'. This command will download a Lean 4 project from a given URL into the folder specified by a folder creation dialog. If the downloaded project is Lean's math library Mathlib or depends on it, it will also download and install the current Mathlib build artifact cache.
The Lean 4 VS Code extension supports the following commands that can be run in existing Lean projects and that can be accessed using the command palette or by navigating to the 'Project Actions…' submenu in the command menu:
- 'Project: Build Project'. Builds the full Lean project. If the project is Lean's math library Mathlib or depends on it, it will also download and install the current Mathlib build artifact cache before trying to build the project.
- 'Project: Clean Project'. Removes all build artifacts for the Lean project. If the project is Mathlib or depends on it, it will also offer to download and install the current Mathlib build artifact cache after cleaning the project.
- 'Project: Update Dependency…'. Displays a list of all dependencies that can be updated. After selecting a dependency and updating it, if the project is Mathlib or depends on it, it will also download and install the current Mathlib build artifact cache. At the end, if the Lean version of the updated project differs from the Lean version of the project, the command will offer to update the Lean version of the project to that of the updated dependency.
- 'Project: Fetch Mathlib Build Cache'. Downloads and installs the current Mathlib build artifact cache if the project is Mathlib or depends on it.
- 'Project: Fetch Mathlib Build Cache For Open Files'. Downloads and installs the current Mathlib build artifacts for selected open files and all of their imports if the project is Mathlib or depends on it.
- 'Project: Fetch Mathlib Build Cache For All Open Files'. Downloads and installs the current Mathlib build artifacts for all open files and all of their imports if the project is Mathlib or depends on it.
- 'Project: Fetch Mathlib Build Cache For Current File'. Downloads and installs the current Mathlib build artifacts for the current file and all of its imports if the project is Mathlib or depends on it.
- 'Project: Select Project Lean Version…'. Displays a list of all available Lean versions. After selecting a Lean version, the command writes the selected Lean version to the
lean-toolchainfile of the given project.
 |
|---|
| 'Project: Update Dependency…' selection dialog |
 |
|---|
| 'Project: Select Project Lean Version…' selection dialog |
When editing a lakefile.toml file, the Lean 4 VS Code extension provides schema validation, auto-completion and hover documentation for all Lake package configuration options. This is powered by the Even Better TOML extension, which is automatically installed as a dependency of the Lean 4 VS Code extension.
If the commands provided by the Lean 4 VS Code extension are not sufficient to manage the Lean project, then a built-in VS Code terminal can be launched by calling the 'Terminal: Create New Terminal' command or by pressing Ctrl+Shift+` (Cmd+Shift+`). In this terminal, all Lake commands can be executed.
 |
|---|
| VS Code terminal view |
This section covers how to manage different Lean versions. All of these commands provide a frontend for Lean's version manager Elan and can be found using the command palette or by navigating to the 'Version Management…' submenu in the command menu.
Elan is Lean's version manager. It automatically installs Lean versions when a Lean command like lean or lake is used depending on the current working directory of the command.
When used inside of a Lean project with a lean-toolchain file, Elan will use the Lean version denoted in the lean-toolchain file. Outside of a Lean project, Elan will use the default Lean version that can be configured using the elan default <version> command.
Lean versions can either be specific Lean versions, like leanprover/lean4:v4.14.0, or release channels, like leanprover/lean4:stable, which is Elan's default Lean version when Elan is first installed. Elan's release channels resolve to the most recent specific Lean version in a given release channel.
Before Elan 4.0.0, release channels were explicitly installed in Elan, would resolve to the most recent version at the point of installation and could be manually updated to the most recent version in the release channel using the elan toolchain update <release channel> command.
Since Elan 4.0.0, release channels cannot be installed anymore, but whenever they are used anywhere, e.g. when running lean with a default Lean version of leanprover/lean4:stable, they will automatically resolve to the most recent Lean version for that release channel. This means that since Elan 4.0.0, release channels are updated on-the-go and do not need to be kept up-to-date manually. When Elan cannot resolve a release channel, e.g. because the machine it runs on has no network connection, it will attempt to fall back to the last installed Lean version of that release channel.
Before Elan 4.0.0, the Lean 4 VS Code extension would always automatically install missing Lean versions as it encountered them by using Elan in exactly the same way as it works on the command line. Since Elan 4.0.0, the Lean 4 VS Code extension now has a 'Lean 4: Always Ask Before Installing Lean Versions' setting that can be enabled to issue a confirmation prompt every time before a Lean version is installed by Elan. Additionally, regardless of this setting, the Lean 4 VS Code extension will always issue a confirmation prompt when opening a Lean file that is using a release channel for its version if there is a new Lean version for the release channel available.
Elan's default Lean version can be selected using the 'Setup: Select Default Lean Version…' command. The command queries all installed Lean version and fetches all available Lean versions from https://release.lean-lang.org/ to present them in a selection dialog.
 |
|---|
| 'Setup: Select Default Lean Version…' selection dialog |
The newest versions of the leanprover/lean4:stable and leanprover/lean4:nightly release channels can be installed manually using the 'Setup: Update Release Channel Lean Version…' command. The command uses Elan to resolve leanprover/lean4:stable and leanprover/lean4:nightly to determine their most recent versions and displays them in a selection dialog if an update for the respective Lean release channel is available.
 |
|---|
| 'Setup: Update Release Channel Lean Version…' selection dialog |
Installed Lean versions can be uninstalled using the 'Setup: Uninstall Lean Versions…' command. The command determines all unused Lean versions using Elan's Lean version garbage collector and displays a selection dialog for uninstalling all unused Lean versions, as well as additional individual Lean versions and the projects they are used in.
 |
|---|
| 'Setup: Uninstall Lean Versions……' selection dialog |
Elan can be installed using the 'Setup: Install Elan' command. Similarly, the 'Setup: Update Elan' command can be used to update Elan to the newest version and the 'Setup: Uninstall Elan' command can be used to remove Elan and all installed Lean versions from the machine.
After installing Elan or updating it from a pre-4.0.0 version, the Lean 4 VS Code extension will also prompt users about whether they want to set the 'Lean 4: Always Ask Before Installing Lean Versions' setting.
This section covers how to find definitions and theorems in key Lean libraries like Mathlib using the Lean 4 VS Code extension.
Loogle, a search engine for definitions and theorems in Lean's standard library and a recent version of Mathlib, can be accessed from within VS Code using the 'Loogle: Search' command. It can be called using the Ctrl+K Ctrl+S (Cmd+K Cmd+S) chord, from the right click context menu in a Lean file, using the command palette or directly from the command menu. The LoogleView can always be closed using Escape.
When selecting text in a text editor before calling 'Loogle: Search', Loogle will immediately search for the selected text. The input field supports the same Unicode input as the text editor when editing Lean files. Clicking the magnifier icon or pressing Enter will search for the given query. Clicking the arrow icons or using the up and down arrow keys will cycle through past queries. The query syntax supported by Loogle is described in the LoogleView itself.
When querying Loogle, it will display either a list of results or a list of possible suggestions if no results were found. The LoogleView will only display the first 200 results matching the query. Each result displays the name of the identifier, the module where it is located and the type of the identifier. Clicking the identifier will launch a browser window in VS Code with the documentation for the given identifier. Clicking a suggestion provided by Loogle if no results were found will immediately issue a query with the given suggestion.
 |
|---|
| LoogleView |
This section covers several tools that can help diagnose issues with a Lean setup, the Lean 4 VS Code extension and Lean itself.
The Lean 4 VS Code extension checks that the user's Lean setup is well-founded before starting Lean. There are two separate kinds of setup diagnostics: Global- and project-level diagnostics.
- Global-level diagnostics are checked when the first Lean file is opened. If there is an error-level setup issue, none of the Lean-specific Lean 4 VS Code extension features are activated. The following global-level aspects of the user's setup are checked:
- Whether Curl and Git are installed (Error)
- Whether some version of Lean can be found (Error)
- Whether Lean's version manager Elan is installed and reasonably up-to-date (Warning)
- Whether the operating system version is recent enough to run current Lean versions (Warning)
- Whether VS Code is sufficiently up-to-date to auto-update the Lean 4 VS Code extension to the next version (Warning)
- Project-level diagnostics are checked whenever the first Lean file of a project is opened. If there is an error-level setup issue, Lean will not launch for that project, but all of the other Lean-specific extension features will be active, provided that the global-level diagnostics did not yield an error. The following project-level aspects of the user's setup are checked:
- Whether Lean is being ran in an untitled file that has not been saved to the file system (Warning)
- Whether a lean-toolchain file can be found in the project associated with the file (Warning)
- Whether some version of Lean can be found (Error)
- Whether the project associated with the file is a Lean 3 project (Error)
- Whether the project associated with the file is using a Lean version from before the first Lean 4 stable release (Warning)
- Whether some version of Lean's package manager Lake can be found (Error)
If there is a global-level setup diagnostic error, pressing the 'Retry' button of the notification in the bottom right corner will attempt to restart the extension and retry the setup check. For project-level setup diagnostic errors, switching to a different file tab and switching back is sufficient to re-check the setup.
All setup warnings can be disabled using the 'Lean 4: Show Setup Warnings' setting.
Executing the 'Troubleshooting: Show Setup Information' command from the command palette or the command menu will collect information about the user's setup in the context of the last focused Lean 4 file and display it. It includes the following information:
- Operating system
- CPU architecture
- CPU model
- Total available RAM
- VS Code version
- Lean 4 VS Code extension version
- Whether Curl is installed
- Whether Git is installed
- Whether Lean's version manager Elan is installed and reasonably up-to-date, as well as the Elan version
- Whether Lean is installed and reasonably up-to-date, as well as the Lean version
- Whether a Lean project with a lean-toolchain has been opened, as well as the path to the project
- Available Elan Lean versions
The output is formatted using Markdown and will produce a nicely rendered output when copied to a Markdown-supporting tool, e.g. the Lean Zulip.
 |
|---|
| Setup information output |
When Lean produces errors while interacting with a file or when an external command is executed, these errors and all external command output are displayed in the 'Lean: Editor' output view, which can be helpful to diagnose issues. It can be opened using the 'Troubleshooting: Show Output' command from the command palette or the command menu.
 |
|---|
| 'Lean: Editor' output view |
When an issue occurs while interacting with Lean and it seems like interacting with Lean is seriously broken, e.g. because a bug occured in Lean, it can always be fully restarted by using the 'Server: Restart Server' command from the command palette or the command menu. If a bug with the Lean 4 VS Code extension occurs instead, then restarting VS Code may help.