leanprover-community
diff --git a/‎.github/workflows/PR_summary.yml‎
Lines changed: 2 additions & 2 deletions b/‎.github/workflows/PR_summary.yml‎
Lines changed: 2 additions & 2 deletions
diff --git a/‎.github/workflows/rm_set_option.yml‎
Lines changed: 65 additions & 13 deletions b/‎.github/workflows/rm_set_option.yml‎
Lines changed: 65 additions & 13 deletions
diff --git a/‎Archive/Examples/PropEncodable.lean‎
Lines changed: 1 addition & 1 deletion b/‎Archive/Examples/PropEncodable.lean‎
Lines changed: 1 addition & 1 deletion
diff --git a/‎Archive/Hairer.lean‎
Lines changed: 0 additions & 1 deletion b/‎Archive/Hairer.lean‎
Lines changed: 0 additions & 1 deletion
diff --git a/‎Archive/Imo/Imo1982Q1.lean‎
Lines changed: 0 additions & 2 deletions b/‎Archive/Imo/Imo1982Q1.lean‎
Lines changed: 0 additions & 2 deletions
diff --git a/‎Archive/Imo/Imo1986Q5.lean‎
Lines changed: 0 additions & 2 deletions b/‎Archive/Imo/Imo1986Q5.lean‎
Lines changed: 0 additions & 2 deletions
diff --git a/‎Archive/Imo/Imo1987Q1.lean‎
Lines changed: 1 addition & 1 deletion b/‎Archive/Imo/Imo1987Q1.lean‎
Lines changed: 1 addition & 1 deletion
diff --git a/‎Archive/Imo/Imo2019Q4.lean‎
Lines changed: 0 additions & 1 deletion b/‎Archive/Imo/Imo2019Q4.lean‎
Lines changed: 0 additions & 1 deletion
diff --git a/‎Archive/MiuLanguage/Basic.lean‎
Lines changed: 0 additions & 2 deletions b/‎Archive/MiuLanguage/Basic.lean‎
Lines changed: 0 additions & 2 deletions
diff --git a/‎Archive/MiuLanguage/DecisionNec.lean‎
Lines changed: 2 additions & 9 deletions b/‎Archive/MiuLanguage/DecisionNec.lean‎
Lines changed: 2 additions & 9 deletions
@@ -228,7 +228,7 @@ jobs:
         then
           # Format each changed workflow path as a Markdown bullet: "- `path`"
           workflowFilesChangedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${workflowFilesChanged}")"
-          workflowDocsReminder="$(printf "### Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
+          workflowDocsReminder="$(printf "### ⚠️ Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
         else
           workflowDocsReminder=""
         fi
@@ -239,7 +239,7 @@ jobs:
         then
           # Format each added scripts path as a Markdown bullet: "- `path`"
           scriptsFilesAddedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${scriptsFilesAdded}")"
-          scriptsLocationReminder="$(printf "### Scripts folder reminder\nThis PR adds files under \`scripts/\`.\nPlease consider whether each added script belongs in this repository or in \`leanprover-community/mathlib-ci\`.\n\nAdded scripts files:\n%s\n" "${scriptsFilesAddedMarkdown}")"
+          scriptsLocationReminder="$(printf "### ⚠️ Scripts folder reminder\nThis PR adds files under \`scripts/\`.\nPlease consider whether each added script belongs in this repository or in [\`leanprover-community/mathlib-ci\`](https://github.com/leanprover-community/mathlib-ci).\n\nA script belongs in **\`mathlib-ci\`** if it is a CI automation script that interacts with GitHub (e.g. managing labels, posting comments, triggering bots), runs from a trusted external checkout in CI, or requires access to secrets.\n\nA script belongs in **this repository** (\`scripts/\`) if it is a developer or maintainer tool to be run locally, a code maintenance or analysis utility, a style linting tool, or a data file used by the library's own linters.\n\nSee the [\`mathlib-ci\` README](https://github.com/leanprover-community/mathlib-ci) for more details.\n\nAdded scripts files:\n%s\n" "${scriptsFilesAddedMarkdown}")"
         else
           scriptsLocationReminder=""
         fi
 
