pinned InfoView not updated #616
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:
not-updating.mp4
Versions
Details
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.