Mathlib.Init linter error

Stream: mathlib4

[Kim Morrison]

I've never particularly been a fan of Mathlib.Init, but I understand people like it. Could I put in a request for such a person to improve the error message:

error: the following 1 module(s) do not import Mathlib.Init: #[...]

in the situation that adding import Mathlib.Init would cause an import cycle, to instead explain where to add the exception?

(c.f. #32416)

[Michael Rothgang]

Thanks for the complaint. Sorry that you got stuck on an unhelpful error messages. I just commented on the PR suggesting the right fix.

[Michael Rothgang]

I'm happy to make a PR improving the error, but am really busy in the next two weeks. If you periodically ping me (say, start of next week and the one after), I'll make sure to find time for this.

[Kim Morrison]

Did you mean that if I import Mathlib.Tactic.Linter.Header, then I can remove the exception in lint-style?

[Kim Morrison]

I think I have it now.

[Michael Rothgang]

No: you should import the header linter and keep the exception (but with a different comment for its existence).

[Kim Morrison]

It seems if I import this file into Mathlib.Init then no exception is needed?

[Michael Rothgang]

Ah, you're importing it directly: then it's fine. Transitive imports you need to add by hand, for now.

[Kim Morrison]

Longer term, should we insist that everything is imported directly (thereby not needing the confusing exceptions) or just do the analysis and allow everything transitively imported by Mathlib.Init?

[Kim Morrison]

fix(scripts/lint-style): improve Mathlib.Init import error messages #32419

is Claude's attempt at providing me with an actionable error message.

[Michael Rothgang]

If you add the analysis for transitive imports (i.e., making the linter smarter), I'm happy about that!

[Kim Morrison]

Sure!

[Kevin Buzzard]

My least favourite thing about Mathlib.Init is that if anyone ever downloads the FLT repo and opens a new file, they immediately get the incomprehensible error

invalid -D parameter, unknown configuration option 'linter.mathlibStandardSet'

If the option is defined in a library, use '-Dweak.linter.mathlibStandardSet' to set it conditionally

(thus making it look like the repo is mis-installed, but it is actually code for "please type import Mathlib.Init")

[Kim Morrison]

Yes, this is really disastrous. :-) I am all for killing Mathlib.Init, but working with the constraint that we don't, let's see what we could do in this situation...

[Kim Morrison]

Actually, @Kevin Buzzard, why doesn't FLT just prepend weak. to that option name, as the error suggests? :-)

[Kim Morrison]

Michael Rothgang said:

If you add the analysis for transitive imports (i.e., making the linter smarter), I'm happy about that!

@Michael Rothgang, done.

[Kevin Buzzard]

Kim Morrison said:

Actually, Kevin Buzzard, why doesn't FLT just prepend weak. to that option name, as the error suggests? :-)

Oh I absolutely could do that -- basically I never change any system files in FLT, the default set-up with anything other than mathematics in FLT is "other people do everything and I understand nothing" (although this changed recently because I actually attempted, and failed, to add a test; see #general > Project dashboard @ 💬 , so maybe there's hope for me yet )

[Michael Rothgang]

Kim Morrison said:

Yes, this is really disastrous. :-) I am all for killing Mathlib.Init, but working with the constraint that we don't, let's see what we could do in this situation...

I agree this is not great user experience! I do think Mathlib.Init solves a real problem, though (making sure all files in mathlib are run with all syntax linters - and making sure some basic imports are available everywhere). Kim: If you propose killing that file, how would you like to solve this?

[Chris Henson]

In CSLib we also spent a lot of time thinking about Mathlib.Init with the motivation Michael mentions of making sure syntax linters are available everywhere. I don't consider weak a great solution, because it puts you in a situation where you could silently not have linters if you're missing an import.

The solution I came up with is to write a test that uses importGraph to check transitive imports. In fact we ended up creating our own Cslib.Init file, currently including Mathlib.Tactic.Common, Mathlib.Init, and our own linters. To me this indicates that maybe this idea of ensuring imports is something that could be a broadly useful tool.

(I know we had some of this discussion previously, but I can't find it at the moment)