I have a hunch that this is because #460 switched to using the set of open documents tracked by the language client. I already noticed a potential bug in the language client library in that PR, but thought that this bug would not affect us. Perhaps it does. Typically, I prefer using state that is already there to avoid introducing race conditions, but it looks like that may not be possible here.
Reported at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Warning.20in.20project.20version/near/442775409.
I have a hunch that this is because #460 switched to using the set of open documents tracked by the language client. I already noticed a potential bug in the language client library in that PR, but thought that this bug would not affect us. Perhaps it does. Typically, I prefer using state that is already there to avoid introducing race conditions, but it looks like that may not be possible here.