Fix deprecations and update exposition page CI

.github/workflows/blueprint.yml

@@ -24,8 +24,18 @@ permissions:
   actions: write          # Write access to GitHub Actions
 
 env:
-  LEAN_EXPOSITION_REPO: LeanMachineLearning/exposition
-  LEAN_EXPOSITION_REF: main
+  REFEREE_REPO: LeanMachineLearning/exposition
+  # The referee release to use. Leave empty for the most recent one; set a tag (e.g. `v0.1.0`) to
+  # pin the site generator, which is worth doing once the output is being read by anyone.
+  #
+  # A *release* rather than a run artifact on purpose: release assets of a public repository need no
+  # authentication and never expire, while a cross-repository artifact download needs a PAT with
+  # `actions:read` (a workflow's own GITHUB_TOKEN cannot reach another repository's artifacts) and
+  # is deleted after 90 days.
+  REFEREE_VERSION: ""
+  # Kept as `exposition` rather than renamed to `referee` along with the tool: this path is the
+  # published URL, and existing links to it would break.
+  REFEREE_SITE_URL: https://leanmachinelearning.org/LML/exposition
 
 jobs:
   build_project:
@@ -59,29 +69,89 @@ jobs:
         run: |
           ./scripts/build_docs.sh
 
-      - name: Clone lean-exposition
+      - name: Download referee binary
         if: github.event_name == 'push'
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          git clone --depth 1 --branch "$LEAN_EXPOSITION_REF" \
-            "https://github.com/$LEAN_EXPOSITION_REPO" /tmp/lean-exposition
+          set -euo pipefail
+          mkdir -p /tmp/referee
+          gh release download ${REFEREE_VERSION:+"$REFEREE_VERSION"} \
+            -R "$REFEREE_REPO" \
+            --pattern 'referee-linux-x86_64-*.tar.gz' \
+            --dir /tmp/referee --clobber
+          tar -xzf /tmp/referee/referee-linux-x86_64-*.tar.gz -C /tmp/referee
+          referee_bin=$(echo /tmp/referee/referee-linux-x86_64-*/referee)
+          chmod +x "$referee_bin"
+          echo "REFEREE_BIN=$referee_bin" >> "$GITHUB_ENV"
 
-      - name: Build exposition binary
+          # `referee` is a Lean executable built with `supportInterpreter := true`, so it loads the
+          # shared library of the toolchain it was compiled against and has to match this project's.
+          # Checked here because the alternative is a link-time failure four steps later that says
+          # nothing about the cause.
+          want=$(tr -d '[:space:]' < lean-toolchain)
+          got=$(jq -r .lean_toolchain "$(dirname "$referee_bin")/metadata.json" | tr -d '[:space:]')
+          if [ "$want" != "$got" ]; then
+            echo "::error::referee was built for $got but this project uses $want. Publish a \
+              referee release from a matching toolchain, or pin REFEREE_VERSION to one."
+            exit 1
+          fi
+
+      # The previous run's collected data, so the site can say what changed since it. Optional in
+      # every direction: the first run has nothing to download, a failed lookup is swallowed, and
+      # `build-site` simply omits the Changes page when no baseline reaches it.
+      - name: Fetch previous referee data for the revision diff
         if: github.event_name == 'push'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          cd /tmp/lean-exposition && lake build exposition
-          echo "EXPOSITION_BIN=/tmp/lean-exposition/.lake/build/bin/exposition" >> "$GITHUB_ENV"
+          set -euo pipefail
+          run_id=$(gh run list -R "$GITHUB_REPOSITORY" \
+            --workflow "${{ github.workflow }}" --branch "${{ github.ref_name }}" \
+            --status success --limit 1 --json databaseId --jq '.[0].databaseId // empty')
+          [ -n "$run_id" ] || { echo "no earlier successful run; skipping the baseline"; exit 0; }
+          gh run download "$run_id" -R "$GITHUB_REPOSITORY" \
+            -n referee-data -D /tmp/referee-baseline
+          echo "REFEREE_BASELINE=/tmp/referee-baseline/referee-data.json" >> "$GITHUB_ENV"
 
-      - name: Build exposition documentation
+      - name: Build the referee site
         if: github.event_name == 'push'
         run: |
