Sync #3
Open
Sync #3
Conversation
This file contains hidden or 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 leanprover#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
```
…er#577) 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.
Adds abbreviations for `⦋` and `⦌`, which are used in mathlib to denote objects of the simplex category (as of [mathlib4#21565](leanprover-community/mathlib4#21565)). --------- Co-authored-by: Marc Huisinga <[email protected]>
Came across this while I tried to use the input. Took me a while to figure out why it wasn't behaving like on https://loogle.lean-lang.org/, so I think the fix should be documented.
…ver#572) I tried to use this component, but it prevents accessibility because it prevents default for all `tab` clicks.
This PR reverts leanprover#571 because it could sometimes cause trace messages to be formatted incorrectly. The proper fix for this issue is leanprover/lean4#7143. On Lean versions before leanprover/lean4#7143, this PR will simply cause some trace messages to contain redundant newlines again. After leanprover/lean4#7143, these newlines will be gone, and trace messages will be formatted correctly.
This PR adjusts the progress bar message to reflect that it is cloning missing packages (suggesting that it may hence take a while). It also adjusts the output of `lake serve` in the output panel to mention the command that was called.
…eanprover#623) `#stringBlock` is a block in the lean 3 / lean 4 syntax file, and it was added in 48ad018 on 2020-06-23, when people were developing in the legacy vscode-lean repo. Later, `#stringBlock` was removed in ca65431 on 2021-01-18 when migrating from lean 3 to lean 4. Somehow, the `include` line was forgotten. This PR now removes the line. In fact, VS Code’s parser (vscode-textmate) will tolerate missing includes, so the original syntax works. (You could verify it by amending `~/.vscode/extensions/leanprover.lean4-0.0.207/syntaxes/lean4.json` and reloading the VS Code window.) However, including the inexistent `#stringBlock` will cause problems for a downstream project. If you are concerned about the details, please refer to sharkdp/bat#3286.
…ver#622) This PR ensures that doc comments can use `lean` in addition to `lean4` for the language ID in markdown code blocks and also have them be highlighted in hovers.
This PR ensures that the VS Code extension always reports the error that occurred when `lake exe cache get` fails in Mathlib or in a project downstream of Mathlib. Previously, this was only the case for project creation commands.
…over#624) This PR adjusts the error message that is reported on Windows when Lake commands fail while fetching build cache artifacts to suggest that the issue might have been caused by a third-party antivirus, linking to the setup guide with steps to fix the issue.
This PR adds client-side support for a new module hierarchy component in VS Code that can be used to navigate both the import tree of a module and the imported-by tree of a module. Specifically, it adds a new module hierarchy tree view and 'Module Hierarchy: Show Module Hierarchy' and 'Module Hierarchy: Show Inverse Module Hierarchy' commands to display it for the current file. Companion PR at [leanprover/lean4#8654](leanprover/lean4#8654).   This PR also changes all commands of the extension to exclude the `Category:` prefix from menus.
`≍` has recently been added as notation for `HEq`, but the only abbreviation for it currently available is `\asymp`. This PR adds the more intuitive `\heq` as abbreviation for the same symbol.
We already have `norm`, but this matches the convention for other "bracketed" abbreviations where `\<opening><closing>` produces `<opening>$CURSOR<closing>`.
I'm Miyahara K**ō**, so it takes a time to type my name.
This PR ensures that the extension will attempt to activate all Lean-specific features when opening any file in a Lean project, not just when opening a Lean file. The came up at [#general > Updating Mathlib via VSCode menu does not work @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Updating.20Mathlib.20via.20VSCode.20menu.20does.20not.20work/near/526969295).
Discussed at [#lean4 > \cdot != \centerdot @ 💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.5Ccdot.20!.3D.20.5Ccenterdot/near/528312220).
Elan 4.0.0 has been out for a while now, so we now issue a warning if the Elan version is older than that.
…r#638) This PR removes the logic from the 'Update Dependency' command that hides dependencies that are already up-to-date relative to the manifest and removes the revision information from the selection dialog. The reason for this is that the manifest is not an up-to-date representation of the set of dependencies in the `lakefile.lean` or the `lakefile.toml`, e.g. if the input revision in the Lake configuration file was changed. I don't know of a way to query this information from Lake without also updating all the revisions of the manifest in the process, so we now just avoid this situation entirely by considering the revision information in the manifest to be unreliable. Note that there is still a shortcoming of this approach: When adding a new dependency to the `lakefile.lean` or the `lakefile.toml`, we won't display it in the update dialog until the manifest is updated. This came up at [#general > Updating Mathlib via VSCode menu does not work @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Updating.20Mathlib.20via.20VSCode.20menu.20does.20not.20work/near/526969295).
Author: austaras <[email protected]> Date: Thu Jan 9 19:52:07 2025 +0800
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.