server out of sync with file when editing imports on Windows

[fpvandoorn]

Description

On Windows, the following steps reliably cause the server to go out of sync with the file. This issue is not reproducible on Linux.

Context

Zulip thread

Steps to Reproduce

1. Download mathlib and its cache (I can reproduce on v4.2.0, but presumably also every other version)
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 2 separate Windows computers 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.

Impact

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

[Kha]

The relevant code has been almost completely rewritten on master, it would be good to check if 4.8.0-rc1 still exhibits the behavior when it lands

[mhuisi]

@fpvandoorn Do you still encounter this issue on 4.8.0?

[fpvandoorn]

Yes, both this issue and #3786 still happen for me. In fact, with the steps described in this issue, both these behaviors can happen. I'm testing this now on Mathlib 826a3e67f2 (from yesterday), Lean version 4.8.0-rc2.

Executing steps 1-3 can lead now to one of the following three situations:

• The server doesn't recompile the file at all after step 3, and the behavior of steps 4-5 happens
• The server starts recompiling, but never stops. The yellow bars stay for many seconds (issue server hangs when changing imports #3786)
• Sometimes we get the intended behavior: the server recompiles the file for <0.1 second, and the file behaves completely normally afterwards.

These situations can all happen after performing these steps, even when trying to do exactly the same thing. If I take the file and repeatedly remove and add the import-line with uses of ctrl+X and ctrl+V, I can get all three outcomes on different iterations.

[mhuisi]

Ok, I can reproduce the outcome of step 5 on Windows as well. I haven't seen the server eternally recompiling yet, though.