sync: 2025-01-12 #2
Open
+3,236
−663
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Fixes a bug where InfoView would not appear in locked tab group after restarting VS Code - Adds a command to the forall menu for re-displaying a sticky setup error in case it was closed by accident and users have no clue how to re-open it (by selecting a new Lean tab)
This PR replaces
```
import path = require('path')
```
by
```
import path from 'path'
```
in a couple of files.
---------
Co-authored-by: Jon Eugster <[email protected]>
The InfoProvider opens the webviewPanel, so it should also call the webviewPanel's dispose function when gettting disposed.
The `Console` class does not seem to exist for the browser. This implementation of the `logger` behaves exactly like before for all `logger.log` and `logger.error` calls (which are the only ones used in the project).
The diff on `userWidget.tsx` explains the purpose of this PR.
This PR implements support for Elan 4.0.0. Specifically: - A new setting that can be enabled to issue confirmation prompts before installing new toolchains - Confirmation prompts before eagerly updating release channels when opening Lean files in VS Code with Elan 4.0.0's eager toolchain resolution - New VS Code command integrations for Elan: - Project and default toolchain selection that displays all available Lean toolchains by using https://release.lean-lang.org/ - Toolchain deinstallation, including integration for `elan toolchain gc` in Elan 4.0.0 - Manual updates of release channel toolchains It also fixes a couple of bugs: - When the output of `elan show` got too large, the 'Troubleshooting: Show Setup Information' command would display a dialog that could exceed the height of the screen, hiding all buttons. With Elan 4.0.0, the content of this dialog is now kept much smaller so that this cannot happen on most screens anymore. - The InfoView would sometimes report internal errors (including stacktraces) when something went wrong on the VS Code side of the InfoView. Now it correctly displays the error. - The order of the buttons in lots of modal dialogs was a bit unorganized, and it should now be more coherent. - If the default toolchain was changed while VS Code was running, the VS Code extension would hold on to the old toolchain for the language client of untitled files indefinitely. - VS Code extension commands that use the active client of the client provider would behave incorrectly or use an incorrect client if a client failed or was stopped manually using a command. - The 'Restart Server' command didn't always restart the setup check for the selected language client if that language client had failed in the past. <details> <summary>Update dialog</summary>  </details> <details> <summary>Installation dialog</summary>  </details> <details> <summary>New version management commands</summary>  </details> <details> <summary>Default version dialog</summary>  </details> <details> <summary>Release channel update dialog</summary>  </details> <details> <summary>Version uninstall dialog</summary>  </details> This PR will be merged at the start of 2025.
Adds a note about disabling automatic hovers to the manual and notes about antivirus software, adding `brew` to the PATH and network drives or cloud storage to the setup guide. Closes #533.
Implements context menu entries to (un)select subexpressions in the tactic state, in particular to unselect all of them at once.
Issue originally reported at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Elan.20.2B.20Lean4.20Extension/near/493333609. Unfortunately, the language client library still doesn't support relative patterns (e.g. VS Code's `GlobPattern`) to avoid having to escape these file names. This is already implemented, but not released yet, so this may be worth re-visiting in the future.
This PR ensures that there are no redundant line breaks when the trace
formatter is including a newline at the end of a trace line.
Example (from `whnfProj.lean`):
```lean
import Lean
def h (x : Nat) := x
def f (x : Nat) := x + 1
def g (x : Nat) := (x, x+1).fst
open Lean
open Lean.Meta
def tst (declName : Name) : MetaM Unit := do
let c ← getConstInfo declName
lambdaTelescope c.value! fun _ b => do
trace[Meta.debug] "1. {b}"
trace[Meta.debug] "2. {← withReducible <| whnf b}"
trace[Meta.debug] "3. {← withReducibleAndInstances <| whnf b}"
trace[Meta.debug] "4. {← withDefault <| whnf b}"
pure ()
set_option trace.Meta.debug true
#eval tst `f
#eval tst `g
```
With Elan 4.0.0, installing Elan doesn't actually install a toolchain anymore. Only when creating or opening a project it will install a toolchain. This PR adjusts the setup guide and the Elan installation prompt to reflect that.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.