From a7a63b19d7538c8e1f89702425cc396650614e31 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 12 Oct 2026 14:11:27 -0400 Subject: [PATCH 01/16] feat: lint import formatting --- Mathlib/Tactic/Linter/Header.lean | 70 +++++++++++---------- MathlibTest/Linter/Header/ImportFormat.lean | 29 +++++++++ 2 files changed, 67 insertions(+), 32 deletions(-) create mode 100644 MathlibTest/Linter/Header/ImportFormat.lean diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index b86d4cb06dc29b..4283334aea5812 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -5,11 +5,11 @@ Authors: Michael Rothgang, Damiano Testa, Thomas R. Murrills -/ module -public meta import Lean.Elab.Command +public meta import ImportGraph.Imports.Pretty +public meta import Lean.Linter.Basic public meta import Std.Sync.Mutex public import Lean.Parser.Module public import Mathlib.Tactic.Linter.DirectoryDependency -public meta import Lean.Linter.Basic public import Std.Sync.Mutex /-! @@ -47,7 +47,7 @@ a module doc-string (unless the command is exempted for some reason). meta section -open Lean Elab Command Linter +open ImportGraph Lean Elab Command Linter namespace Mathlib.Linter @@ -233,34 +233,15 @@ public register_option linter.style.header.license : String := { descr := "The text required as the second line of the copyright header." } -/-- Extends `Import` with ``stx : TSyntax `Lean.Parser.Module.import`` to allow reporting at the -given import. -/ -structure ImportRef extends Import where - stx : TSyntax ``Parser.Module.import - -/-- Returns the module `Ident` (following `(public)? (meta)? import (all)?` of a given -`ImportRef`. -/ -def ImportRef.getIdent (i : ImportRef) : Ident := - match i.stx with - | `(Parser.Module.import| - $[public]? $[meta]? import $[all]? $n:ident) => n - | _ => ⟨.missing⟩ - -/-- Destructures header syntax (`(module)? (prelude)? $imports*`) into an array of `ImportRef`s. -/ -def headerToImportRefs (header : TSyntax ``Parser.Module.header) : Array ImportRef := - match header with - | `(Parser.Module.header| $[module%$moduleTk]? $[prelude]? $imports*) => - imports.filterMap fun - | stx@`(Parser.Module.import| - $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n:ident) => - some { - module := n.getId - importAll := allTk.isSome - isExported := publicTk.isSome || moduleTk.isNone - isMeta := metaTk.isSome - stx := ⟨stx⟩ } - | _ => none - | _ => #[] +/-- +Whether to reformat import blocks in the module system according to the style convention. Note that +this only has an effect if `linter.style.header` is `true` and the header is participating in the +module system. This does not remove redundant imports. +-/ +public register_option linter.style.header.imports : Bool := { + defValue := true + descr := "Whether to reformat import blocks according to the style convention." +} /-- Returns the `module` token from header syntax, if there is one. -/ def headerToModuleTk? (header : TSyntax ``Parser.Module.header) : Option Syntax := @@ -283,6 +264,7 @@ because they are files that test the linter. def headerTestFiles : NameSet := .ofList [ `MathlibTest.Linter.Header.Basic, `MathlibTest.Linter.Header.Fail, + `MathlibTest.Linter.Header.ImportFormat, `MathlibTest.Linter.Header.Verso, `MathlibTest.DirectoryDependencyLinter.Test] @@ -334,6 +316,28 @@ def duplicateImportsCheck (imports : Array ImportRef) : CommandElabM Unit := do else importsSoFar := importsSoFar.insert imp.toImport +/-- +If we are in the module system and `linter.style.header.imports` is `true`, reformat imports. +-/ +def formatImports (imports : Array (ImportRef × Import.Whitespace)) : CommandElabM Unit := do + unless + (← getEnv).header.isModule && getLinterValue linter.style.header.imports (← getLinterOptions) + do + return + let some (lastImportRef, _) := imports.back? | return + let impsRef := mkNullNode <| imports.map (·.1.stx) + let some (msg, errs) ← liftCoreM <| + Import.mkImportSuggestionMessage impsRef (imports.map (·.1.toImport)) imports + | return + -- Note: potentially, we should just bail if there are errors. + if errs.isEmpty then + -- Note: the widget nature of `diffGranularity := .word` effectively gives us a newline + -- before `{msg}`, meaning we don't need one here. + logWarningAt lastImportRef.stx m!"Imports can be reformatted:{msg}" + else + logWarningAt lastImportRef.stx m!"Imports can be reformatted, but some comments could not be \ + carried over. Please review the comment that will be inserted after the imports.\n{msg}" + section HeaderParser open Lean.ParseImports @@ -424,7 +428,9 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do -- Re-parse the header slowly, to get the leading whitespace and nice source locations for imports let (headerStx, s, log) ← Parser.parseHeader (Parser.mkInputContext map.source (← getFileName)) if log.hasErrors then return - let importRefs := headerToImportRefs headerStx + let importRefsWithWhitespace := headerToImportRefsWithWhitespace headerStx + formatImports importRefsWithWhitespace + let importRefs := importRefsWithWhitespace.map (·.1) -- Report on broad or duplicate imports. broadImportsCheck importRefs mainModule duplicateImportsCheck importRefs diff --git a/MathlibTest/Linter/Header/ImportFormat.lean b/MathlibTest/Linter/Header/ImportFormat.lean new file mode 100644 index 00000000000000..d64ed0effdf169 --- /dev/null +++ b/MathlibTest/Linter/Header/ImportFormat.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2026 Thomas R. Murrills. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas R. Murrills +-/ +module + +import Mathlib.Init +meta import Mathlib.Init + + + public meta import Mathlib.Init + +public import Mathlib.Init +import Lean.Elab.Command + +/-- +warning: Imports can be reformatted: + i̵m̵p̵o̵r̵t̵ ̵M̵a̵t̵h̵l̵i̵b̵.̵I̵n̵i̵t̵p̲u̲b̲l̲i̲c̲ meta import Mathlib.Init + public i̲m̲p̲o̲r̲t̲ ̲M̲a̲t̲h̲l̲i̲b̲.̲I̲n̲i̲t̲ + ̲ + ̲meta ̵ ̵import Mathlib.Init + p̵u̵b̵l̵i̵c̵ ̵import M̵a̵t̵h̵l̵i̵b̵.̵I̵n̵i̵t̵ + ̵i̵m̵p̵o̵r̵t̵ ̵Lean.Elab.Command + ̲i̲m̲p̲o̲r̲t̲ ̲M̲a̲t̲h̲l̲i̲b̲.̲I̲n̲i̲t̲ +-/ +#guard_msgs in +set_option linter.style.header true in +/-! -/ From 134e7ce6283889017b18e8cf15cd6a6de997d4a1 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 12 Oct 2026 14:25:11 -0400 Subject: [PATCH 02/16] chore: set_option --- Mathlib/Tactic/Linter/Header.lean | 15 +++++++++++---- MathlibTest/Linter/Header/ImportFormat.lean | 2 ++ 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 4283334aea5812..8277f4f12d92e5 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -240,7 +240,8 @@ module system. This does not remove redundant imports. -/ public register_option linter.style.header.imports : Bool := { defValue := true - descr := "Whether to reformat import blocks according to the style convention." + descr := "Whether to reformat module system import blocks according to the style convention when \ + `linter.style.header` is `true`." } /-- Returns the `module` token from header syntax, if there is one. -/ @@ -318,6 +319,8 @@ def duplicateImportsCheck (imports : Array ImportRef) : CommandElabM Unit := do /-- If we are in the module system and `linter.style.header.imports` is `true`, reformat imports. + +Note that this assumes the check for `linter.style.header` has already been performed. -/ def formatImports (imports : Array (ImportRef × Import.Whitespace)) : CommandElabM Unit := do unless @@ -329,14 +332,15 @@ def formatImports (imports : Array (ImportRef × Import.Whitespace)) : CommandEl let some (msg, errs) ← liftCoreM <| Import.mkImportSuggestionMessage impsRef (imports.map (·.1.toImport)) imports | return - -- Note: potentially, we should just bail if there are errors. + let note := .note m!"This linter can be disabled by writing \ + `set_option {linter.style.header.imports.name} false` just after the import block." if errs.isEmpty then -- Note: the widget nature of `diffGranularity := .word` effectively gives us a newline -- before `{msg}`, meaning we don't need one here. - logWarningAt lastImportRef.stx m!"Imports can be reformatted:{msg}" + logWarningAt lastImportRef.stx m!"Imports can be reformatted:{msg}{note}" else logWarningAt lastImportRef.stx m!"Imports can be reformatted, but some comments could not be \ - carried over. Please review the comment that will be inserted after the imports.\n{msg}" + carried over. Please review the comment that will be inserted after the imports.\n{msg}{note}" section HeaderParser @@ -380,6 +384,9 @@ partial def allowedHeaderParser : Parser := keyword "doc.verso.module", -- check last, otherwise it prevents hitting the ones it is a prefix of keyword "doc.verso", + keyword "linter.style.header.license", + keyword "linter.style.header.imports", + -- check last, otherwise it prevents hitting the ones it is a prefix of keyword "linter.style.header" -- for testing and downstream ] >> boolLit) diff --git a/MathlibTest/Linter/Header/ImportFormat.lean b/MathlibTest/Linter/Header/ImportFormat.lean index d64ed0effdf169..ad652d73034aec 100644 --- a/MathlibTest/Linter/Header/ImportFormat.lean +++ b/MathlibTest/Linter/Header/ImportFormat.lean @@ -23,6 +23,8 @@ warning: Imports can be reformatted: p̵u̵b̵l̵i̵c̵ ̵import M̵a̵t̵h̵l̵i̵b̵.̵I̵n̵i̵t̵ ̵i̵m̵p̵o̵r̵t̵ ̵Lean.Elab.Command ̲i̲m̲p̲o̲r̲t̲ ̲M̲a̲t̲h̲l̲i̲b̲.̲I̲n̲i̲t̲ + +Note: This linter can be disabled by writing `set_option linter.style.header.imports false` just after the import block. -/ #guard_msgs in set_option linter.style.header true in From b5a44f34660667df415a7367cee8e64f950ba0e6 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 12 Oct 2026 14:32:27 -0400 Subject: [PATCH 03/16] chore: test turning off --- Mathlib/Tactic/Linter/Header.lean | 1 + .../Linter/Header/ImportFormatOff.lean | 21 +++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 MathlibTest/Linter/Header/ImportFormatOff.lean diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 8277f4f12d92e5..47036805951424 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -266,6 +266,7 @@ def headerTestFiles : NameSet := .ofList [ `MathlibTest.Linter.Header.Basic, `MathlibTest.Linter.Header.Fail, `MathlibTest.Linter.Header.ImportFormat, + `MathlibTest.Linter.Header.ImportFormatOff, `MathlibTest.Linter.Header.Verso, `MathlibTest.DirectoryDependencyLinter.Test] diff --git a/MathlibTest/Linter/Header/ImportFormatOff.lean b/MathlibTest/Linter/Header/ImportFormatOff.lean new file mode 100644 index 00000000000000..24db04cb4eb31f --- /dev/null +++ b/MathlibTest/Linter/Header/ImportFormatOff.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2026 Thomas R. Murrills. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas R. Murrills +-/ +module + +import Mathlib.Init +meta import Mathlib.Init + + + public meta import Mathlib.Init + +public import Mathlib.Init +import Lean.Elab.Command + +set_option linter.style.header.imports false + +#guard_msgs in +set_option linter.style.header true in +/-! -/ From 760f90410194de1c53b2df95b9e51eb833c9db24 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 12 Oct 2026 14:48:55 -0400 Subject: [PATCH 04/16] chore: keep Metahlib.Tactic.Common ordering --- Mathlib/Tactic/Common.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index 4340fec1f141e1..baf96a23fb9b81 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -124,6 +124,9 @@ public import Mathlib.Util.WhatsNew public import Lean.Elab.Tactic.Try public meta import Lean.Meta.Tactic.Try.Collect +-- Preserve custom import ordering: +set_option linter.style.header.imports false + /-! # Common tactics, linters, and utilities From 60af689cb7ce828812f0f6cf0e8582ecd3b96980 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 12 Oct 2026 14:50:41 -0400 Subject: [PATCH 05/16] chore: fix unformatted imports that crept in --- .../Functor/Derived/RightDerivedCompositionCommShift.lean | 2 +- Mathlib/CategoryTheory/Linear/Yoneda.lean | 2 +- Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean b/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean index 14eea2b87a6c31..4586d8b4478799 100644 --- a/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean +++ b/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean @@ -5,8 +5,8 @@ Authors: Joël Riou -/ module -public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift +public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition /-! # Compatibility with shifts of the comparison morphism for the composition of right derived functors diff --git a/Mathlib/CategoryTheory/Linear/Yoneda.lean b/Mathlib/CategoryTheory/Linear/Yoneda.lean index a8324e48202675..7cfe55cc8c1e37 100644 --- a/Mathlib/CategoryTheory/Linear/Yoneda.lean +++ b/Mathlib/CategoryTheory/Linear/Yoneda.lean @@ -5,8 +5,8 @@ Authors: Kim Morrison -/ module -public import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic public import Mathlib.CategoryTheory.Linear.LinearFunctor +public import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic /-! # The Yoneda embedding for `R`-linear categories diff --git a/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean b/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean index ba72f6464a459a..c45f5d0dbf123b 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean @@ -10,9 +10,9 @@ public import Mathlib.LinearAlgebra.PiTensorProduct.Basic public import Mathlib.LinearAlgebra.TensorProduct.Map import Mathlib.Data.Set.Card +import Mathlib.LinearAlgebra.Finsupp.LinearCombination import Mathlib.LinearAlgebra.Quotient.Basic import Mathlib.SetTheory.Cardinal.Finite -import Mathlib.LinearAlgebra.Finsupp.LinearCombination /-! # Generators of multiple tensor products From 061d41c4523c1c13e2d95fdec704952fbd23a94e Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 12 Oct 2026 15:32:38 -0400 Subject: [PATCH 06/16] chore: restrict to mathlib for now? --- Mathlib/Tactic/Linter/Header.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 47036805951424..fddff73463c895 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -437,7 +437,9 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do let (headerStx, s, log) ← Parser.parseHeader (Parser.mkInputContext map.source (← getFileName)) if log.hasErrors then return let importRefsWithWhitespace := headerToImportRefsWithWhitespace headerStx - formatImports importRefsWithWhitespace + -- TODO: Enable this more broadly (Archive, etc., and downstream) once tooling is available. + if mainModule.getRoot == `Mathlib then + formatImports importRefsWithWhitespace let importRefs := importRefsWithWhitespace.map (·.1) -- Report on broad or duplicate imports. broadImportsCheck importRefs mainModule From c3b8c570dc0cac26e63daee9ae8e179871d81ca7 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 12 Oct 2026 15:34:04 -0400 Subject: [PATCH 07/16] chore: test files --- Mathlib/Tactic/Linter/Header.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index fddff73463c895..10da1f24823f44 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -437,8 +437,8 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do let (headerStx, s, log) ← Parser.parseHeader (Parser.mkInputContext map.source (← getFileName)) if log.hasErrors then return let importRefsWithWhitespace := headerToImportRefsWithWhitespace headerStx - -- TODO: Enable this more broadly (Archive, etc., and downstream) once tooling is available. - if mainModule.getRoot == `Mathlib then + -- TODO: Enable this more broadly (Archive, etc., and downstream) + if mainModule.getRoot == `Mathlib || headerTestFiles.contains mainModule then formatImports importRefsWithWhitespace let importRefs := importRefsWithWhitespace.map (·.1) -- Report on broad or duplicate imports. From d290f6b23281e09781b9a531065bc73a07557ca5 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Tue, 13 Oct 2026 17:05:19 -0400 Subject: [PATCH 08/16] chore: update drifting files --- Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean | 2 +- Mathlib/NumberTheory/NumberField/AdeleRing.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean b/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean index f3d223704f5753..464ed6c62c50d7 100644 --- a/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean @@ -5,9 +5,9 @@ Authors: Rémy Degenne -/ module +public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs -public import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym diff --git a/Mathlib/NumberTheory/NumberField/AdeleRing.lean b/Mathlib/NumberTheory/NumberField/AdeleRing.lean index ff287057a4d2be..1ec4ff0ba53a8f 100644 --- a/Mathlib/NumberTheory/NumberField/AdeleRing.lean +++ b/Mathlib/NumberTheory/NumberField/AdeleRing.lean @@ -5,8 +5,8 @@ Authors: Salvatore Mercuri, María Inés de Frutos-Fernández -/ module -public import Mathlib.NumberTheory.NumberField.InfiniteAdeleRing public import Mathlib.NumberTheory.NumberField.FiniteAdeleRing +public import Mathlib.NumberTheory.NumberField.InfiniteAdeleRing /-! # The adele ring of a number field From 042e06f7d9419ef0f8efe30f8f800769b05e52e8 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Wed, 14 Oct 2026 17:09:42 -0400 Subject: [PATCH 09/16] chore: update drift --- Mathlib/Analysis/LocallyConvex/Asymptotics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/LocallyConvex/Asymptotics.lean b/Mathlib/Analysis/LocallyConvex/Asymptotics.lean index b391ac749d3807..0dd65e8900bf32 100644 --- a/Mathlib/Analysis/LocallyConvex/Asymptotics.lean +++ b/Mathlib/Analysis/LocallyConvex/Asymptotics.lean @@ -5,8 +5,8 @@ Authors: Anatole Dedecker, Moritz Doll -/ module -public import Mathlib.Analysis.Asymptotics.TVS public import Mathlib.Analysis.Asymptotics.Basic +public import Mathlib.Analysis.Asymptotics.TVS public import Mathlib.Analysis.LocallyConvex.WithSeminorms /-! From c67bd00368715d3b856e07a241573539708c9229 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Sun, 18 Oct 2026 12:46:08 -0400 Subject: [PATCH 10/16] chore: update drifting files --- Mathlib/Algebra/Lie/Solvable.lean | 2 +- Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean | 2 +- .../SimpleGraph/Extremal/ErdosStoneSimonovits.lean | 1 - .../Manifold/VectorBundle/ContinuousAlternatingMap.lean | 4 ++-- 4 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Lie/Solvable.lean b/Mathlib/Algebra/Lie/Solvable.lean index 52702b3c575477..62a6d5f736bf29 100644 --- a/Mathlib/Algebra/Lie/Solvable.lean +++ b/Mathlib/Algebra/Lie/Solvable.lean @@ -6,8 +6,8 @@ Authors: Oliver Nash module public import Mathlib.Algebra.Lie.BaseChange -public import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic public import Mathlib.Algebra.Lie.Quotient +public import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic /-! # Solvable Lie algebras diff --git a/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean b/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean index 206e093b50b027..9b0550bfb15a3d 100644 --- a/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean +++ b/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean @@ -5,8 +5,8 @@ Authors: Jireh Loreaux -/ module -public import Mathlib.Analysis.Normed.Algebra.GelfandRadius public import Mathlib.Analysis.Calculus.Deriv.Basic +public import Mathlib.Analysis.Normed.Algebra.GelfandRadius public import Mathlib.Analysis.Normed.Algebra.Spectrum public import Mathlib.Analysis.Normed.Operator.Mul diff --git a/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean b/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean index deca0151b66100..6939f23c4b4516 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean @@ -10,7 +10,6 @@ public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite import Mathlib.Combinatorics.Pigeonhole import Mathlib.Combinatorics.SimpleGraph.Bipartite - import Mathlib.Tactic.LinearCombination /-! diff --git a/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean b/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean index fde053db96e12d..1de60de2fdd0d5 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean @@ -5,10 +5,10 @@ Authors: Sébastien Gouëzel -/ module +public import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.VectorBundle.Hom -public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable -public import Mathlib.Geometry.Manifold.Notation +public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap /-! # The bundle of alternating maps between `C^n` vector bundles over the same base space is `C^n` From f70a744f14557500e8588e9e3ccc70f5fa18099d Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 19 Oct 2026 11:41:27 -0400 Subject: [PATCH 11/16] chore: improve comment --- Mathlib/Tactic/Linter/Header.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 10916f921233c3..4371a6182f4432 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -336,8 +336,9 @@ def formatImports (imports : Array (ImportRef × Import.Whitespace)) : CommandEl let note := .note m!"This linter can be disabled by writing \ `set_option {linter.style.header.imports.name} false` just after the import block." if errs.isEmpty then - -- Note: the widget nature of `diffGranularity := .word` effectively gives us a newline - -- before `{msg}`, meaning we don't need one here. + -- Note: when `errs.isEmpty`, `Import.mkImportSuggestionMessage` gives us a clickable widget + -- that uses `diffGranularity := .word`. This effectively gives us a newline before `{msg}`, + -- meaning we don't need one after `reformatted:` here. logWarningAt lastImportRef.stx m!"Imports can be reformatted:{msg}{note}" else logWarningAt lastImportRef.stx m!"Imports can be reformatted, but some comments could not be \ From ccadc9896df5a3c40f0e87f7398e8b36b5ac7965 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 19 Oct 2026 20:02:27 -0400 Subject: [PATCH 12/16] feat: access library root path correctly --- Mathlib/Tactic/Linter/Header.lean | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 4371a6182f4432..0ea1768b1b8d06 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -176,6 +176,18 @@ public def copyrightHeaderChecks (copyright : String) (expectedLicense : String) output := output.push (toSyntax copyright "-/", s!"Copyright too short!") return output +/-- Given `modPath := foo/bar/A/B/C(.lean)` and a module name `A.B.C`, return `foo/bar/A.lean`. +Return `none` if the name components do not match the path components. -/ +def modPathToRootPath (modPath : System.FilePath) (modName : Name) : Option System.FilePath := + match modName with + | .str .anonymous root => do + guard <| modPath.fileStem == root + modPath.withExtension "lean" + | .str pre last => do + guard <| modPath.fileStem == last + modPathToRootPath (← modPath.parent) pre + | _ => none + /-- `isInLibraryRoot modName` returns `true` if `.lean` imports the file `modName`, where `` is the top-level component of `modName`. For example, for `Mathlib.Foo.Bar` this checks @@ -184,8 +196,8 @@ This is used by the `Header` linter as a heuristic of whether it should inspect so that the linter works in any project whose library root follows the standard Lean convention of being named after the top-level module. -/ -def isInLibraryRoot (modName : Name) : IO Bool := do - let rootPath := (modName.getRoot.toString : System.FilePath).addExtension "lean" +def isInLibraryRoot (modPath : System.FilePath) (modName : Name) : IO Bool := do + let some rootPath := modPathToRootPath modPath modName | return false if ← rootPath.pathExists then let res ← parseImports' (← IO.FS.readFile rootPath) "" return res.imports.any (·.module == modName) @@ -425,7 +437,7 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do match ← get with | some d => return d | none => - let val ← isInLibraryRoot mainModule + let val ← isInLibraryRoot (← getFileName) mainModule -- We cache the answer to avoid recomputing it on every command. The fill runs under the mutex -- so that concurrent (async) linter runs don't all miss the cache and each redundantly parse -- the library root file; `mainModule` is fixed for the duration of the elaboration. From b14eaae2b76c46c8242948684974e1a802289cc0 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Mon, 19 Oct 2026 20:48:45 -0400 Subject: [PATCH 13/16] fix: directory dependency fix? --- .../Tactic/Linter/DirectoryDependency.lean | 39 +++++++++---------- Mathlib/Tactic/Linter/Header.lean | 15 +++---- 2 files changed, 27 insertions(+), 27 deletions(-) diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index 720ed2be331a0a..fc2ee1e58fcab9 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -287,7 +287,8 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ Each key names a module prefix; modules matching that prefix may not import modules matching any of the prefixes in the corresponding list. Exceptions to these rules live in `overrideAllowedImportDirs` below. -/ -def forbiddenDirsPath : System.FilePath := "scripts" / "forbiddenDirs.json" +def forbiddenDirsPath (srcDir : System.FilePath) : System.FilePath := + srcDir / "scripts" / "forbiddenDirs.json" /-- The root modules of the libraries built from the mathlib repository itself. When elaborating one of their modules, the linter configuration file must be present. -/ @@ -309,10 +310,10 @@ outside `Mathlib/Algebra/Notation.lean`. This relation is read at runtime from `scripts/forbiddenDirs.json`, so that updating the configuration does not require recompiling this linter (and everything importing it). -/ -def forbiddenImportDirs : IO NamePrefixRel := do +def forbiddenImportDirs (srcDir : System.FilePath) : IO NamePrefixRel := do if let some rel ← forbiddenImportDirsCache.get then return rel - let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile forbiddenDirsPath) + let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile <| forbiddenDirsPath srcDir) let entries : Std.TreeMap String (Array String) ← IO.ofExcept <| fromJson? json let rel := NamePrefixRel.ofArray <| entries.toArray.flatMap fun (n₁, ns) ↦ ns.map fun n₂ ↦ (n₁.toName, n₂.toName) @@ -386,7 +387,8 @@ def checkBlocklist (env : Environment) (forbidden : NamePrefixRel) (mainModule : | none => none @[inherit_doc Mathlib.Linter.linter.directoryDependency] -public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array MessageData) := do +public def directoryDependencyCheck (srcDir : System.FilePath) (mainModule : Name) : + CommandElabM (Array MessageData) := do unless Linter.getLinterValue linter.directoryDependency (← Linter.getLinterOptions) do return #[] let env ← getEnv @@ -397,15 +399,12 @@ public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array Me let matchingPrefixes := mainModule.prefixes.filter (fun prf ↦ allowedImportDirs.containsKey prf) if matchingPrefixes.isEmpty then -- Otherwise, we fall back to the blocklist `forbiddenImportDirs`. - unless ← forbiddenDirsPath.pathExists do - -- When mathlib is used as a dependency, its configuration file is not available; - -- in that case, there is nothing to check. - -- Within mathlib itself, the file must exist: fail loudly if it does not. + unless ← (forbiddenDirsPath srcDir).pathExists do if mathlibRoots.contains mainModule.getRoot then - throwError "directoryDependency linter: configuration file '{forbiddenDirsPath}' \ - not found; was mathlib built from its root directory?" + throwError "directoryDependency linter: configuration file '{forbiddenDirsPath srcDir}' \ + not found." return #[] - if let some msg := checkBlocklist env (← forbiddenImportDirs) mainModule imports then + if let some msg := checkBlocklist env (← forbiddenImportDirs srcDir) mainModule imports then return #[msg] else return #[] else @@ -413,7 +412,7 @@ public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array Me -- from `Init`, `Lean` and `Std`, as well as imports in `Aesop`, `Qq`, `Plausible`, -- `ImportGraph`, `ProofWidgets` or `LeanSearchClient` (as these are imported in Tactic.Common). -- We also allow transitive imports of Mathlib.Init, as well as Mathlib.Init itself. - let initImports := (← findImports ("Mathlib" / "Init.lean")).append + let initImports := (← findImports (srcDir / "Mathlib" / "Init.lean")).append #[`Mathlib.Init, `Mathlib.Tactic.DeclarationNames] let exclude := [ `Init, `Std, `Lean, @@ -431,12 +430,12 @@ public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array Me if !allowedImportDirs.contains mainModule imported then let importPath := env.importPath imported let mut msg := m!"Module {mainModule} depends on {imported},\n\ - but is only allowed to import modules starting with one of \ - {allRules.toArray.qsort (·.toString < ·.toString)}.\n\ - Note: module {imported}" + but is only allowed to import modules starting with one of \ + {allRules.toArray.qsort (·.toString < ·.toString)}.\n\ + Note: module {imported}" let mut superseded := false match importPath.toList with - | [] => msg := msg ++ " is directly imported by this module" + | [] => msg := m!"{msg} is directly imported by this module" | a :: rest => -- Only add messages about imports that aren't themselves transitive imports of -- forbidden imports. @@ -444,14 +443,14 @@ public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array Me if !allowedImportDirs.contains mainModule a then superseded := true else - msg := msg ++ s!" is imported by {a},\n" + msg := m!"{msg} is imported by {a},\n" for dep in rest do if !allowedImportDirs.contains mainModule dep then superseded := true break - msg := msg ++ m!"which is imported by {dep},\n" - msg := msg ++ m!"which is imported by this module." - msg := msg ++ "(Exceptions can be added to `allowedImportDirs`.)" + msg := m!"{msg}which is imported by {dep},\n" + msg := m!"{msg}which is imported by this module.\n\ + (Exceptions can be added to `allowedImportDirs`.)" if !superseded then messages := messages.push msg return messages diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 0ea1768b1b8d06..2e857d55834ba2 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -196,8 +196,7 @@ This is used by the `Header` linter as a heuristic of whether it should inspect so that the linter works in any project whose library root follows the standard Lean convention of being named after the top-level module. -/ -def isInLibraryRoot (modPath : System.FilePath) (modName : Name) : IO Bool := do - let some rootPath := modPathToRootPath modPath modName | return false +def isInLibraryRoot (rootPath : System.FilePath) (modName : Name) : IO Bool := do if ← rootPath.pathExists then let res ← parseImports' (← IO.FS.readFile rootPath) "" return res.imports.any (·.module == modName) @@ -433,11 +432,12 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do and any necessary `set_option` commands.\n\ Please, add a module doc-string (`/-! ... -/`) before `{stx}`.\ {.hint' m!"Type `m(odule docstring) + [tab]` to insert a template via snippet."}" + let some rootPath := modPathToRootPath (← getFileName) mainModule | return let inLibraryRoot? ← inLibraryRootMutex.atomically do match ← get with | some d => return d | none => - let val ← isInLibraryRoot (← getFileName) mainModule + let val ← isInLibraryRoot rootPath mainModule -- We cache the answer to avoid recomputing it on every command. The fill runs under the mutex -- so that concurrent (async) linter runs don't all miss the cache and each redundantly parse -- the library root file; `mainModule` is fixed for the duration of the elaboration. @@ -457,10 +457,11 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do -- Report on broad or duplicate imports. broadImportsCheck importRefs mainModule duplicateImportsCheck importRefs - let errors ← directoryDependencyCheck mainModule - if errors.size > 0 then - Linter.logLint linter.directoryDependency (importRefs.back?.elim headerStx (·.stx)) <| - m!"\n\n".joinSep errors.toList + if let some srcDir := rootPath.parent then + let errors ← directoryDependencyCheck srcDir mainModule + if errors.size > 0 then + Linter.logLint linter.directoryDependency (importRefs.back?.elim headerStx (·.stx)) <| + m!"\n\n".joinSep errors.toList -- Report any errors about the copyright line. if mainModule != `Mathlib.Init && mainModule != `Mathlib.Tactic then let expectedLicense := linter.style.header.license.get (← getOptions) From ab53ac2fe49935d8c02346ade151b5307abaf5e9 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Tue, 20 Oct 2026 00:03:57 -0400 Subject: [PATCH 14/16] chore: `getD "."` for lake env --- Mathlib/Tactic/Linter/Header.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 2e857d55834ba2..f05602c7d147be 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -457,11 +457,11 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do -- Report on broad or duplicate imports. broadImportsCheck importRefs mainModule duplicateImportsCheck importRefs - if let some srcDir := rootPath.parent then - let errors ← directoryDependencyCheck srcDir mainModule - if errors.size > 0 then - Linter.logLint linter.directoryDependency (importRefs.back?.elim headerStx (·.stx)) <| - m!"\n\n".joinSep errors.toList + let srcDir := rootPath.parent.getD "." + let errors ← directoryDependencyCheck srcDir mainModule + if errors.size > 0 then + Linter.logLint linter.directoryDependency (importRefs.back?.elim headerStx (·.stx)) <| + m!"\n\n".joinSep errors.toList -- Report any errors about the copyright line. if mainModule != `Mathlib.Init && mainModule != `Mathlib.Tactic then let expectedLicense := linter.style.header.license.get (← getOptions) From 1e14c97add062b8cbc914fa65bfa8fd3516826dc Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Tue, 20 Oct 2026 01:36:44 -0400 Subject: [PATCH 15/16] chore: `scripts/runSkimmer.sh` --- .../Homology/HomotopyCategory/HomComplexShift.lean | 2 +- Mathlib/Basic/Logic/Basic.lean | 4 ++-- Mathlib/Init.lean | 8 ++++---- Mathlib/Lean/CoreM.lean | 2 +- Mathlib/Lean/Json.lean | 2 +- Mathlib/Lean/Meta/CongrTheorems.lean | 2 +- Mathlib/Lean/Meta/DiscrTree.lean | 2 +- Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean | 2 +- Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean | 2 +- Mathlib/Order/Notation.lean | 2 +- Mathlib/Tactic/AdaptationNote.lean | 2 +- Mathlib/Tactic/Bound/Attribute.lean | 2 +- Mathlib/Tactic/CategoryTheory/Coherence.lean | 2 +- Mathlib/Tactic/ClickSuggestions.lean | 2 +- Mathlib/Tactic/ClickSuggestions/SectionState.lean | 2 +- Mathlib/Tactic/ClickSuggestions/Util.lean | 6 +++--- Mathlib/Tactic/DeclarationNames.lean | 2 +- Mathlib/Tactic/DepRewrite.lean | 2 +- Mathlib/Tactic/Eval.lean | 2 +- Mathlib/Tactic/FunProp/Core.lean | 2 +- Mathlib/Tactic/FunProp/Types.lean | 2 +- Mathlib/Tactic/GrindAttrs.lean | 2 +- Mathlib/Tactic/Linter/AuxLemma.lean | 2 +- Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean | 2 +- Mathlib/Tactic/Linter/DocPrime.lean | 2 +- Mathlib/Tactic/Linter/DocString.lean | 4 ++-- Mathlib/Tactic/Linter/EmptyLine.lean | 2 +- Mathlib/Tactic/Linter/FlexibleLinter.lean | 2 +- Mathlib/Tactic/Linter/HashCommandLinter.lean | 2 +- Mathlib/Tactic/Linter/InternalConstructor.lean | 2 +- Mathlib/Tactic/Linter/Multigoal.lean | 2 +- Mathlib/Tactic/Linter/OldObtain.lean | 2 +- Mathlib/Tactic/Linter/Style.lean | 6 +++--- Mathlib/Tactic/Linter/UnusedInstancesInType.lean | 4 ++-- Mathlib/Tactic/Linter/UnusedTactic.lean | 2 +- Mathlib/Tactic/Linter/UnusedTacticExtension.lean | 2 +- Mathlib/Tactic/Matrix/MulExpand.lean | 2 +- Mathlib/Tactic/MinImports.lean | 2 +- Mathlib/Tactic/Nontriviality/Core.lean | 4 ++-- Mathlib/Tactic/NormNum/Core.lean | 2 +- Mathlib/Tactic/NormNum/NatLog.lean | 2 +- Mathlib/Tactic/NormNum/Pow.lean | 2 +- Mathlib/Tactic/SetLike.lean | 2 +- Mathlib/Tactic/TacticAnalysis.lean | 2 +- Mathlib/Tactic/Tauto.lean | 2 +- Mathlib/Tactic/Widget/Calc.lean | 2 +- Mathlib/Tactic/Widget/CommDiag.lean | 2 +- Mathlib/Tactic/Widget/Conv.lean | 2 +- Mathlib/Tactic/Widget/LibraryRewrite.lean | 4 ++-- Mathlib/Tactic/Widget/SelectPanelUtils.lean | 2 +- Mathlib/Tactic/Widget/StringDiagram.lean | 4 ++-- Mathlib/Util/AtomM.lean | 2 +- Mathlib/Util/Notation3.lean | 2 +- Mathlib/Util/PrintSorries.lean | 2 +- Mathlib/Util/Qq.lean | 2 +- Mathlib/Util/SynthesizeUsing.lean | 2 +- 56 files changed, 69 insertions(+), 69 deletions(-) diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean index 6faace7d9609d0..fed2951bafd707 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean @@ -7,8 +7,8 @@ module public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex public import Mathlib.Algebra.Homology.HomotopyCategory.Shift -public import Mathlib.CategoryTheory.Shift.ShiftedHom public import Mathlib.Algebra.Module.Equiv.Basic +public import Mathlib.CategoryTheory.Shift.ShiftedHom public import Mathlib.Tactic.Linarith /-! # Shifting cochains diff --git a/Mathlib/Basic/Logic/Basic.lean b/Mathlib/Basic/Logic/Basic.lean index 672430cad17ed0..873da0354e2fb0 100644 --- a/Mathlib/Basic/Logic/Basic.lean +++ b/Mathlib/Basic/Logic/Basic.lean @@ -5,10 +5,10 @@ Authors: Jeremy Avigad, Leonardo de Moura -/ module -public import Batteries.Logic -public import Batteries.Util.LibraryNote public meta import Mathlib.Lean.Meta.Simp public meta import Mathlib.Tactic.Attr.Register +public import Batteries.Logic +public import Batteries.Util.LibraryNote /-! # Basic logic properties diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean index 068997e6b342c8..597a4b7b3ae705 100644 --- a/Mathlib/Init.lean +++ b/Mathlib/Init.lean @@ -1,11 +1,7 @@ module -- shake: keep-all, shake: keep-downstream --- This import makes the `alias` command available globally. -public import Batteries.Tactic.Alias -- This import makes the `#help` command available globally. public meta import Batteries.Tactic.HelpCmd --- This import makes the `proof_wanted` command available globally. -public import Batteries.Util.ProofWanted -- This import makes the `#redundant_imports`/`#min_imports`/`#find_home`/`#import_diff` commands -- available globally. public meta import ImportGraph.Tools @@ -43,6 +39,10 @@ public meta import Mathlib.Tactic.TacticAnalysis.Declarations public meta import Mathlib.Tactic.TypeStar -- This import makes the binder plicity code action available globally public meta import Mathlib.Util.CodeActions +-- This import makes the `alias` command available globally. +public import Batteries.Tactic.Alias +-- This import makes the `proof_wanted` command available globally. +public import Batteries.Util.ProofWanted /-! This is the root file in Mathlib: it is imported by virtually *all* Mathlib files. diff --git a/Mathlib/Lean/CoreM.lean b/Mathlib/Lean/CoreM.lean index a64a7da261cfe8..5676cf38e7c50d 100644 --- a/Mathlib/Lean/CoreM.lean +++ b/Mathlib/Lean/CoreM.lean @@ -5,8 +5,8 @@ Authors: Kim Morrison -/ module -public import Mathlib.Init public import Lean.CoreM +public import Mathlib.Init /-! # Additional functions using `CoreM` state. diff --git a/Mathlib/Lean/Json.lean b/Mathlib/Lean/Json.lean index 378592fb19d195..ab703755b70b86 100644 --- a/Mathlib/Lean/Json.lean +++ b/Mathlib/Lean/Json.lean @@ -5,8 +5,8 @@ Authors: Eric Wieser -/ module -public import Mathlib.Init public import Lean.Data.Json.FromToJson.Basic +public import Mathlib.Init /-! # Json serialization typeclass for `PUnit` & `Fin n` & `Subtype p` diff --git a/Mathlib/Lean/Meta/CongrTheorems.lean b/Mathlib/Lean/Meta/CongrTheorems.lean index 4a8c7889db5928..23580de0cef924 100644 --- a/Mathlib/Lean/Meta/CongrTheorems.lean +++ b/Mathlib/Lean/Meta/CongrTheorems.lean @@ -5,9 +5,9 @@ Authors: Kyle Miller -/ module +public meta import Lean.Meta.CongrTheorems public meta import Lean.Meta.Tactic.Refl public meta import Mathlib.Basic.IsEmpty.Defs -public meta import Lean.Meta.CongrTheorems public import Mathlib.Basic.IsEmpty.Defs /-! diff --git a/Mathlib/Lean/Meta/DiscrTree.lean b/Mathlib/Lean/Meta/DiscrTree.lean index 257081b6d7a0f1..3359a3ca796523 100644 --- a/Mathlib/Lean/Meta/DiscrTree.lean +++ b/Mathlib/Lean/Meta/DiscrTree.lean @@ -5,10 +5,10 @@ Authors: Kim Morrison -/ module -public import Mathlib.Init public import Lean.Meta.Basic public import Lean.Meta.DiscrTree.Main public import Lean.Meta.DiscrTree.Types +public import Mathlib.Init /-! # Additions to `Lean.Meta.DiscrTree` diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean index 8007904d8b9179..a8e722d831385a 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean @@ -5,8 +5,8 @@ Authors: Jovan Gerbscheid -/ module -public import Mathlib.Init public import Lean.Meta.Basic +public import Mathlib.Init /-! # Basic Definitions for `RefinedDiscrTree` diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean index f88533d8c44fd0..166f5eb0220049 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean @@ -5,10 +5,10 @@ Authors: Jovan Gerbscheid -/ module +public import Lean.Linter.Deprecated public import Mathlib.Lean.Meta.RefinedDiscrTree.Basic import Lean.Meta.CompletionName -public import Lean.Linter.Deprecated /-! # Constructing a RefinedDiscrTree diff --git a/Mathlib/Order/Notation.lean b/Mathlib/Order/Notation.lean index 813292397a956b..ff58e9afe6128b 100644 --- a/Mathlib/Order/Notation.lean +++ b/Mathlib/Order/Notation.lean @@ -7,9 +7,9 @@ module public meta import Lean.PrettyPrinter.Delaborator.Builtins public meta import Mathlib.Lean.PrettyPrinter.Delaborator +public meta import Qq public import Mathlib.Tactic.Simps public import Mathlib.Tactic.ToDual -public meta import Qq /-! # Notation classes for lattice operations diff --git a/Mathlib/Tactic/AdaptationNote.lean b/Mathlib/Tactic/AdaptationNote.lean index 71cfa35f1aaad8..ce914c2a33f486 100644 --- a/Mathlib/Tactic/AdaptationNote.lean +++ b/Mathlib/Tactic/AdaptationNote.lean @@ -6,10 +6,10 @@ Authors: Kyle Miller module public meta import Lean.Meta.Tactic.TryThis +public meta import Lean.Meta.TryThis -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Meta.TryThis /-! # Adaptation notes diff --git a/Mathlib/Tactic/Bound/Attribute.lean b/Mathlib/Tactic/Bound/Attribute.lean index c23f44494301e8..63cc475ec120f2 100644 --- a/Mathlib/Tactic/Bound/Attribute.lean +++ b/Mathlib/Tactic/Bound/Attribute.lean @@ -6,8 +6,8 @@ Authors: Geoffrey Irving module public meta import Aesop -public import Mathlib.Tactic.Bound.Init public meta import Qq +public import Mathlib.Tactic.Bound.Init /-! # The `bound` attribute diff --git a/Mathlib/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean index 1a8cf863352e33..1d19614636e42e 100644 --- a/Mathlib/Tactic/CategoryTheory/Coherence.lean +++ b/Mathlib/Tactic/CategoryTheory/Coherence.lean @@ -6,8 +6,8 @@ Authors: Kim Morrison, Yuma Mizuno, Oleksandr Manzyuk module public meta import Lean.Meta.Tactic.Congr -public import Mathlib.CategoryTheory.Monoidal.Free.Basic public meta import Mathlib.Lean.Meta +public import Mathlib.CategoryTheory.Monoidal.Free.Basic public import Mathlib.Tactic.CategoryTheory.BicategoryCoherence public import Mathlib.Tactic.CategoryTheory.MonoidalComp diff --git a/Mathlib/Tactic/ClickSuggestions.lean b/Mathlib/Tactic/ClickSuggestions.lean index 072557f0efb351..4bc1d97e9e35e3 100644 --- a/Mathlib/Tactic/ClickSuggestions.lean +++ b/Mathlib/Tactic/ClickSuggestions.lean @@ -6,9 +6,9 @@ Authors: Jovan Gerbscheid module public meta import Lean.Server.FileWorker.RequestHandling +public meta import Lean.Widget.InteractiveGoal public meta import Mathlib.Lean.GoalsLocation public meta import Mathlib.Lean.Meta.KAbstractPositions -public meta import Lean.Widget.InteractiveGoal public import Mathlib.Tactic.ClickSuggestions.TryPremises public import Mathlib.Tactic.ClickSuggestions.Unfold public import ProofWidgets.Component.OfRpcMethod diff --git a/Mathlib/Tactic/ClickSuggestions/SectionState.lean b/Mathlib/Tactic/ClickSuggestions/SectionState.lean index b5c0eac219b0ae..710ab270988c3c 100644 --- a/Mathlib/Tactic/ClickSuggestions/SectionState.lean +++ b/Mathlib/Tactic/ClickSuggestions/SectionState.lean @@ -5,9 +5,9 @@ Authors: Jovan Gerbscheid -/ module +public meta import ProofWidgets.Component.FilterDetails public meta import ProofWidgets.Util public import Mathlib.Tactic.ClickSuggestions.Util -public meta import ProofWidgets.Component.FilterDetails /-! # Infrastructure for searching and displaying sets of lemmas diff --git a/Mathlib/Tactic/ClickSuggestions/Util.lean b/Mathlib/Tactic/ClickSuggestions/Util.lean index e692aa7ea91d36..2501a35cb2a417 100644 --- a/Mathlib/Tactic/ClickSuggestions/Util.lean +++ b/Mathlib/Tactic/ClickSuggestions/Util.lean @@ -6,15 +6,15 @@ Authors: Jovan Gerbscheid module public meta import Lean.PrettyPrinter.Delaborator.Builtins +public meta import Lean.Server.Utils public meta import Mathlib.Data.String.Defs +public meta import ProofWidgets.Component.MakeEditLink +public meta import ProofWidgets.Component.RefreshComponent public import Batteries.Tactic.PermuteGoals -public meta import Lean.Server.Utils public import Mathlib.Tactic.DepRewrite public import Mathlib.Tactic.GRewrite public import Mathlib.Tactic.NthRewrite public import Mathlib.Tactic.SimpRw -public meta import ProofWidgets.Component.MakeEditLink -public meta import ProofWidgets.Component.RefreshComponent /-! # Various utilities used in `#click_suggestions` diff --git a/Mathlib/Tactic/DeclarationNames.lean b/Mathlib/Tactic/DeclarationNames.lean index 03a508f99f5b3f..bd71ca21e32903 100644 --- a/Mathlib/Tactic/DeclarationNames.lean +++ b/Mathlib/Tactic/DeclarationNames.lean @@ -6,11 +6,11 @@ Authors: Damiano Testa, Moritz Firsching module public meta import Lean.DeclarationRange +public meta import Lean.Message public meta import Lean.ResolveName -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! This file contains functions that are used by multiple linters. diff --git a/Mathlib/Tactic/DepRewrite.lean b/Mathlib/Tactic/DepRewrite.lean index 881b0560442d1b..d59439642e94b5 100644 --- a/Mathlib/Tactic/DepRewrite.lean +++ b/Mathlib/Tactic/DepRewrite.lean @@ -5,11 +5,11 @@ Authors: Aaron Liu, Wojciech Nawrocki -/ module +public meta import Lean.Elab.ConfigEval public meta import Lean.Elab.ConfigEval.Basic public meta import Lean.Elab.Tactic.Conv.Basic public meta import Lean.Elab.Tactic.Rewrite public meta import Lean.Elab.Tactic.Simp -public meta import Lean.Elab.ConfigEval meta import Lean.Elab.ConfigEval.DeriveEvalExpr meta import Lean.Elab.ConfigEval.DeriveEvalTerm diff --git a/Mathlib/Tactic/Eval.lean b/Mathlib/Tactic/Eval.lean index 062afd26c1ba90..1a22bf8fce90fa 100644 --- a/Mathlib/Tactic/Eval.lean +++ b/Mathlib/Tactic/Eval.lean @@ -5,8 +5,8 @@ Authors: Eric Wieser -/ module -public import Mathlib.Init public meta import Qq.Macro +public import Mathlib.Init /-! # The `eval%` term elaborator diff --git a/Mathlib/Tactic/FunProp/Core.lean b/Mathlib/Tactic/FunProp/Core.lean index 8604dd4cbe62f8..ac69d279b8e3be 100644 --- a/Mathlib/Tactic/FunProp/Core.lean +++ b/Mathlib/Tactic/FunProp/Core.lean @@ -9,9 +9,9 @@ public meta import Mathlib.Lean.Expr.Basic public meta import Mathlib.Tactic.FunProp.Theorems public meta import Mathlib.Tactic.FunProp.ToBatteries public meta import Mathlib.Tactic.FunProp.Types +public meta import Qq public import Batteries.Tactic.Exact public import Mathlib.Tactic.FunProp.Theorems -public meta import Qq /-! # Tactic `fun_prop` for proving function properties like `Continuous f`, `Differentiable ℝ f`, ... diff --git a/Mathlib/Tactic/FunProp/Types.lean b/Mathlib/Tactic/FunProp/Types.lean index ab4c755362bbda..032fe1ef9a5838 100644 --- a/Mathlib/Tactic/FunProp/Types.lean +++ b/Mathlib/Tactic/FunProp/Types.lean @@ -5,9 +5,9 @@ Authors: Tomáš Skřivan -/ module +public meta import Lean.Meta.Tactic.Simp public meta import Mathlib.Lean.Meta.RefinedDiscrTree.Basic public meta import Mathlib.Tactic.FunProp.FunctionData -public meta import Lean.Meta.Tactic.Simp /-! ## `funProp` diff --git a/Mathlib/Tactic/GrindAttrs.lean b/Mathlib/Tactic/GrindAttrs.lean index 21e0124caa133b..44d47e61d0c656 100644 --- a/Mathlib/Tactic/GrindAttrs.lean +++ b/Mathlib/Tactic/GrindAttrs.lean @@ -7,9 +7,9 @@ Authors: Floris van Doorn module public import Lean.Meta.Tactic.Grind.RegisterCommand +public import Std.Data.HashSet.Basic import Mathlib.Init -public import Std.Data.HashSet.Basic /-! # Custom grind-sets diff --git a/Mathlib/Tactic/Linter/AuxLemma.lean b/Mathlib/Tactic/Linter/AuxLemma.lean index ac1728bd645dd7..07626f64d3c33b 100644 --- a/Mathlib/Tactic/Linter/AuxLemma.lean +++ b/Mathlib/Tactic/Linter/AuxLemma.lean @@ -6,10 +6,10 @@ Authors: Kim Morrison module public meta import Lean.Elab.Command +public meta import Lean.Message -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! # The `auxLemma` linter diff --git a/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean b/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean index 475d172bc1adc8..fcc921163974f1 100644 --- a/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean +++ b/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa, Jeremy Tan, Adomas Baliuka module public meta import Lean.Elab.Command +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # Linter against deprecated syntax diff --git a/Mathlib/Tactic/Linter/DocPrime.lean b/Mathlib/Tactic/Linter/DocPrime.lean index 0e2c30e6111949..4712681ac2d123 100644 --- a/Mathlib/Tactic/Linter/DocPrime.lean +++ b/Mathlib/Tactic/Linter/DocPrime.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module public meta import Lean.Elab.Command +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # The "docPrime" linter diff --git a/Mathlib/Tactic/Linter/DocString.lean b/Mathlib/Tactic/Linter/DocString.lean index 151b457db2772e..114f7141f8b864 100644 --- a/Mathlib/Tactic/Linter/DocString.lean +++ b/Mathlib/Tactic/Linter/DocString.lean @@ -5,12 +5,12 @@ Authors: Michael Rothgang, Damiano Testa -/ module +public meta import Lean.DocString.Parser +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep public meta import Std.Data.Iterators.Combinators.Zip -public meta import Lean.DocString.Parser -public meta import Lean.Parser.Command meta import Std.Data.Iterators.Producers.Range diff --git a/Mathlib/Tactic/Linter/EmptyLine.lean b/Mathlib/Tactic/Linter/EmptyLine.lean index 5b87f7645d65f5..9ac5bdc0dcfdad 100644 --- a/Mathlib/Tactic/Linter/EmptyLine.lean +++ b/Mathlib/Tactic/Linter/EmptyLine.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # The "emptyLine" linter diff --git a/Mathlib/Tactic/Linter/FlexibleLinter.lean b/Mathlib/Tactic/Linter/FlexibleLinter.lean index dc034cb71da2b0..c58712a3355a73 100644 --- a/Mathlib/Tactic/Linter/FlexibleLinter.lean +++ b/Mathlib/Tactic/Linter/FlexibleLinter.lean @@ -9,10 +9,10 @@ public meta import Lean.Elab.Command public meta import Lean.Elab.InfoTree.Util public meta import Lean.Elab.Tactic.Simp public meta import Lean.Meta.Tactic.TryThis +public meta import Lean.Parser.Term -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Term /-! # The "flexible" linter diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index 1252410425e7bb..4a47d7be892b58 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module public meta import Lean.Elab.Command +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # `#`-command linter diff --git a/Mathlib/Tactic/Linter/InternalConstructor.lean b/Mathlib/Tactic/Linter/InternalConstructor.lean index 37a73315a2efcc..f26d9e53e182f2 100644 --- a/Mathlib/Tactic/Linter/InternalConstructor.lean +++ b/Mathlib/Tactic/Linter/InternalConstructor.lean @@ -7,10 +7,10 @@ module public meta import Lean.Elab.InfoTree.Util public meta import Lean.Linter.Basic +public meta import Lean.Message -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! # Linting against internal constructors diff --git a/Mathlib/Tactic/Linter/Multigoal.lean b/Mathlib/Tactic/Linter/Multigoal.lean index 55abfd7d84f995..71833faf100a08 100644 --- a/Mathlib/Tactic/Linter/Multigoal.lean +++ b/Mathlib/Tactic/Linter/Multigoal.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module public meta import Lean.Elab.Command +public meta import Lean.Parser.Term -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Term /-! # The "multiGoal" linter diff --git a/Mathlib/Tactic/Linter/OldObtain.lean b/Mathlib/Tactic/Linter/OldObtain.lean index c13f1a8b012aa0..0718424902565f 100644 --- a/Mathlib/Tactic/Linter/OldObtain.lean +++ b/Mathlib/Tactic/Linter/OldObtain.lean @@ -6,10 +6,10 @@ Authors: Michael Rothgang module public meta import Lean.Elab.Command +public meta import Lean.Message -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! # The `oldObtain` linter, against stream-of-consciousness `obtain` diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean index 36630d3f15eb10..d1cce77d20044b 100644 --- a/Mathlib/Tactic/Linter/Style.lean +++ b/Mathlib/Tactic/Linter/Style.lean @@ -5,13 +5,13 @@ Authors: Michael Rothgang -/ module +public meta import Batteries.Tactic.Lint.Basic +public meta import Batteries.Util.ExtendedBinder public meta import Lean.Elab.Command +public meta import Lean.Parser.Module -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Batteries.Tactic.Lint.Basic -public meta import Batteries.Util.ExtendedBinder -public meta import Lean.Parser.Module public import Mathlib.Tactic.DeclarationNames meta import Lean.Parser.Command diff --git a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean index 4c4babb8887807..e3837eae63d586 100644 --- a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean +++ b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean @@ -6,12 +6,12 @@ Authors: Thomas R. Murrills module public meta import Batteries.Lean.Position +public meta import Batteries.Tactic.Lint.Basic +public meta import Batteries.Tactic.Lint.Misc public meta import Lean.Linter.Basic public meta import Mathlib.Lean.Elab.InfoTree public meta import Mathlib.Lean.Environment public meta import Mathlib.Lean.Expr.Basic -public meta import Batteries.Tactic.Lint.Basic -public meta import Batteries.Tactic.Lint.Misc -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public import Mathlib.Tactic.Linter.Header -- shake: keep diff --git a/Mathlib/Tactic/Linter/UnusedTactic.lean b/Mathlib/Tactic/Linter/UnusedTactic.lean index 4d6901e782b005..e167b535bcf6a2 100644 --- a/Mathlib/Tactic/Linter/UnusedTactic.lean +++ b/Mathlib/Tactic/Linter/UnusedTactic.lean @@ -6,11 +6,11 @@ Authors: Damiano Testa module public meta import Lean.Elab.InfoTree.Util +public meta import Lean.Parser.Syntax -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep public import Batteries.Tactic.Unreachable -public meta import Lean.Parser.Syntax public import Mathlib.Tactic.Linter.UnusedTacticExtension /-! diff --git a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean index 806f763ec54e90..728809ffb2fa67 100644 --- a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean +++ b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module +public meta import Lean.Exception -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Exception /-! This file defines the environment extension to keep track of which tactics are allowed to leave diff --git a/Mathlib/Tactic/Matrix/MulExpand.lean b/Mathlib/Tactic/Matrix/MulExpand.lean index c0f7fd6453654a..03e7216b79dd74 100644 --- a/Mathlib/Tactic/Matrix/MulExpand.lean +++ b/Mathlib/Tactic/Matrix/MulExpand.lean @@ -7,9 +7,9 @@ module public meta import Mathlib.Tactic.Matrix.ListMatrix public meta import Mathlib.Util.Qq +public meta import Qq public import Batteries.Logic -- shake: keep (Qq dependency) public import Mathlib.Init -public meta import Qq /-! # Expansion of products of list matrices diff --git a/Mathlib/Tactic/MinImports.lean b/Mathlib/Tactic/MinImports.lean index a150d26813dd00..cf4d6471aab893 100644 --- a/Mathlib/Tactic/MinImports.lean +++ b/Mathlib/Tactic/MinImports.lean @@ -7,12 +7,12 @@ module public meta import ImportGraph.Imports.Redundant public meta import ImportGraph.Imports.RequiredModules +public meta import Lean.Elab.DeclModifiers public meta import Lean.Elab.DefView public meta import Lean.Util.CollectAxioms -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Elab.DeclModifiers /-! # `#min_imports in` a command to find minimal imports diff --git a/Mathlib/Tactic/Nontriviality/Core.lean b/Mathlib/Tactic/Nontriviality/Core.lean index 1b7177ed4aa9cb..12474b89c419e9 100644 --- a/Mathlib/Tactic/Nontriviality/Core.lean +++ b/Mathlib/Tactic/Nontriviality/Core.lean @@ -7,11 +7,11 @@ module public meta import Lean.Elab.Tactic.Meta public meta import Lean.Elab.Tactic.SolveByElim +public meta import Qq.Macro public meta import Qq.MetaM +public meta import Qq.Typ public import Mathlib.Basic.Nontrivial.Basic -- shake: keep (tactic dependency) public import Mathlib.Tactic.Attr.Register -- shake: keep (tactic dependency) -public meta import Qq.Macro -public meta import Qq.Typ /-! # The `nontriviality` tactic. -/ diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean index ad1c541ee293ef..68abff57947d0b 100644 --- a/Mathlib/Tactic/NormNum/Core.lean +++ b/Mathlib/Tactic/NormNum/Core.lean @@ -5,10 +5,10 @@ Authors: Mario Carneiro -/ module +public meta import Lean.Elab.Tactic.Try -- shake: keep (`register_try?_tactic` command dependency) public meta import Lean.Meta.Tactic.Try.Collect public meta import Mathlib.Lean.Expr.Rat public meta import Mathlib.Util.Qq -public meta import Lean.Elab.Tactic.Try -- shake: keep (`register_try?_tactic` command dependency) public import Mathlib.Tactic.NormNum.Result /-! diff --git a/Mathlib/Tactic/NormNum/NatLog.lean b/Mathlib/Tactic/NormNum/NatLog.lean index e6a0163bc4e5ad..417faf980b1e3f 100644 --- a/Mathlib/Tactic/NormNum/NatLog.lean +++ b/Mathlib/Tactic/NormNum/NatLog.lean @@ -5,8 +5,8 @@ Authors: Kyle Miller, Andreas Gittis -/ module -public meta import Mathlib.Data.Nat.Log public meta import Batteries.Lean.Expr +public meta import Mathlib.Data.Nat.Log public import Mathlib.Data.Nat.Log public import Mathlib.Tactic.NormNum diff --git a/Mathlib/Tactic/NormNum/Pow.lean b/Mathlib/Tactic/NormNum/Pow.lean index c8b8d28b70111f..c2ea38afea1ed3 100644 --- a/Mathlib/Tactic/NormNum/Pow.lean +++ b/Mathlib/Tactic/NormNum/Pow.lean @@ -5,9 +5,9 @@ Authors: Mario Carneiro, Thomas Murrills -/ module +public meta import Mathlib.Util.Qq public import Mathlib.Data.Int.Cast.Lemmas public import Mathlib.Tactic.NormNum.Basic -public meta import Mathlib.Util.Qq /-! ## `norm_num` plugin for `^`. diff --git a/Mathlib/Tactic/SetLike.lean b/Mathlib/Tactic/SetLike.lean index 1d51f675ff329a..1c6436ac5f5bb1 100644 --- a/Mathlib/Tactic/SetLike.lean +++ b/Mathlib/Tactic/SetLike.lean @@ -5,9 +5,9 @@ Authors: Jireh Loreaux -/ module -public meta import Batteries.Util.LibraryNote public meta import Aesop.Frontend public meta import Aesop.Frontend.Basic +public meta import Batteries.Util.LibraryNote public import Batteries.Util.LibraryNote import Mathlib.Init diff --git a/Mathlib/Tactic/TacticAnalysis.lean b/Mathlib/Tactic/TacticAnalysis.lean index 56550c5ed03368..cc666b0e9a0815 100644 --- a/Mathlib/Tactic/TacticAnalysis.lean +++ b/Mathlib/Tactic/TacticAnalysis.lean @@ -6,10 +6,10 @@ Authors: Anne Baanen module public meta import Lean.Compiler.IR.CompilerM +public meta import Lean.Elab.Command public meta import Lean.Elab.InfoTree.Util public meta import Lean.Util.Heartbeats public meta import Mathlib.Lean.Elab.Tactic.Meta -public meta import Lean.Elab.Command public import Mathlib.Lean.ContextInfo /-! # Tactic analysis framework diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean index d7d1c9fb58754c..ac9c7511497f4e 100644 --- a/Mathlib/Tactic/Tauto.lean +++ b/Mathlib/Tactic/Tauto.lean @@ -8,10 +8,10 @@ module public meta import Lean.Elab.ConfigEval public meta import Lean.Elab.Tactic.Classical public meta import Mathlib.Lean.Meta +public meta import Qq public import Mathlib.Basic.Logic.Basic -- shake: keep (dependency of tactic output) public import Mathlib.Tactic.CasesM public import Mathlib.Tactic.Core -public meta import Qq /-! The `tauto` tactic. diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean index f5304c846f28b9..60ce419e206fa0 100644 --- a/Mathlib/Tactic/Widget/Calc.lean +++ b/Mathlib/Tactic/Widget/Calc.lean @@ -10,8 +10,8 @@ public meta import Lean.Elab.Tactic.Calc public meta import Lean.Meta.Tactic.TryThis public meta import Mathlib.Data.String.Defs public meta import Mathlib.Tactic.Widget.SelectPanelUtils -public import Mathlib.Tactic.Widget.SelectPanelUtils public meta import ProofWidgets.Component.OfRpcMethod +public import Mathlib.Tactic.Widget.SelectPanelUtils meta import ProofWidgets.Component.Basic diff --git a/Mathlib/Tactic/Widget/CommDiag.lean b/Mathlib/Tactic/Widget/CommDiag.lean index ae66cb381c6276..44159eee5c043c 100644 --- a/Mathlib/Tactic/Widget/CommDiag.lean +++ b/Mathlib/Tactic/Widget/CommDiag.lean @@ -6,9 +6,9 @@ Authors: Wojciech Nawrocki module public meta import Mathlib.Tactic.ToDual -public import Mathlib.CategoryTheory.Category.Basic public meta import ProofWidgets.Component.PenroseDiagram public meta import ProofWidgets.Presentation.Expr +public import Mathlib.CategoryTheory.Category.Basic /-! This module defines tactic/meta infrastructure for displaying commutative diagrams in the infoview. -/ diff --git a/Mathlib/Tactic/Widget/Conv.lean b/Mathlib/Tactic/Widget/Conv.lean index 4a52fd8f2601c6..fad0aa47193527 100644 --- a/Mathlib/Tactic/Widget/Conv.lean +++ b/Mathlib/Tactic/Widget/Conv.lean @@ -6,8 +6,8 @@ Authors: Robin Böhne, Wojciech Nawrocki, Patrick Massot, Aaron Liu module public meta import Lean.PrettyPrinter.Delaborator.Builtins -public meta import ProofWidgets.Component.Basic public meta import Mathlib.Lean.Name +public meta import ProofWidgets.Component.Basic public import Mathlib.Tactic.Widget.SelectPanelUtils import ProofWidgets.Component.Basic diff --git a/Mathlib/Tactic/Widget/LibraryRewrite.lean b/Mathlib/Tactic/Widget/LibraryRewrite.lean index 6f743cecfef83f..37a936a18a2a77 100644 --- a/Mathlib/Tactic/Widget/LibraryRewrite.lean +++ b/Mathlib/Tactic/Widget/LibraryRewrite.lean @@ -9,11 +9,11 @@ public meta import Mathlib.Lean.GoalsLocation public meta import Mathlib.Lean.Meta.KAbstractPositions public meta import Mathlib.Lean.Meta.RefinedDiscrTree public meta import Mathlib.Tactic.Widget.SelectPanelUtils -public import Mathlib.Tactic.Widget.SelectPanelUtils public meta import ProofWidgets.Component.FilterDetails +public import Mathlib.Tactic.Widget.SelectPanelUtils -import Mathlib.Tactic.NthRewrite meta import ProofWidgets.Component.OfRpcMethod +import Mathlib.Tactic.NthRewrite /-! # Point & click library rewriting diff --git a/Mathlib/Tactic/Widget/SelectPanelUtils.lean b/Mathlib/Tactic/Widget/SelectPanelUtils.lean index 05cfa128897b6e..f7bc73c81952a5 100644 --- a/Mathlib/Tactic/Widget/SelectPanelUtils.lean +++ b/Mathlib/Tactic/Widget/SelectPanelUtils.lean @@ -7,9 +7,9 @@ module public meta import Lean.Meta.ExprLens public meta import Mathlib.Tactic.Widget.SelectInsertParamsClass -public import Mathlib.Tactic.Widget.SelectInsertParamsClass public meta import ProofWidgets.Component.MakeEditLink public meta import ProofWidgets.Data.Html +public import Mathlib.Tactic.Widget.SelectInsertParamsClass /-! # Selection panel utilities diff --git a/Mathlib/Tactic/Widget/StringDiagram.lean b/Mathlib/Tactic/Widget/StringDiagram.lean index bd387ba0f92fc7..19ebe070a4bcc3 100644 --- a/Mathlib/Tactic/Widget/StringDiagram.lean +++ b/Mathlib/Tactic/Widget/StringDiagram.lean @@ -7,12 +7,12 @@ module public meta import Mathlib.Data.List.Defs public meta import Mathlib.Tactic.CategoryTheory.Coherence.Normalize +public meta import ProofWidgets.Component.HtmlDisplay public meta import ProofWidgets.Component.Panel.Basic public meta import ProofWidgets.Component.PenroseDiagram +public meta import ProofWidgets.Presentation.Expr public import Mathlib.Tactic.CategoryTheory.Bicategory.Normalize public import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize -public meta import ProofWidgets.Component.HtmlDisplay -public meta import ProofWidgets.Presentation.Expr /-! # String Diagram Widget diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean index 91defa79e9431f..6d9d3e30b0b9c3 100644 --- a/Mathlib/Util/AtomM.lean +++ b/Mathlib/Util/AtomM.lean @@ -6,8 +6,8 @@ Authors: Mario Carneiro module public meta import Lean.Meta.Tactic.Simp.Types -public import Mathlib.Init public meta import Qq +public import Mathlib.Init meta import Qq.Typ diff --git a/Mathlib/Util/Notation3.lean b/Mathlib/Util/Notation3.lean index 60f8c024a325f2..811d9d457d1f7b 100644 --- a/Mathlib/Util/Notation3.lean +++ b/Mathlib/Util/Notation3.lean @@ -6,13 +6,13 @@ Authors: Mario Carneiro, Kyle Miller module public meta import Batteries.Lean.Syntax +public meta import Lean.Elab.AuxDef public meta import Lean.Elab.MacroArgUtil public meta import Lean.PrettyPrinter.Delaborator -- shake: keep (dependency of elaborator output) public meta import Lean.PrettyPrinter.Delaborator.Builtins public meta import Mathlib.Lean.PrettyPrinter.Delaborator public import Batteries.Linter.UnreachableTactic public import Batteries.Util.ExtendedBinder -public meta import Lean.Elab.AuxDef public import Mathlib.Lean.Elab.Term public import Mathlib.Tactic.ScopedNS diff --git a/Mathlib/Util/PrintSorries.lean b/Mathlib/Util/PrintSorries.lean index 420d42d16753af..8f5751e98ab657 100644 --- a/Mathlib/Util/PrintSorries.lean +++ b/Mathlib/Util/PrintSorries.lean @@ -6,8 +6,8 @@ Authors: Henrik Böving, Yaël Dillies, Kyle Miller module public meta import Lean.Elab.Command -public meta import Mathlib.Lean.Name public meta import Lean.Meta.Sorry +public meta import Mathlib.Lean.Name /-! # Tracking uses of `sorry` diff --git a/Mathlib/Util/Qq.lean b/Mathlib/Util/Qq.lean index 1edbcb3c15451e..47e12199de3e4e 100644 --- a/Mathlib/Util/Qq.lean +++ b/Mathlib/Util/Qq.lean @@ -5,8 +5,8 @@ Authors: Kim Morrison, Alex J. Best, Yaël Dillies -/ module -public import Qq public import Lean.Meta.Tactic.Assumption +public import Qq import Mathlib.Init import Qq.Typ diff --git a/Mathlib/Util/SynthesizeUsing.lean b/Mathlib/Util/SynthesizeUsing.lean index ed14af46d2d409..f1651a66eda3ed 100644 --- a/Mathlib/Util/SynthesizeUsing.lean +++ b/Mathlib/Util/SynthesizeUsing.lean @@ -8,8 +8,8 @@ module public meta import Lean.Elab.Tactic.Basic public meta import Qq -import Mathlib.Init meta import Qq.Typ +import Mathlib.Init /-! # `SynthesizeUsing` From 47670b5b8fbc92eada461665fe1b49dd76d83bcb Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Tue, 20 Oct 2026 01:40:58 -0400 Subject: [PATCH 16/16] Revert path changes --- .../Tactic/Linter/DirectoryDependency.lean | 39 ++++++++++--------- Mathlib/Tactic/Linter/Header.lean | 21 ++-------- 2 files changed, 24 insertions(+), 36 deletions(-) diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index fc2ee1e58fcab9..720ed2be331a0a 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -287,8 +287,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ Each key names a module prefix; modules matching that prefix may not import modules matching any of the prefixes in the corresponding list. Exceptions to these rules live in `overrideAllowedImportDirs` below. -/ -def forbiddenDirsPath (srcDir : System.FilePath) : System.FilePath := - srcDir / "scripts" / "forbiddenDirs.json" +def forbiddenDirsPath : System.FilePath := "scripts" / "forbiddenDirs.json" /-- The root modules of the libraries built from the mathlib repository itself. When elaborating one of their modules, the linter configuration file must be present. -/ @@ -310,10 +309,10 @@ outside `Mathlib/Algebra/Notation.lean`. This relation is read at runtime from `scripts/forbiddenDirs.json`, so that updating the configuration does not require recompiling this linter (and everything importing it). -/ -def forbiddenImportDirs (srcDir : System.FilePath) : IO NamePrefixRel := do +def forbiddenImportDirs : IO NamePrefixRel := do if let some rel ← forbiddenImportDirsCache.get then return rel - let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile <| forbiddenDirsPath srcDir) + let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile forbiddenDirsPath) let entries : Std.TreeMap String (Array String) ← IO.ofExcept <| fromJson? json let rel := NamePrefixRel.ofArray <| entries.toArray.flatMap fun (n₁, ns) ↦ ns.map fun n₂ ↦ (n₁.toName, n₂.toName) @@ -387,8 +386,7 @@ def checkBlocklist (env : Environment) (forbidden : NamePrefixRel) (mainModule : | none => none @[inherit_doc Mathlib.Linter.linter.directoryDependency] -public def directoryDependencyCheck (srcDir : System.FilePath) (mainModule : Name) : - CommandElabM (Array MessageData) := do +public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array MessageData) := do unless Linter.getLinterValue linter.directoryDependency (← Linter.getLinterOptions) do return #[] let env ← getEnv @@ -399,12 +397,15 @@ public def directoryDependencyCheck (srcDir : System.FilePath) (mainModule : Nam let matchingPrefixes := mainModule.prefixes.filter (fun prf ↦ allowedImportDirs.containsKey prf) if matchingPrefixes.isEmpty then -- Otherwise, we fall back to the blocklist `forbiddenImportDirs`. - unless ← (forbiddenDirsPath srcDir).pathExists do + unless ← forbiddenDirsPath.pathExists do + -- When mathlib is used as a dependency, its configuration file is not available; + -- in that case, there is nothing to check. + -- Within mathlib itself, the file must exist: fail loudly if it does not. if mathlibRoots.contains mainModule.getRoot then - throwError "directoryDependency linter: configuration file '{forbiddenDirsPath srcDir}' \ - not found." + throwError "directoryDependency linter: configuration file '{forbiddenDirsPath}' \ + not found; was mathlib built from its root directory?" return #[] - if let some msg := checkBlocklist env (← forbiddenImportDirs srcDir) mainModule imports then + if let some msg := checkBlocklist env (← forbiddenImportDirs) mainModule imports then return #[msg] else return #[] else @@ -412,7 +413,7 @@ public def directoryDependencyCheck (srcDir : System.FilePath) (mainModule : Nam -- from `Init`, `Lean` and `Std`, as well as imports in `Aesop`, `Qq`, `Plausible`, -- `ImportGraph`, `ProofWidgets` or `LeanSearchClient` (as these are imported in Tactic.Common). -- We also allow transitive imports of Mathlib.Init, as well as Mathlib.Init itself. - let initImports := (← findImports (srcDir / "Mathlib" / "Init.lean")).append + let initImports := (← findImports ("Mathlib" / "Init.lean")).append #[`Mathlib.Init, `Mathlib.Tactic.DeclarationNames] let exclude := [ `Init, `Std, `Lean, @@ -430,12 +431,12 @@ public def directoryDependencyCheck (srcDir : System.FilePath) (mainModule : Nam if !allowedImportDirs.contains mainModule imported then let importPath := env.importPath imported let mut msg := m!"Module {mainModule} depends on {imported},\n\ - but is only allowed to import modules starting with one of \ - {allRules.toArray.qsort (·.toString < ·.toString)}.\n\ - Note: module {imported}" + but is only allowed to import modules starting with one of \ + {allRules.toArray.qsort (·.toString < ·.toString)}.\n\ + Note: module {imported}" let mut superseded := false match importPath.toList with - | [] => msg := m!"{msg} is directly imported by this module" + | [] => msg := msg ++ " is directly imported by this module" | a :: rest => -- Only add messages about imports that aren't themselves transitive imports of -- forbidden imports. @@ -443,14 +444,14 @@ public def directoryDependencyCheck (srcDir : System.FilePath) (mainModule : Nam if !allowedImportDirs.contains mainModule a then superseded := true else - msg := m!"{msg} is imported by {a},\n" + msg := msg ++ s!" is imported by {a},\n" for dep in rest do if !allowedImportDirs.contains mainModule dep then superseded := true break - msg := m!"{msg}which is imported by {dep},\n" - msg := m!"{msg}which is imported by this module.\n\ - (Exceptions can be added to `allowedImportDirs`.)" + msg := msg ++ m!"which is imported by {dep},\n" + msg := msg ++ m!"which is imported by this module." + msg := msg ++ "(Exceptions can be added to `allowedImportDirs`.)" if !superseded then messages := messages.push msg return messages diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index f05602c7d147be..4371a6182f4432 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -176,18 +176,6 @@ public def copyrightHeaderChecks (copyright : String) (expectedLicense : String) output := output.push (toSyntax copyright "-/", s!"Copyright too short!") return output -/-- Given `modPath := foo/bar/A/B/C(.lean)` and a module name `A.B.C`, return `foo/bar/A.lean`. -Return `none` if the name components do not match the path components. -/ -def modPathToRootPath (modPath : System.FilePath) (modName : Name) : Option System.FilePath := - match modName with - | .str .anonymous root => do - guard <| modPath.fileStem == root - modPath.withExtension "lean" - | .str pre last => do - guard <| modPath.fileStem == last - modPathToRootPath (← modPath.parent) pre - | _ => none - /-- `isInLibraryRoot modName` returns `true` if `.lean` imports the file `modName`, where `` is the top-level component of `modName`. For example, for `Mathlib.Foo.Bar` this checks @@ -196,7 +184,8 @@ This is used by the `Header` linter as a heuristic of whether it should inspect so that the linter works in any project whose library root follows the standard Lean convention of being named after the top-level module. -/ -def isInLibraryRoot (rootPath : System.FilePath) (modName : Name) : IO Bool := do +def isInLibraryRoot (modName : Name) : IO Bool := do + let rootPath := (modName.getRoot.toString : System.FilePath).addExtension "lean" if ← rootPath.pathExists then let res ← parseImports' (← IO.FS.readFile rootPath) "" return res.imports.any (·.module == modName) @@ -432,12 +421,11 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do and any necessary `set_option` commands.\n\ Please, add a module doc-string (`/-! ... -/`) before `{stx}`.\ {.hint' m!"Type `m(odule docstring) + [tab]` to insert a template via snippet."}" - let some rootPath := modPathToRootPath (← getFileName) mainModule | return let inLibraryRoot? ← inLibraryRootMutex.atomically do match ← get with | some d => return d | none => - let val ← isInLibraryRoot rootPath mainModule + let val ← isInLibraryRoot mainModule -- We cache the answer to avoid recomputing it on every command. The fill runs under the mutex -- so that concurrent (async) linter runs don't all miss the cache and each redundantly parse -- the library root file; `mainModule` is fixed for the duration of the elaboration. @@ -457,8 +445,7 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do -- Report on broad or duplicate imports. broadImportsCheck importRefs mainModule duplicateImportsCheck importRefs - let srcDir := rootPath.parent.getD "." - let errors ← directoryDependencyCheck srcDir mainModule + let errors ← directoryDependencyCheck mainModule if errors.size > 0 then Linter.logLint linter.directoryDependency (importRefs.back?.elim headerStx (·.stx)) <| m!"\n\n".joinSep errors.toList