Server out of sync with file

Stream: lean4

[Floris van Doorn]

I think people have mentioned that sometimes the Lean server will get out of sync with the state of the file. I just found a way to reproduce it. I can reproduce it on v4.2.0, but also on other versions on Mathlib. This is on Windows, does this reproduce on other machines?

(1) Download mathlib and its cache
(2) Create a new file with the following contents, and wait until Lean has compiled the file

import Mathlib
#eval 1+1

(3) Delete the first line all at once (e.g. with ctrl+X). On my computer this does not cause a recompilation of the file
(4) Type the letter a on the first line and wait until Lean shows an error
(5) Remove the letter a. The error remains. The error remains even if you start typing new commands (e.g. def foo := 1), and the server is interpreting as a letter a floating somewhere in your file. It disappears once you write import again.

I experimented with importing less than Mathlib, and below a certain number of imports, this behavior seems to go away. (e.g. if we replace import Mathlib with import Std, then step 3 does cause a recompilation of the file.

[Damiano Testa]

I tried, but I cannot reproduce on Linux with VSCode.

(Also, the online editor does not seem to have the behaviour that you mention.)

[Floris van Doorn]

Interesting. Thanks for trying.
Can someone on Windows try to reproduce this?

[Sebastien Gouezel]

I'm on windows, and I get the same behavior as the one you describe, with a phantom a floating around. For instance, if my first line is

theorem foo : True := trivial

I get the error message

unknown identifier 'triviala'

[Floris van Doorn]

vscode-lean4#364

[Kevin Buzzard]

Also on linux, when I delete the first line all at once in step 3 I very briefly see orange bars, and the error does not remain in step 5.

[Eric Wieser]

Does this error persist if you save the file with unix line endings?

[Floris van Doorn]

Yes, this happens if the file is using unix line endings (VSCode is showing LF in the bottom-right).