quick build of all files at `import`

Stream: lean4

[Jireh Loreaux]

On recent Mathlib (I think after the v4.8 bump), I'm experiencing a slowdown when I import something. In particular, with a fresh cache, I get this whenever I edit something right below the import. It seems to go through and check all files which it obviously had to do before, but maybe the fact that it's now printing them all slows it down? This is significantly slower for me.

Screencast_20240503_113917.webm

[Kim Morrison]

Just tagging @Mac Malone to be sure he's seen this.

[Mac Malone]

My guess is that this is due ot VSCode waiting on the sever to report each of this individual lines.Hopefully, we can threshold updates in the server to avoid sending an update every line.