This extension adds support for Lean.
We currently support a variety of features.
- Automatic installation of Lean via elan
- Incremental compilation and checking via the Lean server
- Hover shows documentation, types, and Unicode input help
- Auto-completion based on context and type via the Lean server
- Error messages / diagnostics
- Customizable Unicode input support (e.g. type
\la
tab to inputλ
) - Info view window to show goal, tactic state, and error messages:
- Batch file execution
- Search for declarations in open files (ctrl p
#
) - Region of interest checking (i.e. control how much of the project is checked automatically by Lean)
- Fill in
{! !}
holes with the code actions menu (ctrl .) - Tasks for
leanpkg
(ctrl shift p and select "Tasks: Configure Task") - Tactic state filtering with regex
- Type of the term under the cursor can be displayed in the status bar
- 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 .)
This extension requires an installation of Lean. As of version 0.12.1, the extension can install Lean for you using elan. See the mathlib installation docs for alternative instructions.
On Windows, if you installed Lean using MSYS2, you need to add both C:\msys64\mingw64\bin
(or wherever you installed MSYS2) and C:\projects\lean\bin
(or wherever you installed Lean) to the system PATH
environment variable. To do this, press Win Pause > go to Advanced System Settings > go to Environment variables. Under system variables (not user variables) find the Path
variable, and add these two folders.
This extension contributes the following settings (for a complete list, open the VS Code Settings and scroll to "Lean configuration"):
lean.executablePath
: controls which Lean executable is used when starting the server. If you are bundling Lean andvscode-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 tolean
in the same folder as the VS Code executable / application.lean.leanpkgPath
: controls which leanpkg executable is used forleanpkg
task integration. The%extensionPath%
token can be used here as well.lean.timeLimit
: controls the-T
flag passed to the Lean executablelean.memoryLimit
: controls the-M
flag passed to the Lean executablelean.roiModeDefault
: controls the default region of interest, the options are:nothing
: check nothingvisible
: check only visible filesopen
: check all open filesproject
: check the entire project's files
lean.input.leader
: character to type to trigger Unicode input mode (\
by default)lean.input.languages
: allows the Unicode input functionality to be used in other languageslean.input.customTranslations
: add additional input Unicode translations. Example:{"foo": "☺"}
will correct\foo
to☺
(assuming thelean.input.leader
has its default value\
).lean.infoViewAutoOpen
: controls whether the info view is automatically displayed when the Lean extension is activated (true
by default).lean.infoViewTacticStateFilters
: An array of objects containing regular expression strings that can be used to filter (positively or negatively) the tactic state in the info view. Set to an empty array[]
to hide the filter select dropdown. Each object must contain the following keys:regex
is a properly-escaped regex string,match
is a boolean, wheretrue
(false
) means blocks in the tactic state matchingregex
will be included (excluded) in the info view,flags
are additional flags passed to the JavaScript RegExp constructor.- The
name
key is optional and may contain a string that is displayed in the dropdown instead of the full regex details.
lean.infoViewFilterIndex
: index of the filter applied to the tactic state (in the arraylean.infoViewTacticStateFilters
). An index of -1 means no filter is applied.lean.typeInStatusBar
: controls whether the type of the term under the cursor is displayed as a status bar item (true
by default).lean.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.
It also contributes the following commands, which can be bound to keys if desired:
lean.input.convert
: converts the current Unicode abbreviation (bound to tab by default)lean.infoView.displayGoal
: show the tactic state and any messages (e.g. info, warning, error) at the current position in the info view window (bound to ctrl shift enter by default)lean.infoView.displayList
: show all messages for the current file from Lean in the info view window (bound to ctrl shift alt enter by default)lean.infoView.copyToComment
: copy the current contents of the info view into a new comment on the next line (same as clicking on the icon)lean.infoView.toggleStickyPosition
: enable / disable "sticky" mode. On enable this places a marker at the current position, and the goal will continue to be reported from this position even as the cursor moves and edits are made to the file. Disabling the mode goes back to tracking the cursor. (same as clicking on the icon)lean.infoView.toggleUpdating
: pause / continue live updates of the info view (same as clicking on the and icons)lean.roiMode.select
: select the region of interest (files to be checked by the Lean server)lean.batchExecute
: execute the current file using Lean (bound to ctrl shift r by default)lean.pasteTacticSuggestion
: if any tactic suggestions (i.e. tactics which return a "Try this:" in their output) are active for the code under the cursor, apply the first suggested edit. (bound to alt v by defaullt)
- Fonts with good Unicode support:
"editor.fontFamily": "Source Code Pro Medium, DejaVu Sans Mono"
. Note that for this configuration to work properly, both fonts must be specified in this order (so that characters that are not available in Source Code Pro are rendered using DejaVu Sans Mono). - By default, VS Code will complete
then
tohas_bind.and_then
when you press enter. To disable this behavior, set"editor.acceptSuggestionOnEnter": false
- If you like colored brackets, try out Bracket Pair Colorizer 2.
- Install
npm
(and for Ubuntu 17.04nodejs-legacy
) - Install
code
from http://code.visualstudio.com - Run
git clone https://github.com/leanprover/vscode-lean
- Run
npm install
in thevscode-lean
directory - Install the ESLint extension for vscode
- Open the
vscode-lean
directory in VS Code and start developing (F5 starts the debugger)
- "sticky" mode for the infoview position
- Command to apply tactic suggestions such as from
library_search
(using alt v or clicking "Try this:" in the info view)
- Show type of term under cursor in status bar
- Info view opens automatically
- Dropdown to filter tactic states
- Dropped support for Lean versions older than 3.1.0.
- Automated
elan
installation
- Tactic state highlighting
- Support for
visibleRanges
API in vscode. Per default, only the currently visible lines and the rest of the file above are checked.
- Updated syntax highlighting.
- New configuration option for extra command-line arguments. (
lean.extraOptions
) - Integration with
leanpkg
.
- Extremely improved info view (ctrl shift enter)
- Only show commands acting on Lean files when a Lean file is open in the current editor
- Hole support
- Info view showing the current goal and error messages.
- Search command (ctrl p
#
) - Improved Unicode input.
- New input mode for Unicode symbols.
- Internally uses new client library to interact with the Lean server.
- Fixes issue with highlighting commands beginning with
#
.
- Support for controlling the "region of interest", i.e. which files are considered by the Lean server for checking and recompilation.
- Miscellaneous improvements to the grammar, and syntax highlighting
- Initial support for recording Lean server errors, and an option for displaying them upon crash.
- Support for more bracket pairs including many Unicode options.
- Properly set working directory when executing in batch mode.
- Configuration for controlling default region of interest.
- Use
semver
for detecting and comparing versions. - Fix issue where diagnostics were not cleared on server restart.
Add support for detecting Lean server versions.
Add support for time and memory limits.
Consider angle brackets and parenthesis when completing Unicode symbols.
Bug fixes, stability, and a handful of feature improvements
Implement many features implemented by the EMACS mode. We now support:
- Hovering over names for type information
- Go-to-definition & peeking for constants
- Goal support, with the ability to display the goal at the current position.
- Basic auto-completion support
- Diagnostics support, displaying errors, information & warnings.
Add basic integration with the Lean server.
Initial release of the package.
Please report issues on Github.