Skip to content

Releases: leanprover/vscode-lean4

v0.0.212

15 Sep 09:04
Compare
Choose a tag to compare
  • Add new installation mechanism that installs Git and curl automatically (#641, #648)
  • Add language server support for lakefile.toml by depending on Even Better TOML (#646)
  • Add a new sort order for 'All messages' in the InfoView (#645, #647)
  • Re-add copy-state and copy-message functionality to the InfoView context menu (#644)
  • Increase auto-completion delay (#654)
  • Fix 'Stop Server' command (#642)
  • Ensure that all update options are provided in the 'Update Dependency' command (#638)
  • Bump recommended Elan version to 4.0.0 (#640)
  • Ensure that Lean extension activates when any file in a Lean project is opened (#637)
  • Alias \dot and \cdot to \centerdot (#639)
  • Add abbreviations for macrons (#633, author: @Komyyy)
  • Add two-sided abbreviation for norms (#634, author: @Julian)
  • Add abbreviation for HEq (#632, author: @Rob23oba)
  • Fix a bug where the extension would issue 'Restart Server' notifications even when a config file was merely touched, not actually modified (#651)

v0.0.211-pre

21 Aug 08:47
Compare
Choose a tag to compare
v0.0.211-pre Pre-release
Pre-release
  • Fix a bug where the extension would issue 'Restart Server' notifications even when a config file was merely touched, not actually modified (#651)
  • Increase auto-completion delay (#654)

v0.0.210-pre

19 Aug 09:29
Compare
Choose a tag to compare
v0.0.210-pre Pre-release
Pre-release
  • Add new installation mechanism that installs Git and curl automatically (#641, #648)
  • Add language server support for lakefile.toml by depending on Even Better TOML (#646)
  • Add a new sort order for 'All messages' in the InfoView (#645, #647)
  • Re-add copy-state and copy-message functionality to the InfoView context menu (#644)
  • Fix 'Stop Server' command (#642)
  • Ensure that all update options are provided in the 'Update Dependency' command (#638)
  • Bump recommended Elan version to 4.0.0 (#640)
  • Ensure that Lean extension activates when any file in a Lean project is opened (#637)
  • Alias \dot and \cdot to \centerdot (#639)
  • Add abbreviations for macrons (#633, author: @Komyyy)
  • Add two-sided abbreviation for norms (#634, author: @Julian)
  • Add abbreviation for HEq (#632, author: @Rob23oba)

v0.0.209

26 Jun 11:36
Compare
Choose a tag to compare
  • Add client-side support for module hierarchy (#620)
  • Improve lake exe cache get error reporting (#621)
  • Add better error message for Windows antivirus cache errors (#624)
  • Allow using language ID lean in markdown blocks (#622)

v0.0.208-pre

11 Jun 12:22
Compare
Choose a tag to compare
v0.0.208-pre Pre-release
Pre-release
  • Add client-side support for module hierarchy (#620)
  • Improve lake exe cache get error reporting (#621)
  • Add better error message for Windows antivirus cache errors (#624)
  • Allow using language ID lean in markdown blocks (#622)

This release was not published on OpenVSX because OpenVSX is once again broken.

v0.0.207

04 Jun 08:23
Compare
Choose a tag to compare
  • Improve the progress bar message when launching the language server (#619)

v0.0.206

03 Jun 11:53
Compare
Choose a tag to compare
  • Fix vscode-lean4 being broken on v4.21.0-rc1 due to an invalid semantic version reported by Lake (#618)

v0.0.205

30 Apr 16:00
Compare
Choose a tag to compare
  • Fix bug where InfoView tooltips would pop up while selecting text (#615)

v0.0.204

23 Apr 14:56
Compare
Choose a tag to compare
  • Revamp InfoView settings and actions (#606)
  • Improve error when fork of extension is installed (#613)
  • Sort installed toolchains in dialogs that display them (#611)

This release was not published on OpenVSX because it is currently down.

v0.0.203

17 Apr 12:37
Compare
Choose a tag to compare
  • Make Lean files in .elan and .lake read-only (#608)
  • Add error when opening project that contains a Lakefile but no lean-toolchain file (#610)