Name: vscode-lean
Owner: Lean
Description: An extension for VS Code which provides support for the Lean language.
Created: 2016-12-19 20:21:34.0
Updated: 2017-10-06 22:32:22.0
Pushed: 2017-11-21 00:02:16.0
Homepage: null
Size: 219
Language: TypeScript
GitHub Committers
User | Most Recent Commit | # Commits |
---|
Other Committers
User | Most Recent Commit | # Commits |
---|
This extension adds support for Lean.
We currently support a variety of features.
{! !}
holes using ctrl+.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 serverlean.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"editor.fontFamily": "Source Code Pro Medium, DejaVu Sans Mono"
then
to has_bind.and_then
when you press enter. To disable this behavior, set "editor.acceptSuggestionOnEnter": false
npm
(and for Ubuntu 17.04 nodejs-legacy
)code
from http://code.visualstudio.comgit clone https://github.com/leanprover/vscode-lean
npm install
in the vscode-lean
directoryvscode-lean
in vscode and start developing (F5 starts the debugger)lean.extraOptions
)#
.semver
for detecting and comparing versions.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:
Add basic integration with the Lean server.
Initial release of the package.
Please report issues on Github.