Trigger CI for leanprover-community/batteries#1692

Author: mathlib-nightly-testing[bot]

.github/workflows/actionlint.yml

@@ -17,3 +17,15 @@ jobs:
         with:
           tool_name: actionlint
           fail_level: any
+
+  ensure-sha-pinned-actions:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      # Using our fork's PR branch until upstream merges the improved error reporting:
+      # https://github.com/zgosalvez/github-actions-ensure-sha-pinned-actions/pull/288
+      # TODO: Update to upstream release once merged.
+      - name: Ensure all actions are pinned to SHA
+        uses: kim-em/github-actions-ensure-sha-pinned-actions@00f51cdb5bbc21f5bc873ef3a2dceef45df213af # improve-error-reporting

.github/workflows/daily.yml

@@ -314,7 +314,7 @@ jobs:
           reinstall-transient-toolchain: true
 
       - name: Install Rust
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@631a55b12751854ce901bb631d5902ceb48146f7 # stable
 
       - name: Check Mathlib using nanoda # make sure this name is consistent with "Get job status and URLs" in the notify job
         id: nanoda

.github/workflows/nightly-docgen.yml

@@ -18,7 +18,7 @@ jobs:
           rm -rf "$HOME/.cache/mathlib"
 
       - name: Checkout mathlib
-        uses: actions/checkout@v6.0.2
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: leanprover-community/mathlib4-nightly-testing
           ref: nightly-testing-green

.github/workflows/splice_bot.yaml

@@ -9,7 +9,7 @@ permissions: {}
 jobs:
   call-splice-bot:
     if: ${{ contains(github.event.comment.body, 'splice-bot') }}
-    uses: leanprover-community/SpliceBot/.github/workflows/splice.yaml@master
+    uses: leanprover-community/SpliceBot/.github/workflows/splice.yaml@fdb442693d6f613b25d2599ad64fd87cf019b9ce # master
     with:
       # Optional override; omit to use the reusable workflow's default "master"
       base_ref: master

.github/workflows/splice_bot_wf_run.yaml

@@ -10,7 +10,7 @@ permissions: {}
 jobs:
   run-reusable:
     if: ${{ github.event.workflow_run.conclusion == 'success' }}
-    uses: leanprover-community/SpliceBot/.github/workflows/splice_wf_run.yaml@master
+    uses: leanprover-community/SpliceBot/.github/workflows/splice_wf_run.yaml@fdb442693d6f613b25d2599ad64fd87cf019b9ce # master
     with:
       source_workflow: ${{ github.event.workflow_run.name }}
       push_to_fork: leanprover-community/mathlib4_copy

.gitignore

@@ -4,3 +4,7 @@
 .cache
 # `lake` stores its files here:
 .lake
+# Python bytecode cache from scripts/
+scripts/__pycache__/
+# Progress file from scripts/rm_set_option.py
+scripts/.rm_set_option_progress.jsonl

Archive/Imo/Imo1961Q3.lean

@@ -21,7 +21,6 @@ website.
 
 open Real
 
-set_option backward.isDefEq.respectTransparency false in
 theorem Imo1961Q3 {n : ℕ} {x : ℝ} (h₀ : n ≠ 0) :
     (cos x) ^ n - (sin x) ^ n = 1 ↔
       (∃ k : ℤ, k * π = x) ∧ Even n ∨ (∃ k : ℤ, k * (2 * π) = x) ∧ Odd n ∨

Archive/Imo/Imo1972Q5.lean

@@ -14,7 +14,6 @@ Problem: `f` and `g` are real-valued functions defined on the real line. For all
 Prove that `|g(x)| ≤ 1` for all `x`.
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 /--
 This proof begins by introducing the supremum of `f`, `k ≤ 1` as well as `k' = k / ‖g y‖`. We then
 suppose that the conclusion does not hold (`hneg`) and show that `k ≤ k'` (by
@@ -71,7 +70,6 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
     k' < k := H₁
     _ ≤ k' := H₂
 
-set_option backward.isDefEq.respectTransparency false in
 /-- IMO 1972 Q5
 
 Problem: `f` and `g` are real-valued functions defined on the real line. For all `x` and `y`,

Archive/Imo/Imo1982Q1.lean

@@ -55,7 +55,6 @@ namespace IsGood
 variable {f : ℕ+ → ℕ} (hf : IsGood f)
 include hf
 
-set_option backward.isDefEq.respectTransparency false in
 lemma f₁ : f 1 = 0 := by
   have h : f 2 = 2 * f 1 ∨ f 2 = 2 * f 1 + 1 := by rw [two_mul]; exact hf.rel 1 1
   obtain h₁ | h₂ := hf.f₂ ▸ h

Archive/Imo/Imo1988Q6.lean

@@ -188,7 +188,6 @@ end Imo1988Q6
 
 open Imo1988Q6
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Question 6 of IMO1988. If a and b are two natural numbers
 such that a*b+1 divides a^2 + b^2, show that their quotient is a perfect square. -/
 theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
@@ -245,7 +244,6 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
   · -- There is no base case in this application of Vieta jumping.
     simp
 
-set_option backward.isDefEq.respectTransparency false in
 /-
 The following example illustrates the use of constant descent Vieta jumping
 in the presence of a non-trivial base case.