VSCode does not react to changes

Stream: lean4

[Alexander Bentkamp]

Hi, I am suffering from a weird bug in VSCode where on some files in my project, Lean4 won't react do changes in the document unless I trigger "Restart File" manually. When I rename the file that suffers from this, it works again. When I reclone the project, the bug suddenly affects other files. But I cannot consistently reproduce the bug unfortunately. Anyone else encountering this?

[Floris van Doorn]

I have also noticed this sometimes when adding a new file to mathlib4. I don't know how to reproduce it consistently or how to solve it once it happens.

[Gabriel Ebner]

Looks like lean4#1219

[Alexander Bentkamp]

Thanks, I will try Mac's workaround at the next occasion!

[Floris van Doorn]

I can consistently reproduce this on my Windows machine and added some observations in lean4#1219.