search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
170 stars 49 forks source link

Pinned locations are tracked incorrectly #499

Closed Vtec234 closed 4 months ago

Vtec234 commented 4 months ago

Description

Adding a newline in the source should move pinned locations below that line down by 1. Under certain circumstances (which I haven't attempted to identify but which seem to occur fairly often), the pinned locations move by 2 instead. This completely defeats the purpose of pinning to see the results of edits made above in realtime. Note that this used to work correctly, so it must have been a recent regression.

Steps to Reproduce

  1. Pin a location, for example Test.lean:100:2.
  2. Add a newline above it.
  3. Pinned location is now Test.lean:102:2.

Expected behavior: Pinned location updates to Test.lean:101:2.

Actual behavior: As above.

Versions

vscode-lean4 v0.0.171 leanprover/lean4:4.10.0-rc1

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

mhuisi commented 4 months ago

Do you have a concrete example? I've tried a couple of examples but couldn't find one where the pin was moved by two lines.

Vtec234 commented 4 months ago

I also can't reproduce it now. If it happens again I will reopen this.