@@ -10,12 +10,20 @@ on:
         required: false
         default: false
         type: boolean
+      global_timeout:
+        description: 'Global timeout in seconds (default: 18000 = 5 hours)'
+        required: false
+        default: '18000'
+        type: string
 
 jobs:
   build:
     name: Remove unnecessary set_option lines
-    runs-on: ubuntu-latest
+    runs-on: pr
     if: github.repository == 'leanprover-community/mathlib4'
+    permissions:
+      contents: read
+      id-token: write
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
@@ -26,21 +34,70 @@ jobs:
           use-github-cache: false
           use-mathlib-cache: true
 
+      - name: Restore progress cache
+        if: toJson(inputs.dry_run) != 'true'
+        uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: scripts/.rm_set_option_progress.jsonl
+          # Use run_id in restore-keys so we always pick up the most recent cache
+          # for this toolchain, regardless of which run saved it.
+          key: rm-set-option-progress-${{ hashFiles('lean-toolchain') }}-${{ github.run_id }}
+          restore-keys: |
+            rm-set-option-progress-${{ hashFiles('lean-toolchain') }}-
+
       - name: Remove unnecessary set_option lines
         id: rm_set_option
         shell: bash
+        env:
+          DRY_RUN: ${{ inputs.dry_run }}
+          GLOBAL_TIMEOUT: ${{ inputs.global_timeout }}
         run: |
-          DRY_RUN_FLAG=""
-          if [ "${{ inputs.dry_run }}" = "true" ]; then
-            DRY_RUN_FLAG="--dry-run"
+          ARGS=()
+          if [ "$DRY_RUN" = "true" ]; then
+            ARGS+=("--dry-run")
           fi
-          python3 scripts/rm_set_option.py $DRY_RUN_FLAG
+          TIMEOUT="${GLOBAL_TIMEOUT:-18000}"
+          python3 scripts/rm_set_option.py "${ARGS[@]}" --global-timeout "$TIMEOUT"
           if git diff --quiet; then
             echo "changed=false" >> "$GITHUB_OUTPUT"
           else
             echo "changed=true" >> "$GITHUB_OUTPUT"
           fi
 
+      - name: Save progress cache
+        # Always save (even on failure/timeout) so the next run can resume.
+        # Skip on dry-run (no files are modified) and if the progress file was
+        # cleaned up (meaning the run completed fully).
+        if: always() && toJson(inputs.dry_run) != 'true' && hashFiles('scripts/.rm_set_option_progress.jsonl') != ''
+        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: scripts/.rm_set_option_progress.jsonl
+          key: rm-set-option-progress-${{ hashFiles('lean-toolchain') }}-${{ github.run_id }}
+
+      - name: Build PR body
+        id: pr_body
+        if: steps.rm_set_option.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
+        shell: bash
+        env:
+          LINES_REMOVED: ${{ steps.rm_set_option.outputs.lines_removed }}
+          FILES_MODIFIED: ${{ steps.rm_set_option.outputs.files_modified }}
+          FILES_TIMED_OUT: ${{ steps.rm_set_option.outputs.files_timed_out }}
+          RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+        run: |
+          {
+            echo "body<<EOF"
+            echo "I removed ${LINES_REMOVED} unnecessary \`set_option\` line(s) across ${FILES_MODIFIED} file(s)."
+            if [ "${FILES_TIMED_OUT}" != "0" ]; then
+              echo ""
+              echo "⚠️ This is a partial run — ${FILES_TIMED_OUT} file(s) still to be processed. The next scheduled run will continue automatically."
+            fi
+            echo ""
+            echo "---"
+            echo ""
+            echo "[workflow run for this PR](${RUN_URL})"
+            echo "EOF"
+          } >> "$GITHUB_OUTPUT"
+
       - name: Generate app token
         id: app-token
         if: steps.rm_set_option.outputs.changed == 'true'
