Module system error related to `import all` and renaming

Stream: lean4

[Michael Rothgang]

In #33708, I'm renaming a mathlib linter (and moving the associated file). The associated file in MathlibTest uses the module system and import all (to access internal functions, for unit testing). After this PR, the import all statement errors with

`[redacted]/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lake setup-file [redacted]/mathlib4/WhitespaceLinter.lean -` failed:

stderr:
✔ [136/139] Built Mathlib.Tactic.Linter.Whitespace (2.3s)
✔ [137/139] Built Mathlib.Init (1.2s)
✔ [138/139] Built Mathlib.Tactic.Lemma (860ms)
✖ [139/139] Running setup-file [redacted]/mathlib4/WhitespaceLinter.lean
error: [redacted]/mathlib4/WhitespaceLinter.lean: cannot `import all` the module `Mathlib.Tactic.Linter.Whitespace` from the package `mathlib`
Some required targets logged failures:
- setup-file [redacted]/mathlib4/WhitespaceLinter.lean
Failed to build module dependencies.

[Michael Rothgang]

Just the import statement is fine. Any suggestions how to even investigate this? The PR only renames modules, so I don't see what could be causing this.

[Sebastian Ullrich]

Why did you move it out of the MathlibTest/ folder?

[Jovan Gerbscheid]

Nevermind, you're right

[Michael Rothgang]

Oh, I moved the file outside of MathlibTest :man_facepalming: that explains it. Moving it in there fixes the error.