This extension adds support for Lean.

We currently support a variety of features.

• 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
• Unicode input support
• Info view window to show goal and error messages ("Lean: Open Info View")
• Batch file execution
• Search for declarations in open files (ctrl+p #)
• Region of interest checking (i.e. control over how much of the project we check)
• Fill in {! !} holes using ctrl+.
• Tasks for leanpkg (ctrl+p task configure)

This extension requires an installation of Lean.

On Windows, 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 windows-key + 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:

• lean.executablePath: controls which Lean executable is used when starting the server
• lean.timeLimit: controls the -T flag passed to the Lean executable
• lean.memoryLimit: controls the -M flag passed to the Lean executable
• lean.roiModeDefault: controls the default region of interest, the options are:
  • nothing: check nothing
  • visible: check only visible files
  • open: check all open files
  • project: check the entire project's files

• Fonts with good unicode support (on Linux): "editor.fontFamily": "Source Code Pro Medium, DejaVu Sans Mono"
• By default, vscode will complete then to has_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.

• Install npm (and for Ubuntu 17.04 nodejs-legacy)
• Install code from http://code.visualstudio.com
• Run git clone https://github.com/leanprover/vscode-lean
• Run npm install in the vscode-lean directory
• Open the vscode-lean in vscode and start developing (F5 starts the debugger)

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