vscode-lean4

vscode-lean4 copied to clipboard

The project setup currently downloads the entire repository history of mathlib, consisting of 24 thousand commits. This requires an additional 388 megabytes of disk space. Passing `--depth=1` to git performs...

BalaM314

The less-than sign followed by a non-space character causes a comment to render incorrectly

1

### Description See the code: ```lean /-

ShreckYe

When InfoView has many hypotheses, users have to scroll a lot to examine them. In particular some hypothesis are multil-line taking a lot of screen space. It would be nice...

vzaliva

### Proposal In the InfoView, when I get an error like `error: ././././Foo/Bar.lean:13:37: application type mismatch` or ``` `/Users/boltonbailey/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lake setup-file /Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/Mathlib/Logic/IsEmpty.lean Init Mathlib.Logic.Function.Basic Mathlib.Logic.Relator` failed: ``` I would like to...

BoltonBailey

RFC: Streamlined Entry of LaTeX Math Blocks in Markdown

1

### Proposal This proposal suggests improving the Lean authoring experience by supporting a convenient way to wrap selected Markdown content as a $LaTeX$ math block—e.g., by allowing users to select...

hansonchar

RFC: Presentation / Demo mode

6

### Proposal Provide a "Presentation / Demo" mode that would toggle on / off some useful options for using `vscode-lean4` when doing talks, demos, or congress presentations. - **User Experience**:...

ejgallego

Please verify domain in the vscode marketplace

6

To establish more trust and distinguish from other extensions. See this guide: https://code.visualstudio.com/api/working-with-extensions/publishing-extension

solomatov

Add `$` to surroundingPairs configuration

2

## Motivation VS Code currently has a helpful behavior where, if a block of text is selected and the user presses the backtick ("`"), the selected text is wrapped in...

hansonchar

pinned InfoView not updated

1

### Description I have observed that a pinned InfoView (whether Expected Type or Goal states) does not update as I change the code around it. ### Steps to Reproduce Did...

nomeata