cache error through extension: target is out of date

Stream: mathlib4

[Thomas Murrills]

If I pull, for example, #30577, navigate to, say, Mathlib.Geometry.Manifold.Notation, (which does not see any changes to itself or its imports in this PR) then try to get the cache through the VS Code extension command (either one), it successfully fetches the cache.

Then, however, it automatically restarts the file, an info-severity diagnostic "error: target is out of date" flashes briefly at the top of the file, and I get the "Imports are out of date and must be rebuilt" error. On restarting the file manually, it did start rebuilding (from Mathlib.Data.Fin.Embedding, it seemed).

(Note that git merge master says the branch is already up to date.)

Is this a known issue?

[Johan Commelin]

cc @Marc Huisinga

[Marc Huisinga]

I can't reproduce the issue from these instructions. After the cache is fetched, the language server is restarted and the file processes as expected.

What does running lake exe cache get and then lake build from the command line do for you?

[Marc Huisinga]

@Johan Commelin Did this reproduce for you?

[Johan Commelin]

Sorry, I didn't try to repro. I saw the "Is this a known issue?", and thought that you were in the best position to answer that.

[Nailin Guan]

Marc Huisinga 說：

I can't reproduce the issue from these instructions. After the cache is fetched, the language server is restarted and the file processes as expected.

What does running lake exe cache get and then lake build from the command line do for you?

I think this happens only when cache is not fully fetched. I met the same issue before on a branch with no PR, every thing else is just as normal after restart file.