v0.0.155

• Better setup diagnostics (#436, #443, #448):
  • 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
• Add setup diagnostics for project initialization commands (#450)
• Add an extensive manual for the VS Code extension and how it interacts with Lean (#453, #454, #456)
• Improve granularity of Lean 4 core folder detection (#446, author: @eric-wieser)
• Adds a \span abbreviation for ∙ (#447, author: @arienmalec)