Trigger CI for leanprover/lean4#5542

Author: leanprover-community-mathlib4-bot

Diff for: .github/workflows/build.yml

@@ -41,10 +41,10 @@ jobs:
             exit 1
           fi
 
-      # - name: Check for long lines
-      #   if: always()
-      #   run: |
-      #     ! (find Batteries -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+      - name: Check for long lines
+        if: always()
+        run: |
+          ! (find Batteries -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
 
       - name: Check for trailing whitespace
         if: always()

Diff for: .github/workflows/test_mathlib.yml

@@ -20,7 +20,7 @@ jobs:
           sourceRunId: ${{ github.event.workflow_run.id }}
 
       - name: Checkout mathlib4 repository
-        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
         uses: actions/checkout@v4
         with:
           repository: leanprover-community/mathlib4
@@ -29,14 +29,15 @@ jobs:
           fetch-depth: 0
 
       - name: install elan
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
         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}"
 
       - name: Retrieve PR information
-        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
         id: pr-info
         uses: actions/github-script@v6
         env:
@@ -53,7 +54,7 @@ jobs:
             core.exportVariable('HEAD_BRANCH', pr.head.ref);
 
       - name: Check if tag exists
-        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
         id: check_mathlib_tag
         env:
           PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
@@ -90,7 +91,7 @@ jobs:
           fi
 
       - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
         env:
           PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
         run: |

Diff for: Batteries.lean

@@ -45,9 +45,7 @@ import Batteries.Lean.HashMap
 import Batteries.Lean.HashSet
 import Batteries.Lean.IO.Process
 import Batteries.Lean.Json
-import Batteries.Lean.Meta.AssertHypotheses
 import Batteries.Lean.Meta.Basic
-import Batteries.Lean.Meta.Clear
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.Meta.Expr
 import Batteries.Lean.Meta.Inaccessible

Diff for: Batteries/Classes/SatisfiesM.lean

@@ -52,7 +52,7 @@ protected theorem trivial [Applicative m] [LawfulApplicative m] {x : m α} :
 /-- The `SatisfiesM p x` predicate is monotonic in `p`. -/
 theorem imp [Functor m] [LawfulFunctor m] {x : m α}
     (h : SatisfiesM p x) (H : ∀ {a}, p a → q a) : SatisfiesM q x :=
-  let ⟨x, h⟩ := h; ⟨(fun ⟨a, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩
+  let ⟨x, h⟩ := h; ⟨(fun ⟨_, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩
 
 /-- `SatisfiesM` distributes over `<$>`, general version. -/
 protected theorem map [Functor m] [LawfulFunctor m] {x : m α}

Diff for: Batteries/Data/Array/Basic.lean

@@ -141,7 +141,7 @@ should prove the index bound.
 A proof by `get_elem_tactic` is provided as a default argument for `h`.
 This will perform the update destructively provided that `a` has a reference count of 1 when called.
 -/
-def setN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) (x : α) : Array α :=
+abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.set ⟨i, h⟩ x
 
 /--
@@ -150,7 +150,7 @@ Uses `get_elem_tactic` to supply a proof that the indices are in range.
 `hi` and `hj` are both given a default argument `by get_elem_tactic`.
 This will perform the update destructively provided that `a` has a reference count of 1 when called.
 -/
-def swapN (a : Array α) (i j : Nat)
+abbrev swapN (a : Array α) (i j : Nat)
     (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α :=
   Array.swap a ⟨i,hi⟩ ⟨j, hj⟩
 
@@ -159,8 +159,8 @@ def swapN (a : Array α) (i j : Nat)
 The old entry is returned alongwith the modified vector.
 Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible.
 -/
-def swapAtN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) (x : α) : α × Array α :=
-  swapAt a ⟨i,h⟩ x
+abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
+    α × Array α := swapAt a ⟨i,h⟩ x
 
 /--
 `eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`.
@@ -169,7 +169,7 @@ that the index is valid.
 This function takes worst case O(n) time because it has to backshift all elements at positions
 greater than i.
 -/
-def eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
+abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.feraseIdx ⟨i, h⟩
 
 end Array

Diff for: Batteries/Data/Array/Merge.lean

@@ -31,6 +31,8 @@ set_option linter.unusedVariables false in
 def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α :=
   merge (compare · · |>.isLT) xs ys
 
+-- We name `ord` so it can be provided as a named argument.
+set_option linter.unusedVariables.funArgs false in
 /--
 `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
 not contain duplicates. Equal elements are merged using `merge`. If `merge` respects the order
@@ -85,6 +87,8 @@ where
 
 @[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
 
+-- We name `eq` so it can be provided as a named argument.
+set_option linter.unusedVariables.funArgs false in
 /--
 `O(|xs|)`. Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with
 `f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ`.