Errors on files not in `Mathlib.lean`

Stream: mathlib4

[Michael Rothgang]

@Patrick Massot stumbled across some somewhat surprising behaviour today --- this might be called a feature, but the error messages are really ... not ideal. This behaviour has two parts.

Part one is a hidden scratch file feature (which I had not seen before; is this new, e.g. a side effect of the new module system? is it intentional?). Basically,

• create a new file (in my case, Mathlib/Geometry/Manifold/VectorField/Test.lean)
• do not add this file to Mathlib.lean

• add some basic content, but not copyright or module doc-strin
  (example output: import Mathlib.Geometry.Manifold.VectorBundle.Basic open scoped Manifold )

• observe that there are no linter errors

• add the new file to Mathlib.lean
• reload, and see linter errors appearing

[Michael Rothgang]

I have a theory why this happens: while the header linter is transitively imported in my test file, the configuration enabling it by default is set in the lakefile, which looks at Mathlib.lean, which does not include this file. (Is this correct?)
Is this desirable behaviour? (I can see an argument in favour, but am not sure yet.)

[Michael Rothgang]

Part 2: you can only import files listed in Mathlib.lean. That one is definitely surprising to me, and I don't see it being a useful feature.

• remove your Test.lean file from Mathlib.lean again
• create a new file Mathlib/Geometry/Manifold/VectorField/Test2.lean with content import Mathlib.Geometry.Manifold.VectorField.Test; get an error:

Running Mathlib.Geometry.Manifold.VectorBundle.Test
error: no such file or directory (error code: 2)

[Damiano Testa]

Doesn't the header linter use Mathlib.lean to decide what to lint?

[Damiano Testa]

I think that this was a response to make scratch files not annoyingly noisy.

[Damiano Testa]

I forget the details, but there is https://github.com/leanprover-community/mathlib4/blob/master/Mathlib%2FTactic%2FLinter%2FHeader.lean#L215

[Damiano Testa]

docs#Mathlib.Linter.isInMathlib