@@ -55,20 +112,15 @@ jobs:
       - name: Create Pull Request
         id: pr
         if: steps.rm_set_option.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
-        uses: peter-evans/create-pull-request@271a8d0340265f705b14b6d32b9829c1cb33d45e # v7.0.8
+        uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
         with:
           author: "mathlib-nolints[bot] <258989889+mathlib-nolints[bot]@users.noreply.github.com>"
           token: "${{ steps.app-token.outputs.token }}"
           commit-message: "chore: remove unnecessary set_option lines"
           branch: "rm-set-option"
           base: master
           title: "chore: remove unnecessary set_option lines"
-          body: |
-            I am happy to remove some unnecessary `set_option` lines for you!
-
-            ---
-
-            [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
+          body: ${{ steps.pr_body.outputs.body }}
           # labels: "auto-merge-after-CI"
 
       - name: Send Zulip message (success)
@@ -82,7 +134,7 @@ jobs:
           type: 'stream'
           topic: 'Mathlib `remove unnecessary set_option lines`'
           content: |
-            Please review #${{ steps.pr.outputs.pull-request-number }}, which removes unnecessary set_option lines.
+            Please review #${{ steps.pr.outputs.pull-request-number }}, which removes ${{ steps.rm_set_option.outputs.lines_removed }} unnecessary `set_option` line(s) across ${{ steps.rm_set_option.outputs.files_modified }} file(s).
 
       - name: Send Zulip message (failure)
         if: ${{ toJson(inputs.dry_run) != 'true' && failure() }}
 
@@ -74,7 +74,7 @@ private def finv : (WType fun i => Fin (arity α i)) → PropForm α
   | ⟨cor, fn⟩ => or (finv (fn 0)) (finv (fn 1))
 
 instance [Encodable α] : Encodable (PropForm α) :=
-  haveI : Encodable (Constructors α) := by unfold Constructors; infer_instance
+  haveI : Encodable (Constructors α) := inferInstanceAs <| Encodable (α ⊕ Unit ⊕ Unit ⊕ Unit)
   Encodable.ofLeftInverse f finv (by intro p; induction p <;> simp [f, finv, *])
 
 end PropForm
 
@@ -112,7 +112,6 @@ lemma inj_L : Injective (L ι) :=
     rw [isOpen_ball.interior_eq]
     apply subset_closure
 
-set_option backward.isDefEq.respectTransparency false in
 lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
     ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ∞ ρ ∧
     ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N →
 
@@ -70,7 +70,6 @@ lemma f₃ : f 3 = 1 := by
 
 lemma superadditive {m n : ℕ+} : f m + f n ≤ f (m + n) := by have h := hf.rel m n; grind
 
-set_option backward.isDefEq.respectTransparency false in
 lemma superhomogeneous {m n : ℕ+} : ↑n * f m ≤ f (n * m) := by
   induction n with
   | one => simp
@@ -84,7 +83,6 @@ lemma superhomogeneous {m n : ℕ+} : ↑n * f m ≤ f (n * m) := by
 lemma superlinear {a b c d : ℕ+} : a * f b + c * f d ≤ f (a * b + c * d) :=
   (add_le_add hf.superhomogeneous hf.superhomogeneous).trans hf.superadditive
 
-set_option backward.isDefEq.respectTransparency false in
 lemma le_mul_three_apply (n : ℕ+) : n ≤ f (3 * n) := by
   rw [← mul_one (n : ℕ), ← hf.f₃, mul_comm 3]
   exact hf.superhomogeneous
 
@@ -50,7 +50,6 @@ theorem map_eq_zero : f x = 0 ↔ 2 ≤ x := by
 
 theorem map_ne_zero_iff : f x ≠ 0 ↔ x < 2 := by simp [hf.map_eq_zero]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by
   have hx' : 0 < 2 - x := tsub_pos_of_lt hx
   have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
@@ -68,7 +67,6 @@ theorem map_eq (x : ℝ≥0) : f x = 2 / (2 - x) :=
 
 end IsGood
 
-set_option backward.isDefEq.respectTransparency false in
 theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2 - x) := by
   refine ⟨fun hf ↦ funext hf.map_eq, ?_⟩
   rintro rfl
 
