Search results

RFC: Split into multiple extensions; use extension pack to bundle

RFCRequest for commentsRequest for comments

Status: Open.

#790 In leanprover/vscode-lean4;

· siegebell opened on Jun 23, 2026

Remove unmaintained "Even Better TOML" dependency

bugSomething isn't workingSomething isn't working

Status: Open.

#787 In leanprover/vscode-lean4;

· briansmith opened on Jun 18, 2026

Overzealous caching of tactic state

bugSomething isn't workingSomething isn't working

Status: Open.

#785 In leanprover/vscode-lean4;

· Vtec234 opened on Jun 10, 2026

RFC: Have 'restart file' button show how many files would be rebuilt

RFCRequest for commentsRequest for comments

Status: Open.

#771 In leanprover/vscode-lean4;

· Vtec234 opened on Apr 20, 2026

Unicode file paths displayed as URI-encoded in the infoview

bugSomething isn't workingSomething isn't working

Status: Open.

#759 In leanprover/vscode-lean4;

· kuotsanhsu opened on Apr 12, 2026

Display target before assumptions not always respected

bugSomething isn't workingSomething isn't working

Status: Open.

#734 In leanprover/vscode-lean4;

· MoritzBeroRoos opened on Mar 9, 2026

RFC: Automatic file reloading when dependencies change

RFCRequest for commentsRequest for comments

Status: Open.

#693 In leanprover/vscode-lean4;

· hgoldstein95 opened on Nov 26, 2025

Rename symbol dialog does not do unicode input translation

bugSomething isn't workingSomething isn't working

Status: Open.

#690 In leanprover/vscode-lean4;

· kuruczgy opened on Nov 9, 2025

RFC: collapsing hyps in infoview

RFCRequest for commentsRequest for comments

Status: Open.

#652 In leanprover/vscode-lean4;

· vzaliva opened on Aug 20, 2025

RFC: Command-clickable file links in the InfoView

RFCRequest for commentsRequest for comments

Status: Open.

#631 In leanprover/vscode-lean4;

· BoltonBailey opened on Jul 10, 2025

RFC: Presentation / Demo mode

RFCRequest for commentsRequest for comments

Status: Open.

#627 In leanprover/vscode-lean4;

· ejgallego opened on Jun 13, 2025

RFC: Streamlined Entry of LaTeX Math Blocks in Markdown

RFCRequest for commentsRequest for comments

Status: Open.

#626 In leanprover/vscode-lean4;

· hansonchar opened on Jun 12, 2025