leanprover / leanprover/vscode-lean4
pinned InfoView not updated
Nobody has claimed this yet.
- Dominant language
- TypeScript
- Stars
- 313
- Forks
- 104
- Avg merge
- 1h 56m
- Merged PRs (30d)
- 1
Description
Description
I have observed that a pinned InfoView (whether Expected Type or Goal states) does not update as I change the code around it.
Steps to Reproduce
Did not try to get a #mwe yet, but here is a screencast. I update the type of the hypotheses, but the pinned goal state does not update:
https://github.com/user-attachments/assets/953d506d-9be7-4d0d-8b94-1278deb94fe4
Versions
Operating system: Linux (release: 6.14.2)
CPU architecture: x64
CPU model: 8 x 11th Gen Intel(R) Core(TM) i7-1185G7 @ 3.00GHz
Available RAM: 16.46 GB
VS Code version: Reasonably up-to-date (version: 1.99.1)
Lean 4 extension version: 0.0.200
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.20.0-nightly-2025-04-28)
Project: Valid Lean project (path: /home/…)
Elan toolchains:
installed toolchains
--------------------
lean4
lean4-stage0
leanprover/lean4-nightly:nightly-2024-02-10
leanprover/lean4-nightly:nightly-2024-02-21
leanprover/lean4-nightly:nightly-2024-03-01
leanprover/lean4-nightly:nightly-2024-03-10
leanprover/lean4-nightly:nightly-2024-09-17
leanprover/lean4-nightly:nightly-2025-01-07
leanprover/lean4-nightly:nightly-2025-01-10
leanprover/lean4-nightly:nightly-2025-01-22
leanprover/lean4-nightly:nightly-2025-01-24
leanprover/lean4-nightly:nightly-2025-01-27
leanprover/lean4-nightly:nightly-2025-02-11
leanprover/lean4-nightly:nightly-2025-03-01
leanprover/lean4-nightly:nightly-2025-03-03
leanprover/lean4-nightly:nightly-2025-03-07
leanprover/lean4-nightly:nightly-2025-03-21
leanprover/lean4-nightly:nightly-2025-04-28
leanprover/lean4-pr-releases:pr-release-5998
leanprover/lean4-pr-releases:pr-release-6355
leanprover/lean4-pr-releases:pr-release-6744
leanprover/lean4:v4.10.0
leanprover/lean4:v4.12.0
leanprover/lean4:v4.16.0
leanprover/lean4:v4.16.0-rc1
leanprover/lean4:v4.16.0-rc2
leanprover/lean4:v4.18.0-rc1
leanprover/lean4:v4.19.0-rc2
active toolchain
----------------
leanprover/lean4-nightly:nightly-2025-04-28 (overridden by '/home/jojo/…/lean-toolchain')
Lean (version 4.20.0-nightly-2025-04-28, x86_64-unknown-linux-gnu, commit 747ea853b593, Release)
Impact
Low impact on me. I’m not using this feature so far and was curious if I would want, that’s when I noticed that it didn’t do what I expected it to do.
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by reproducing the behavior in the pinned InfoView for both Expected Type and Goal states, following the linked screencast and the reported Linux, VS Code, and Lean versions. Trace how the extension refreshes the pinned view after hypothesis types change; done means the displayed goal or expected type updates without reopening or repinning the InfoView.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- typescript, vscode
- Domain
- devtools
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100