Bug in the VS Code extension?

Stream: general

[Riccardo Brasca]

In the flt3 repo something strange happens: in the file FLT3.lean, if you comment/delete line 731 everything seems fine (meaning that VS Code does not complain). In reality, there is an error in line 734, as one can see doing lake build.

Even weirder, if one does the same in the previous goal (commenting 724), the error is visible as it is supposed to be at line 727 (the two goals are very similar). This happens for me (on Debian), but not for @Filippo A. E. Nuccio on windows, and it also happens using Codespace.

Does anyone recognize this behavior or should I try to minimize it?

[Filippo A. E. Nuccio]

I should add that I was using version 0.0.155 instead of 0.0.159 (but Riccardo has the same problem even after reverting to the previous version).

[Sebastian Ullrich]

That's probably on me, I'll look into it tomorrow (but further minimization welcome!). Thanks for the reproducer.

[Riccardo Brasca]

It's later than I thought, I will try to minimize it tomorrow

[Riccardo Brasca]

In VS Code I don't see any error in the following code

import Mathlib.Tactic.Ring

local notation3 "λ" => 1

theorem foo (u : Nat) : 1 ∣ u := by
  · use 1
    rw [show λ ^ 2 * (-kX + kY + ↑(u₄ S) * kZ) =
      - (λ ^ 2 * kX - λ ^ 2 * kY - ↑(u₄ S) * (λ ^ 2 * kZ)) by ring]
    sorry

[Riccardo Brasca]

Without mathlib

local notation "λ" => 1

theorem foo (u : Nat) : 1 ∣ u := by
  · refine ⟨1, ?_⟩
    rw [show λ ^ 2 * (-kX + kY + ↑(u₄ S) * kZ) =
      - (λ ^ 2 * kX - λ ^ 2 * kY - ↑(u₄ S) * (λ ^ 2 * kZ)) by sorry]
    sorry

[Riccardo Brasca]

Of course the rw line does not make sense, things like kX don't exist, but still no error in VS Code. If I don't use the · I get the expected error.

[Riccardo Brasca]

Even smaller

theorem foo : 0 = 0 ∧ 0 = 0 := by
  constructor
  · rfl
  · rw [show a = 0 by sorry]
    sorry

[Damiano Testa]

Or even

theorem foo : False := by
  · rw [show a = 0 by sorry]

[Riccardo Brasca]

Yeah, the problem seems to be the dot. I used a goal with two goals just to be in a realistic situation.

[Riccardo Brasca]

The same happens with the online editor