@@ -55,7 +55,7 @@ fixed points. -/
 def fiber (k : ℕ) : Set (Perm α) :=
   {σ : Perm α | card (fixedPoints σ) = k}
 
-instance {k : ℕ} : Fintype (fiber α k) := by unfold fiber; infer_instance
+instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (setOf _)
 
 @[simp]
 theorem mem_fiber {σ : Perm α} {k : ℕ} : σ ∈ fiber α k ↔ card (fixedPoints σ) = k :=
 
@@ -30,7 +30,6 @@ open Nat Finset
 
 namespace Imo2019Q4
 
-set_option backward.isDefEq.respectTransparency false in
 theorem upper_bound {k n : ℕ} (hk : k > 0)
     (h : (k ! : ℤ) = ∏ i ∈ range n, ((2 : ℤ) ^ n - (2 : ℤ) ^ i)) : n < 6 := by
   have h2 : ∑ i ∈ range n, i < k := by
 
@@ -108,8 +108,6 @@ instance : Repr MiuAtom :=
 -/
 abbrev Miustr := List MiuAtom
 
-instance : Membership MiuAtom Miustr := by unfold Miustr; infer_instance
-
 /-- For display purposes, an `Miustr` can be represented as a `String`.
 -/
 def Miustr.mrepr : Miustr → String
 
@@ -103,11 +103,8 @@ string to be derivable, namely that the string must start with an M and contain
 -/
 def Goodm (xs : Miustr) : Prop :=
   List.headI xs = M ∧ M ∉ List.tail xs
+deriving Decidable
 
-set_option backward.isDefEq.respectTransparency false in
-instance : DecidablePred Goodm := by unfold Goodm; infer_instance
-
-set_option backward.isDefEq.respectTransparency false in
 /-- Demonstration that `"MI"` starts with `M` and has no `M` in its tail.
 -/
 theorem goodmi : Goodm [M, I] := by
@@ -121,7 +118,6 @@ We'll show, for each `i` from 1 to 4, that if `en` follows by Rule `i` from `st`
 -/
 
 
-set_option backward.isDefEq.respectTransparency false in
 theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ [I])) (h₂ : Goodm (xs ++ [I])) :
     Goodm (xs ++ [I, U]) := by
   obtain ⟨mhead, nmtail⟩ := h₂
@@ -141,7 +137,6 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
     rw [cons_append] at mtail
     exact or_self_iff.mp (mem_append.mp mtail)
 
-set_option backward.isDefEq.respectTransparency false in
 theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs))
     (h₂ : Goodm (as ++ [I, I, I] ++ bs)) : Goodm (as ++ (U :: bs)) := by
   obtain ⟨mhead, nmtail⟩ := h₂
@@ -160,7 +155,6 @@ The proof of the next lemma is identical, on the tactic level, to the previous p
 -/
 
 
-set_option backward.isDefEq.respectTransparency false in
 theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs))
     (h₂ : Goodm (as ++ [U, U] ++ bs)) : Goodm (as ++ bs) := by
   obtain ⟨mhead, nmtail⟩ := h₂
@@ -197,8 +191,7 @@ that `en` has no `M` in its tail. We automatically derive that this is a decidab
 -/
 def Decstr (en : Miustr) :=
   Goodm en ∧ (count I en % 3 = 1 ∨ count I en % 3 = 2)
-
-instance : DecidablePred Decstr := by unfold Decstr; infer_instance
+deriving Decidable
 
 /-- Suppose `en : Miustr`. If `en` is `Derivable`, then the condition `Decstr en` holds.
 -/