identifier info

Stream: general

[Reid Barton]

Does anyone remember an old "fun" Lean 3 bug where jump to source would sometimes jump to totally unrelated definitions?
And it was somehow related to whether the identifier occurred at the same line/column position (or byte offset?) as something in a tactic?

[Pedro Sánchez Terraf]

I have experienced this several times. IIRC, jumping to source goes to the tactic applied at the beginning of the line. I'm running

Lean (version 3.48.0, commit 283f6ed8083a, Release)
elan 1.4.2 (4a1b1b918 2022-09-13)

[Reid Barton]

Aha, I found it:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Extension.20showing.20goal.20for.20a.20separate.20lemma/near/209569264

[Reid Barton]

Here's another fun jump-to-source bug (Lean 3).

-- test

def nat.to_int (n : ℕ) : ℤ := n

theorem t (n : ℕ) : true :=
begin
  have : _,
  { exact n.to_int.add_zero },
  trivial
end

If you use jump to source on n.to_int.add_zero, it will go to the file containing int.add_zero but the line/column position of nat.to_int.

[Johan Commelin]

What was the other one we found recently, where it wouldn't jump at all. Something like

example : by apply @classical.some = @classical.some := rfl

and it would only have jump-to-defn on the RHS but not on the LHS.

[Reid Barton]

Yes that was extremely mysterious