feat: add lake exe shake to CI (#9751)

- [X] depends on: #9830
- [X] depends on: #9772
- [X] depends on: #9996

This checks files for unused imports. The output here is piped through `gh-problem-matcher-wrap` so that it will show up as annotations.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

.github/workflows/bors.yml

@@ -256,11 +256,6 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
-      - name: verify `lake exe shake` works
-        # Later, we may want to make output from `shake` a CI error?
-        run: |
-          lake exe shake
-
       - name: test mathlib
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
@@ -272,6 +267,13 @@ jobs:
             lake build ProofWidgets
             make -j 8 test"
 
+      - name: check for unused imports
+        id: shake
+        uses: liskin/gh-problem-matcher-wrap@v2
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
+
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2

.github/workflows/build.yml

@@ -263,11 +263,6 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
-      - name: verify `lake exe shake` works
-        # Later, we may want to make output from `shake` a CI error?
-        run: |
-          lake exe shake
-
       - name: test mathlib
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
@@ -279,6 +274,13 @@ jobs:
             lake build ProofWidgets
             make -j 8 test"
 
+      - name: check for unused imports
+        id: shake
+        uses: liskin/gh-problem-matcher-wrap@v2
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
+
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2

.github/workflows/build.yml.in

@@ -242,11 +242,6 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
-      - name: verify `lake exe shake` works
-        # Later, we may want to make output from `shake` a CI error?
-        run: |
-          lake exe shake
-
       - name: test mathlib
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
@@ -258,6 +253,13 @@ jobs:
             lake build ProofWidgets
             make -j 8 test"
 
+      - name: check for unused imports
+        id: shake
+        uses: liskin/gh-problem-matcher-wrap@v2
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
+
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2

.github/workflows/build_fork.yml

@@ -260,11 +260,6 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
-      - name: verify `lake exe shake` works
-        # Later, we may want to make output from `shake` a CI error?
-        run: |
-          lake exe shake
-
       - name: test mathlib
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
@@ -276,6 +271,13 @@ jobs:
             lake build ProofWidgets
             make -j 8 test"
 
+      - name: check for unused imports
+        id: shake
+        uses: liskin/gh-problem-matcher-wrap@v2
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
+
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -3,7 +3,8 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Periodic
+import Mathlib.Algebra.Module.Basic
+import Mathlib.Algebra.Order.Archimedean
 import Mathlib.Algebra.Order.Group.Instances
 
 /-!

Mathlib/Algebra/GroupWithZero/Power.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Data.Int.Order.Basic
 

Mathlib/Algebra/Module/Basic.lean

@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.SMulWithZero
+import Mathlib.Data.Int.Basic
 import Mathlib.Data.Rat.NNRat
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Pi

Mathlib/Algebra/Module/LinearMap/Basic.lean

@@ -7,7 +7,6 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Ring.CompTypeclasses
 import Mathlib.Algebra.Star.Basic
-import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.GroupTheory.GroupAction.Hom
 
 #align_import algebra.module.linear_map from "leanprover-community/mathlib"@"cc8e88c7c8c7bc80f91f84d11adb584bf9bd658f"

Mathlib/Algebra/Module/LinearMap/Pointwise.lean

@@ -6,6 +6,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
 -/
 
 import Mathlib.Algebra.Module.LinearMap.Basic
+import Mathlib.Data.Set.Pointwise.SMul
 
 /-!
 # Pointwise actions of linear maps

Mathlib/Algebra/Order/Floor.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kevin Kappelmann
 -/
 import Mathlib.Algebra.CharZero.Lemmas
+import Mathlib.Data.Int.Basic
 import Mathlib.Data.Int.Lemmas
 import Mathlib.Data.Int.CharZero
 import Mathlib.Data.Set.Intervals.Group

Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.GroupTheory.GroupAction.Ring

Mathlib/Analysis/Complex/LocallyUniformLimit.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vincent Beffara
 -/
 import Mathlib.Analysis.Complex.RemovableSingularity
-import Mathlib.Analysis.Calculus.SmoothSeries
+import Mathlib.Analysis.Calculus.UniformLimitsDeriv
 
 #align_import analysis.complex.locally_uniform_limit from "leanprover-community/mathlib"@"fe44cd36149e675eb5dec87acc7e8f1d6568e081"
 

Mathlib/CategoryTheory/Monoidal/Braided.lean

@@ -3,9 +3,10 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
-import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
 import Mathlib.CategoryTheory.Monoidal.Discrete
+import Mathlib.CategoryTheory.Monoidal.Free.Coherence
+import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
+import Mathlib.Tactic.CategoryTheory.Coherence
 
 #align_import category_theory.monoidal.braided from "leanprover-community/mathlib"@"2efd2423f8d25fa57cf7a179f5d8652ab4d0df44"
 

Mathlib/CategoryTheory/Monoidal/Center.lean

@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 import Mathlib.CategoryTheory.Monoidal.Braided
 import Mathlib.CategoryTheory.Functor.ReflectsIso
-import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
 
 #align_import category_theory.monoidal.center from "leanprover-community/mathlib"@"14b69e9f3c16630440a2cbd46f1ddad0d561dee7"
 

Mathlib/Data/BitVec/Defs.lean

@@ -5,7 +5,6 @@ Authors: Joe Hendrix, Sebastian Ullrich, Harun Khan, Alex Keizer, Abdalrhman M M
 -/
 
 import Mathlib.Data.Fin.Basic
-import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.ZMod.Defs
 import Std.Data.BitVec
 

Mathlib/Data/BitVec/Lemmas.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Harun Khan
 -/
-
+import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.BitVec.Defs
 
 /-!

Mathlib/Data/Complex/Basic.lean

@@ -3,8 +3,9 @@ Copyright (c) 2017 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Mario Carneiro
 -/
-import Mathlib.Data.Real.Basic
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.GroupWithZero.Bitwise
+import Mathlib.Data.Real.Basic
 import Mathlib.Data.Set.Image
 
 #align_import data.complex.basic from "leanprover-community/mathlib"@"31c24aa72e7b3e5ed97a8412470e904f82b81004"

Mathlib/Data/ENNReal/Operations.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov
 -/
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Data.ENNReal.Basic
 
 #align_import data.real.ennreal from "leanprover-community/mathlib"@"c14c8fcde993801fca8946b0d80131a1a81d1520"

Mathlib/Data/Int/Parity.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Benjamin Davidson
 -/
 import Mathlib.Data.Nat.Parity
+import Mathlib.Data.Int.Basic
 import Mathlib.Tactic.Abel
 
 #align_import data.int.parity from "leanprover-community/mathlib"@"e3d9ab8faa9dea8f78155c6c27d62a621f4c152d"

Mathlib/Data/MvPolynomial/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
 import Mathlib.Algebra.Algebra.Tower
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.Regular.Pow
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Data.Finsupp.Antidiagonal

Mathlib/Data/Option/Defs.lean

@@ -3,7 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Init.Algebra.Classes
+import Mathlib.Mathport.Rename
+import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.TypeStar
 
 #align_import data.option.defs from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"

Mathlib/Data/Ordmap/Ordset.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathlib.Data.Ordmap.Ordnode
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Data.Nat.Dist
+import Mathlib.Data.Int.Basic
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Abel
 

Mathlib/Data/Polynomial/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Data.Finset.Sort
 

Mathlib/Data/Rat/NNRat/BigOperators.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.BigOperators.Order
-import Mathlib.Data.Rat.BigOperators
 import Mathlib.Data.Rat.NNRat
 
 /-! # Casting lemmas for non-negative rational numbers involving sums and products

Mathlib/GroupTheory/EckmannHilton.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau, Robert Y. Lewis
 -/
 import Mathlib.Algebra.Group.Defs
-import Mathlib.Init.Algebra.Classes
 
 #align_import group_theory.eckmann_hilton from "leanprover-community/mathlib"@"41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3"
 

Mathlib/GroupTheory/OrderOfElement.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Julian Kuelshammer
 -/
 import Mathlib.Algebra.GroupPower.IterateHom
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Data.Int.ModEq
 import Mathlib.Data.Nat.Interval
 import Mathlib.Data.Set.Pointwise.Basic

Mathlib/LinearAlgebra/Span.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Fréd
   Heather Macbeth
 -/
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
+import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.LinearAlgebra.Basic
 import Mathlib.Order.CompactlyGenerated.Basic
 import Mathlib.Order.OmegaCompletePartialOrder

Mathlib/NumberTheory/FLT/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Yaël Dillies
 -/
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Rat.Defs
 import Mathlib.Tactic.Positivity.Basic

Mathlib/Order/RelIso/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Init.Algebra.Classes
 import Mathlib.Data.FunLike.Basic
 import Mathlib.Logic.Embedding.Basic
 import Mathlib.Order.RelClasses

Mathlib/Order/RelSeries.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Fangming Li
 -/
+import Mathlib.Data.Int.Basic
 import Mathlib.Data.List.Chain
 import Mathlib.Data.List.OfFn
 import Mathlib.Data.Rel

Mathlib/Order/WithBot.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
+import Mathlib.Init.Algebra.Classes
 import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Order.BoundedOrder
 import Mathlib.Data.Option.NAry

Mathlib/RepresentationTheory/Action/Basic.lean

@@ -9,7 +9,6 @@ import Mathlib.CategoryTheory.Limits.FunctorCategory
 import Mathlib.CategoryTheory.Limits.Preserves.Basic
 import Mathlib.CategoryTheory.Adjunction.Limits
 import Mathlib.CategoryTheory.Conj
-import Mathlib.Data.Fin.Basic
 
 #align_import representation_theory.Action from "leanprover-community/mathlib"@"95a87616d63b3cb49d3fe678d416fbe9c4217bf4"
 

Mathlib/RingTheory/Nilpotent.lean

@@ -5,9 +5,10 @@ Authors: Oliver Nash
 -/
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Algebra.Algebra.Bilinear
+import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.Algebra.GeomSum
 import Mathlib.LinearAlgebra.Matrix.ToLin
 
 #align_import ring_theory.nilpotent from "leanprover-community/mathlib"@"da420a8c6dd5bdfb85c4ced85c34388f633bc6ff"

Mathlib/SetTheory/Game/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison, Apurva Nakade
 -/
+import Mathlib.Data.Int.Basic
 import Mathlib.SetTheory.Game.PGame
 import Mathlib.Tactic.Abel
 

Mathlib/Tactic/Abel.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Scott Morrison
 -/
 import Mathlib.Tactic.NormNum
 import Mathlib.Util.AtomM
-import Mathlib.Data.Int.Basic
 
 /-!
 # The `abel` tactic

Mathlib/Topology/Algebra/Field.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Scott Morrison
 -/
+import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.LocalExtr

Mathlib/Topology/MetricSpace/IsometricSMul.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Topology.MetricSpace.Isometry
 import Mathlib.Topology.MetricSpace.Lipschitz
 

Mathlib/Util/DischargerAsTactic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
 import Lean.Elab.Tactic.Basic
-import Lean.Meta.Tactic.Simp.Main
+import Lean.Meta.Tactic.Simp.Rewrite
 import Std.Tactic.Exact
 
 /-!