vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard

Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language.

Results 73 vscode-lean issues
Sort by recently updated
recently updated
newest added

I've been working through mathematics in lean and I've found on the same page multiple incomplete proofs that I just didn't notice. As it stands it puts a red squiggly...

This works fine: ``` /- ~~ -/ def x := 1 ``` Add one more tilde and important stuff breaks. ``` /- ~~~ -/ def x := 1 -- code...

I'm having some trouble setting up: I got the error "Unable to start the Lean server process: `Error: spawn lean ENOENT --- The lean.executablePath "lean" may be incorrect, make sure...

I am using distribution manjaro linux. vscode https://aur.archlinux.org/packages/visual-studio-code-bin lean 4 plugin. I get the following error when trying to get the result of interpreting the proof on lean: `Waiting for...

Bumps [markdown-it](https://github.com/markdown-it/markdown-it), [ovsx](https://github.com/eclipse/openvsx/tree/HEAD/cli) and [vsce](https://github.com/Microsoft/vsce). These dependencies needed to be updated together. Updates `markdown-it` from 10.0.0 to 12.3.2 Changelog Sourced from markdown-it's changelog. [12.3.2] - 2022-01-08 Security Fix possible ReDOS...

dependencies

Bumps [underscore](https://github.com/jashkenas/underscore) to 1.13.1 and updates ancestor dependency [ovsx](https://github.com/eclipse/openvsx/tree/HEAD/cli). These dependencies need to be updated together. Updates `underscore` from 1.8.3 to 1.13.1 Commits 943977e Merge branch 'umd-alias', tag 1.13.1 release...

dependencies

Bumps [terser](https://github.com/terser/terser) from 5.7.0 to 5.16.3. Changelog Sourced from terser's changelog. v5.16.3 Ensure function definitions, don't assume the values of variables defined after them. v5.16.2 Fix sourcemaps with non-ascii characters...

dependencies

Bumps [minimist](https://github.com/minimistjs/minimist) from 1.2.5 to 1.2.8. Changelog Sourced from minimist's changelog. v1.2.8 - 2023-02-09 Merged [Fix] Fix long option followed by single dash [#17](https://github.com/minimistjs/minimist/issues/17) [Tests] Remove duplicate test [#12](https://github.com/minimistjs/minimist/issues/12) [Fix]...

dependencies

Bumps [nth-check](https://github.com/fb55/nth-check) from 2.0.0 to 2.1.1. Release notes Sourced from nth-check's releases. v2.1.1 The ESM code had some issues that are now fixed aeeb067 https://github.com/fb55/nth-check/compare/v2.1.0...v2.1.1 v2.1.0 What's Changed nth-check is...

dependencies

Bumps [follow-redirects](https://github.com/follow-redirects/follow-redirects) from 1.14.1 to 1.15.2. Commits 9655237 Release version 1.15.2 of the npm package. 6e2b86d Default to localhost if no host given. 449e895 Throw invalid URL error on relative...

dependencies