Commit 2026-10-20 19:29 6d442b50

feat(Tactic/Linter/Header): suggest formatting imports according to the style convention (#44507) This PR enables the header linter to reformat imports to match the style guide. It logs an interactive suggestion in the event that imports are not formatted correctly. (The try-this suggestion preserves comments above and inline with each import.) This is only active in the module system, and currently only for files in Mathlib (and test files). This linter is on by default whenever linter.style.header is on, but may be turned off separately from the rest of the header linter by writing set_option linter.style.header.imports false just after the import block. (Note: while we're here, we also allow linter.style.header.license to be set just after the import block for consistency.) The suggestion does not "normalize" imports as #norm_imports does, i.e. eliminate redundancy among imports. It only makes sure that the imports are ordered and grouped correctly. This also fixes some unformatted imports that crept in since #44513.