.

.github/workflows/bors.yml

@@ -192,6 +192,7 @@ jobs:
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
+        id: get
         run: |
           lake exe cache clean
           lake exe cache get
@@ -205,9 +206,10 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
-        # We only upload the cache if the build ran (either succeeding or failing),
-        # but not if it was skipped.
-        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
+        # but not if any earlier step failed or was cancelled.
+        # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
+        if: ${{ always() && steps.get.outcome == 'success' }}
         run: |
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
           # lake exe cache commit || true

.github/workflows/build.yml

@@ -199,6 +199,7 @@ jobs:
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
+        id: get
         run: |
           lake exe cache clean
           lake exe cache get
@@ -212,9 +213,10 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
-        # We only upload the cache if the build ran (either succeeding or failing),
-        # but not if it was skipped.
-        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
+        # but not if any earlier step failed or was cancelled.
+        # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
+        if: ${{ always() && steps.get.outcome == 'success' }}
         run: |
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
           # lake exe cache commit || true

.github/workflows/build.yml.in

@@ -178,6 +178,7 @@ jobs:
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
+        id: get
         run: |
           lake exe cache clean
           lake exe cache get
@@ -191,9 +192,10 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
-        # We only upload the cache if the build ran (either succeeding or failing),
-        # but not if it was skipped.
-        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
+        # but not if any earlier step failed or was cancelled.
+        # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
+        if: ${{ always() && steps.get.outcome == 'success' }}
         run: |
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
           # lake exe cache commit || true

.github/workflows/build_fork.yml

@@ -196,6 +196,7 @@ jobs:
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
+        id: get
         run: |
           lake exe cache clean
           lake exe cache get
@@ -209,9 +210,10 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
-        # We only upload the cache if the build ran (either succeeding or failing),
-        # but not if it was skipped.
-        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
+        # but not if any earlier step failed or was cancelled.
+        # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
+        if: ${{ always() && steps.get.outcome == 'success' }}
         run: |
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
           # lake exe cache commit || true

.github/workflows/nolints.yml

@@ -0,0 +1,81 @@
+name: update nolints
+
+on:
+  schedule:
+    - cron: "0 0 * * 0"
+
+jobs:
+  build:
+    name: Build, lint and update nolints and style exceptions
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      # The Hoskinson runners may not have jq installed, so do that now.
+      - name: 'Setup jq'
+        uses: dcarbone/[email protected]
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - uses: actions/checkout@v3
+
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+      - name: prune ProofWidgets .lake
+        run: |
+          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
+          # but also `.oleans`, which may have been built with the wrong toolchain.
+          # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
+          rm -rf .lake/packages/proofwidgets/.lake/build/lib
+          rm -rf .lake/packages/proofwidgets/.lake/build/ir
+
+      - name: get cache
+        run: |
+          lake exe cache clean
+          lake exe cache get
+
+      - name: build mathlib
+        id: build
+        uses: liskin/gh-problem-matcher-wrap@v2
+        with:
+          linters: gcc
+          run: |
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
+
+      - name: lint mathlib
+        id: lint
+        uses: liskin/gh-problem-matcher-wrap@v2
+        with:
+          linters: gcc
+          run: |
+            env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+            mv nolints.json scripts/nolints.json
+            ./scripts/update-style-exceptions.sh
+            git diff
+
+      - name: configure git setup
+        run: |
+          git remote add origin-bot "https://leanprover-community-bot:${{ secrets.UPDATE_NOLINTS_TOKEN }}@github.com/leanprover-community/mathlib.git"
+          git config user.email "[email protected]"
+          git config user.name "leanprover-community-bot"
+
+          # By default, github actions overrides the credentials used to access any
+          # github url so that it uses the github-actions[bot] user.  We want to access
+          # github using a different username.
+          git config --unset http.https://github.com/.extraheader
+
+      - name: update nolints.json and style-exceptions.txt
+        run: ./scripts/update_nolints_CI.sh
+        env:
+          DEPLOY_GITHUB_TOKEN: ${{ secrets.UPDATE_NOLINTS_TOKEN }}

Archive/Examples/IfNormalization/Result.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes
 -/
 import Archive.Examples.IfNormalization.Statement
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
-import Mathlib.Algebra.Order.Monoid.MinMax
+import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Data.List.AList
 import Mathlib.Tactic.Recall
 

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes, Scott Morrison
 -/
 import Archive.Examples.IfNormalization.Statement
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
-import Mathlib.Algebra.Order.Monoid.MinMax
+import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Data.List.AList
 
 /-!

Archive/Imo/Imo2006Q5.lean