-          lake env "$EXPOSITION_BIN" \
-            --root LeanMachineLearning \
-            --repo-url https://github.com/LeanMachineLearning/LML \
-            --site-url https://leanmachinelearning.org/LML/exposition \
-            --output ./exposition \
-            --exclude-lib LMLTutorial
-          mkdir -p home_page/exposition
-          cp -r exposition/html-multi/* home_page/exposition
+          set -euo pipefail
+          # The phase split: everything needing a Lean environment produces data, and rendering is a
+          # pure function of that data. `--exclude-lib` applies to the three phases that import the
+          # project, and to none of `build-site`, which reads only the JSON. `highlight-extracted`
+          # is deliberately skipped — it re-elaborates every extracted file and costs more than the
+          # rest of this job combined; without it the standalone files are still written and linked,
+          # just not rendered inline.
+          lake env "$REFEREE_BIN" collect \
+            --root LeanMachineLearning --exclude-lib LMLTutorial --data referee-data.json
+          lake env "$REFEREE_BIN" extract \
+            --data referee-data.json --exclude-lib LMLTutorial --output ./referee-site
+          lake env "$REFEREE_BIN" highlight \
+            --data referee-data.json --output ./referee-site
+          # `--trust` is an editorial claim, not a derived fact: it says whoever publishes this site
+          # vouches for Mathlib and everything under it. Drop it and every upstream package counts
+          # as unaudited; name more packages to vouch for more.
+          "$REFEREE_BIN" build-site \
+            --data referee-data.json \
+            --output ./referee-site \
+            --repo-url "https://github.com/$GITHUB_REPOSITORY" \
+            --site-url "$REFEREE_SITE_URL" \
+            --trust mathlib \
+            ${REFEREE_BASELINE:+--baseline "$REFEREE_BASELINE"} \
+            ${REFEREE_BASELINE:+--baseline-label "the previous build"}
+
+      # Kept as an artifact so the *next* run can diff against it. Also the thing to download when
+      # you want to re-render the site locally without re-importing the project.
+      - name: Upload referee data
+        if: github.event_name == 'push'
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: referee-data
+          path: referee-data.json
+          retention-days: 90
 
       - name: Compile blueprint and documentation
         uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14
@@ -91,6 +161,16 @@ jobs:
           build-page: false
           deploy: false
 
+      # After the docs step, which writes into the same folder alongside `tutorial/` from
+      # `build_docs.sh`. Those steps only ever add, so the order is not load-bearing — but copying
+      # last keeps the referee output out of reach of anything else that writes there.
+      - name: Add the referee site to the home page
+        if: github.event_name == 'push'
+        run: |
+          set -euo pipefail
+          mkdir -p home_page/exposition
+          cp -r referee-site/html-multi/. home_page/exposition/
+
       - name: "Upload website (API documentation, blueprint and any home page)"
         if: github.event_name == 'push'
         uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0

LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean

@@ -74,7 +74,7 @@ lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂
     refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_)
     exact measurableSet_eq_fun (by fun_prop) measurable_const
   ext f
-  simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop, exists_eq_right']
+  simp only [Set.mem_ofPred_eq, Set.mem_iUnion, exists_prop, exists_eq_right']
   constructor
   · intro hf x hx
     rw [← hf]

LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean

@@ -457,7 +457,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
       (Measure.map (fun ω ↦ (X ω, Z ω)) μ ⊗ₘ κ) (s ∩ {p | p.1.2 = b}) by
     have hs_iUnion : s = ⋃ b, s ∩ {p | p.1.2 = b} := by
       ext p
-      simp only [Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq]
+      simp only [Set.mem_iUnion, Set.mem_inter_iff, Set.mem_ofPred_eq]
       grind
     have h_disj : Pairwise (Function.onFun Disjoint fun b ↦ s ∩ {p | p.1.2 = b}) := by
       intro i j hij
@@ -486,13 +486,13 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
           ((measurableSet_singleton _).preimage (by fun_prop))
       · fun_prop
       · exact (measurableSet_singleton _).preimage (by fun_prop)
-      simp only [Set.preimage_setOf_eq]
+      simp only [Set.preimage_ofPred_eq]
       classical
       have h_le : ∫⁻ a, (κ (X a, Z a)) {a_1 | Z a = b} ∂μ ≤
           ∫⁻ a, {a' | Z a' = b}.indicator (fun _ ↦ κ.bound) a ∂μ := by
         gcongr with a
         by_cases hZ : Z a = b
-        · simp only [hZ, Set.setOf_true, Set.mem_setOf_eq, Set.indicator_of_mem]
+        · simp only [hZ, Set.ofPred_true, Set.mem_ofPred_eq, Set.indicator_of_mem]
           exact κ.measure_le_bound _ _
         · simp [hZ]
       refine le_antisymm (h_le.trans ?_) zero_le
@@ -525,8 +525,8 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
     rw [← h1, ← mul_assoc, ENNReal.mul_inv_cancel hb (by simp), one_mul]
   convert h1'
   · ext x
-    simp only [Set.preimage_inter, Set.preimage_setOf_eq, Set.mem_inter_iff, Set.mem_preimage,
-      Set.mem_setOf_eq]
+    simp only [Set.preimage_inter, Set.preimage_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage,
+      Set.mem_ofPred_eq]
     grind
   · rw [Measure.compProd_apply, Measure.compProd_apply, lintegral_map, lintegral_map]
     rotate_left
@@ -538,7 +538,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
     · exact hs'
     · exact hs.inter ((measurableSet_singleton _).preimage (by fun_prop))
     rw [lintegral_cond, ← mul_assoc, ENNReal.mul_inv_cancel hb (by simp), one_mul]
-    simp only [Set.preimage_inter, Set.preimage_setOf_eq, Kernel.coe_comap, Function.comp_apply]
+    simp only [Set.preimage_inter, Set.preimage_ofPred_eq, Kernel.coe_comap, Function.comp_apply]
     classical
     have h_eq : (fun a ↦ κ (X a, Z a) (Prod.mk (X a, Z a) ⁻¹' s ∩ {a_1 | Z a = b})) =
         {a | Z a = b}.indicator
@@ -550,7 +550,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
     swap; · exact (measurableSet_singleton _).preimage (by fun_prop)
     refine setLIntegral_congr_fun ((measurableSet_singleton _).preimage (by fun_prop)) fun a ha ↦ ?_
     congr 1 with ω
-    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_setOf_eq, and_iff_left_iff_imp]
+    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_ofPred_eq, and_iff_left_iff_imp]
     grind
 
 lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ)

LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean

@@ -149,7 +149,7 @@ lemma measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKerne
   classical
   have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by
     ext1 a
-    simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]
+    simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]
     exact ⟨fun h ↦ by simp [h], fun h ↦ le_antisymm h.1 h.2⟩
   rw [h_sub]
   refine MeasurableSet.inter ?_ ?_

LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean

@@ -226,7 +226,7 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
   have : (fun ω ↦ (pullCount A a n ω : ℝ))
       =ᵐ[P] fun ω ↦ m + (n - K * m) * {ω' | A (K * m) ω' = a}.indicator (fun _ ↦ 1) ω := by
     filter_upwards [pullCount_of_ge h a hm hn] with ω h
-    simp only [h, Set.indicator_apply, Set.mem_setOf_eq, mul_ite, mul_one, mul_zero, Nat.cast_add,
+    simp only [h, Set.indicator_apply, Set.mem_ofPred_eq, mul_ite, mul_one, mul_zero, Nat.cast_add,
       Nat.cast_ite, CharP.cast_eq_zero, add_right_inj]
     norm_cast
   rw [integral_congr_ae this, integral_add (integrable_const _), integral_const_mul]

LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean

@@ -233,7 +233,7 @@ lemma integral_sum_range_actionMean_bestAction_sub_ucb_bestAction_le {alg : Algo
         intro ω hω
         apply sum_nonpos
         intro t ht
-        rw [Set.mem_compl_iff, Set.mem_setOf_eq] at hω
+        rw [Set.mem_compl_iff, Set.mem_ofPred_eq] at hω
         push Not at hω
         grind [hω t (mem_range.mp ht), ucb, actionMean]
     _ ≤ ∫ ω in F, ∑ t ∈ range n, (u - l) ∂P := by
@@ -284,7 +284,7 @@ lemma integral_sum_range_ucb_action_sub_actionMean_action_le {alg : Algorithm (F
         · apply setIntegral_mono_on (Integrable.integrableOn (by fun_prop))
             (Integrable.integrableOn (by fun_prop)) hF.compl
           intro ω hω
-          rw [Set.mem_compl_iff, Set.mem_setOf_eq] at hω
+          rw [Set.mem_compl_iff, Set.mem_ofPred_eq] at hω
           push Not at hω
           exact sum_ucb_sub_mean_le (fun a ↦ (κ (E ω, a))[id]) (hm (E ω)) hlu
             (fun t ht hpc ↦ hω t ht (A t ω) hpc)

LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean

@@ -216,7 +216,7 @@ lemma prob_ucbIndex_le [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
       1 / (n + 1) ^ (c - 1) := by
   let s : Set (ℕ × ℝ) := {(m, x) | 0 < m ∧ x / m + √(2 * (c * σ2) * log (↑n + 1) / m) ≤ (ν a)[id]}
   have hs : MeasurableSet s := by
-    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOf, s]
+    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOfPred, s]
     fun_prop
   classical
   calc P {h | 0 < pullCount A a n h ∧ empMean A R a n h + ucbWidth A (c * σ2) a n h ≤ (ν a)[id]}
@@ -234,8 +234,8 @@ lemma prob_ucbIndex_le [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
     refine Finset.sum_congr rfl fun k hk ↦ ?_
     congr with ω
     have hk : 0 < k := by grind
-    simp only [Nat.cast_nonneg, sqrt_div', id_eq, Set.preimage_setOf_eq, hk, true_and,
-      Set.mem_setOf_eq, s]
+    simp only [Nat.cast_nonneg, sqrt_div', id_eq, Set.preimage_ofPred_eq, hk, true_and,
+      Set.mem_ofPred_eq, s]
     grind
   _ ≤ ∑ k ∈ Icc 1 n, (1 : ℝ≥0∞) / (n + 1) ^ c := by
     gcongr with k hk
@@ -259,7 +259,7 @@ lemma prob_ucbIndex_ge [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
       (ν a)[id] ≤ empMean A R a n h - ucbWidth A (c * σ2) a n h} ≤ 1 / (n + 1) ^ (c - 1) := by
   let s : Set (ℕ × ℝ) := {(m, x) | 0 < m ∧ (ν a)[id] ≤ x / m - √(2 * (c * σ2) * log (↑n + 1) / m)}
   have hs : MeasurableSet s := by
-    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOf, s]
+    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOfPred, s]
     fun_prop
   classical
   calc P {h | 0 < pullCount A a n h ∧ (ν a)[id] ≤ empMean A R a n h - ucbWidth A (c * σ2) a n h}
@@ -277,8 +277,8 @@ lemma prob_ucbIndex_ge [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
     refine Finset.sum_congr rfl fun k hk ↦ ?_
     congr with ω
     have hk : 0 < k := by grind
-    simp only [id_eq, Nat.cast_nonneg, sqrt_div', Set.preimage_setOf_eq, hk, true_and,
-      Set.mem_setOf_eq, s]
+    simp only [id_eq, Nat.cast_nonneg, sqrt_div', Set.preimage_ofPred_eq, hk, true_and,
+      Set.mem_ofPred_eq, s]
     grind
   _ ≤ ∑ k ∈ Icc 1 n, (1 : ℝ≥0∞) / (n + 1) ^ c := by
     gcongr with k hk
@@ -397,7 +397,7 @@ lemma some_sum_eq_zero [Nonempty (Fin K)]
   have h_gt := time_gt_of_pullCount_gt_one h a (ν := ν) (c := c * σ2) (hK := hK)
   filter_upwards [h_ae, h_gt] with ω h_le h_time_ge
   simp only [id_eq, tsub_le_iff_right, sum_eq_zero_iff, mem_range, Set.indicator_apply_eq_zero,
-    Set.mem_setOf_eq, Pi.one_apply, one_ne_zero, imp_false, not_and, not_le]
+    Set.mem_ofPred_eq, Pi.one_apply, one_ne_zero, imp_false, not_and, not_le]
   intro k hn h_arm hC_lt h_le_best
   by_contra! h_le_arm
   have h := pullCount_arm_le (by positivity : 0 ≤ c * σ2) h_le_best (by simpa) ?_ ?_ ?_
@@ -472,12 +472,12 @@ lemma expectation_pullCount_le'
       (measurableSet_lt (by fun_prop) (by fun_prop))
   have h_meas_1 b : Measurable fun h ↦ {s | 0 < pullCount A a s h ∧ (ν a)[id] <
       empMean A R a s h - ucbWidth A (c * σ2) a s h}.indicator (1 : ℕ → ℕ) b := by
-    simp only [id_eq, Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
+    simp only [id_eq, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply]
     exact Measurable.ite (h_set_1 _) (by fun_prop) (by fun_prop)
   have h_meas_2 b : Measurable fun h ↦ {s | 0 < pullCount A (bestArm ν) s h ∧
       empMean A R (bestArm ν) s h + ucbWidth A (c * σ2) (bestArm ν) s h <
           (ν (bestArm ν))[id]}.indicator (1 : ℕ → ℕ) b := by
-    simp only [id_eq, Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
+    simp only [id_eq, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply]
     exact Measurable.ite (h_set_2 _) (by fun_prop) (by fun_prop)
   calc ∫⁻ ω, pullCount A a n ω ∂P
   _ ≤ ∫⁻ ω, C a + 1 +