v0.0.152-pre

• Add an extensive manual for the VS Code extension and how it interacts with Lean (#453)

v0.0.151-pre

• Add setup diagnostics for project initialization commands (#450)
• Fix a bug where upgrading from Elan 3.1.0 silently failed (#448)
• Adds a \span abbreviation for ∙ (#447, author: @arienmalec)

v0.0.150-pre

• Improve granularity of Lean 4 core folder detection (#446, author: @eric-wieser)

0.0.147-0.0.149 were dud releases that were only published to the VS Code marketplace, not the open-vsx one, due to an open-vsx issue with the Eclipse publisher agreement.

v0.0.146-pre

• Fixes an issue where opening the core Lean 4 repository would yield an error (#443)

v0.0.145-pre

• Better setup diagnostics (#436):
  • Warnings and errors for issues with the user's Lean 4 setup (warnings can be disabled with the lean4.showSetupWarnings option)
  • 'Troubleshooting: Show Setup Information' command to dump information about the user's Lean 4 setup
  • Removal of the following config options: lean4.toolchainPath, lean4.lakePath, lean4.enableLake, lean4.serverEnv, lean4.serverEnvPaths
  • New config option lean4.envPathExtensions to replace these settings
  • Removal of pre-lake serve compatibility

v0.0.144

• Add support for multi-toolchain projects and support correct operation when no project folder is opened (#428)
• Use the correct toolchain when opening sub-folders of Lean 4 projects (#433)
• Fix a bug where output URIs would regularly crash the VS Code extension (#437)

v0.0.143-pre

• Fix a bug where output URIs would regularly crash the VS Code extension (#437)

v0.0.142-pre

• Use the correct toolchain when opening sub-folders of Lean 4 projects (#433)

v0.0.141-pre

• Add support for multi-toolchain projects and support correct operation when no project folder is opened (#428)

v0.0.140

• Fix an InfoView performance bug that was introduced recently (#432)
• Refer to setup guide in some errors encountered by new users (#429)