@@ -173,21 +173,21 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
     suffices H' : (P.comp P - X).roots.toFinset ⊆ (P + (X : ℤ[X]) - a - b).roots.toFinset from
       (Finset.card_le_card H').trans
         ((Multiset.toFinset_card_le _).trans <| (card_roots' _).trans_eq hPab)
-    · -- Let t be a root of P(P(t)) - t, define u = P(t).
-      intro t ht
-      replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
-      rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
-      simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def,
-        eval_sub, eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
-      -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
-      -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
-      -- the other.
-      apply (Int.add_eq_add_of_natAbs_eq_of_natAbs_eq hab _ _).symm <;>
-          apply Int.natAbs_eq_of_dvd_dvd <;> set u := P.eval t
-      · rw [← ha, ← ht]; apply sub_dvd_eval_sub
-      · apply sub_dvd_eval_sub
-      · rw [← ht]; apply sub_dvd_eval_sub
-      · rw [← ha]; apply sub_dvd_eval_sub
+    -- Let t be a root of P(P(t)) - t, define u = P(t).
+    intro t ht
+    replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
+    rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
+    simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def,
+      eval_sub, eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
+    -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
+    -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
+    -- the other.
+    apply (Int.add_eq_add_of_natAbs_eq_of_natAbs_eq hab _ _).symm <;>
+        apply Int.natAbs_eq_of_dvd_dvd <;> set u := P.eval t
+    · rw [← ha, ← ht]; apply sub_dvd_eval_sub
+    · apply sub_dvd_eval_sub
+    · rw [← ht]; apply sub_dvd_eval_sub
+    · rw [← ha]; apply sub_dvd_eval_sub
 #align imo2006_q5.imo2006_q5' Imo2006Q5.imo2006_q5'
 
 end Imo2006Q5

Archive/Imo/Imo2021Q1.lean

@@ -89,9 +89,9 @@ theorem exists_finset_3_le_card_with_pairs_summing_to_squares (n : ℕ) (hn : 10
     suffices a ∉ {b, c} ∧ b ∉ {c} by
       rw [Finset.card_insert_of_not_mem this.1, Finset.card_insert_of_not_mem this.2,
         Finset.card_singleton]
-    · rw [Finset.mem_insert, Finset.mem_singleton, Finset.mem_singleton]
-      push_neg
-      exact ⟨⟨hab.ne, (hab.trans hbc).ne⟩, hbc.ne⟩
+    rw [Finset.mem_insert, Finset.mem_singleton, Finset.mem_singleton]
+    push_neg
+    exact ⟨⟨hab.ne, (hab.trans hbc).ne⟩, hbc.ne⟩
   · intro x hx y hy hxy
     simp only [Finset.mem_insert, Finset.mem_singleton] at hx hy
     rcases hx with (rfl | rfl | rfl) <;> rcases hy with (rfl | rfl | rfl)

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -201,8 +201,8 @@ theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p
     rw [counted_succ_succ, measure_union (disjoint_bits _ _) list_int_measurableSet,
       count_injective_image List.cons_injective, count_countedSequence _ _,
       count_injective_image List.cons_injective, count_countedSequence _ _]
-    · norm_cast
-      rw [add_assoc, add_comm 1 q, ← Nat.choose_succ_succ, Nat.succ_eq_add_one, add_right_comm]
+    norm_cast
+    rw [add_assoc, add_comm 1 q, ← Nat.choose_succ_succ, Nat.succ_eq_add_one, add_right_comm]
 #align ballot.count_counted_sequence Ballot.count_countedSequence
 
 theorem first_vote_pos :
@@ -237,12 +237,11 @@ theorem first_vote_pos :
       rw [(condCount_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, condCount,
         cond_apply _ list_int_measurableSet, hint, count_injective_image List.cons_injective,
         count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
-        Nat.cast_add, Nat.cast_one]
-      · rw [mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
-        · norm_cast
-          rw [mul_comm _ (p + 1), ← Nat.succ_eq_add_one p, Nat.succ_add, Nat.succ_mul_choose_eq,
-            mul_comm]
-        all_goals simp [(Nat.choose_pos <| (le_add_iff_nonneg_right _).2 zero_le').ne.symm]
+        Nat.cast_add, Nat.cast_one, mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
+      · norm_cast
+        rw [mul_comm _ (p + 1), ← Nat.succ_eq_add_one p, Nat.succ_add, Nat.succ_mul_choose_eq,
+          mul_comm]
+      all_goals simp [(Nat.choose_pos <| (le_add_iff_nonneg_right _).2 zero_le').ne.symm]
     · simp
 #align ballot.first_vote_pos Ballot.first_vote_pos
 
@@ -394,11 +393,11 @@ theorem ballot_problem :
       ENNReal.toReal_sub_of_le, ENNReal.toReal_nat, ENNReal.toReal_nat]
     exacts [Nat.cast_le.2 qp.le, ENNReal.natCast_ne_top _]
   rwa [ENNReal.toReal_eq_toReal (measure_lt_top _ _).ne] at this
-  · simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,
-      add_eq_zero_iff, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
-      not_false_iff, and_true_iff]
-    push_neg
-    exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩
+  simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,
+    add_eq_zero_iff, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
+    not_false_iff, and_true_iff]
+  push_neg
+  exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩
 #align ballot.ballot_problem Ballot.ballot_problem
 
 end Ballot

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -317,7 +317,7 @@ theorem existsPolitician_of_degree_le_two (hd : G.IsRegularOfDegree d) (h : d 
     ExistsPolitician G := by
   interval_cases d
   iterate 2 apply existsPolitician_of_degree_le_one hG hd; norm_num
-  · exact existsPolitician_of_degree_eq_two hG hd
+  exact existsPolitician_of_degree_eq_two hG hd
 #align theorems_100.friendship.exists_politician_of_degree_le_two Theorems100.Friendship.existsPolitician_of_degree_le_two
 
 end Friendship

Cache/Hashing.lean

@@ -53,8 +53,7 @@ def getFileImports (source : String) (pkgDirs : PackageDirs) : Array FilePath :=
 /-- Computes a canonical hash of a file's contents. -/
 def hashFileContents (contents : String) : UInt64 :=
   -- revert potential file transformation by git's `autocrlf`
-  let contents := Lake.crlf2lf contents
-  hash contents
+  hash contents.crlfToLf
 
 /--
 Computes the root hash, which mixes the hashes of the content of: