Issues

• Completion popup reopens after Esc in Lean files; caused by default quickSuggestionsDelay of 200

  bug
  leanprover/vscode-lean4#800 · Filter by author Calmadeas opened on Sep 17, 2026
  1

• The "Rename Symbol" code action fails to account for constructor/destructor tags

  bug
  leanprover/vscode-lean4#799 · Filter by author omentic opened on Sep 15, 2026

• install leanprover/lean4 again and again

  leanprover/vscode-lean4#796 · Filter by author wieniawski-lai opened on Aug 19, 2026
  9

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

  RFC
  leanprover/vscode-lean4#790 · Filter by author siegebell opened on Jun 23, 2026
  1

• Remove unmaintained "Even Better TOML" dependency

  bug
  leanprover/vscode-lean4#787 · Filter by author briansmith opened on Jun 18, 2026
  5

• Overzealous caching of tactic state

  bug
  leanprover/vscode-lean4#785 · Filter by author Vtec234 opened on Jun 10, 2026
  1

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

  RFC
  leanprover/vscode-lean4#771 · Filter by author Vtec234 opened on Apr 20, 2026

• Unicode file paths displayed as URI-encoded in the infoview

  bug
  leanprover/vscode-lean4#759 · Filter by author kuotsanhsu opened on Apr 12, 2026

• Display target before assumptions not always respected

  bug
  leanprover/vscode-lean4#734 · Filter by author MoritzBeroRoos opened on Mar 9, 2026
  1

• RFC: Automatic file reloading when dependencies change

  RFC
  leanprover/vscode-lean4#693 · Filter by author hgoldstein95 opened on Nov 26, 2025
  5

• Rename symbol dialog does not do unicode input translation

  bug
  leanprover/vscode-lean4#690 · Filter by author kuruczgy opened on Nov 9, 2025
  1

• RFC: collapsing hyps in infoview

  RFC
  leanprover/vscode-lean4#652 · Filter by author vzaliva opened on Aug 20, 2025

• RFC: Command-clickable file links in the InfoView

  RFC
  leanprover/vscode-lean4#631 · Filter by author BoltonBailey opened on Jul 10, 2025

• RFC: Presentation / Demo mode

  RFC
  leanprover/vscode-lean4#627 · Filter by author ejgallego opened on Jun 13, 2025
  6

• RFC: Streamlined Entry of LaTeX Math Blocks in Markdown

  RFC
  leanprover/vscode-lean4#626 · Filter by author hansonchar opened on Jun 12, 2025
  1

• Please verify domain in the vscode marketplace

  leanprover/vscode-lean4#617 · Filter by author solomatov opened on May 29, 2025
  6

• pinned InfoView not updated

  bug
  leanprover/vscode-lean4#616 · Filter by author nomeata opened on Apr 29, 2025
  1

• Setup Guide should say something about running resulting executables

  leanprover/vscode-lean4#598 · Filter by author Kha opened on Apr 1, 2025
  1

• Working with lean/git installed in WSLv1 or WSLv2 instance

  leanprover/vscode-lean4#597 · Filter by author vadimkantorov opened on Mar 28, 2025
  3

• Rendering of \varphi and \phi in Lean files

  leanprover/vscode-lean4#584 · Filter by author bgoodri opened on Mar 5, 2025
  2

• Opening some paths with curly brackets still fails

  bug
  leanprover/vscode-lean4#570 · Filter by author mhuisi opened on Jan 13, 2025
  1

• RFC: Math in hovers

  RFC
  leanprover/vscode-lean4#541 · Filter by author Vtec234 opened on Oct 21, 2024
  1

• InfoView not working Xubuntu 22.04

  leanprover/vscode-lean4#517 · Filter by author solmersa opened on Aug 13, 2024
  1

• RFC: do not use _serverProcess in leanclient.

  leanprover/vscode-lean4#487 · Filter by author joneugster opened on Jun 26, 2024
  1

• Stale dependency diagnostic does not show up under 'Messages' after opening VS Code

  bug
  leanprover/vscode-lean4#424 · Filter by author mhuisi opened on Mar 27, 2024