Linting hangs on missing imports

Stream: mathlib4

[Yaël Dillies]

Whenever an import is wrong, build fails but CI hangs on linting. See eg https://github.com/leanprover-community/mathlib4/actions/runs/9228031291/job/25391234077?pr=11448. Is this known?

[Damiano Testa]

I have observed this as well, but have not seen it reported.

[Yaël Dillies]

I assume this is a lake issue? cc @Mac Malone

[Kim Morrison]

Can you reproduce it locally, @Yaël Dillies? It seems more likely to be a linter issue than a lake issue.