ci: split compile vs doc generation into separate jobs (non-blocking docs)

.github/workflows/ci.yml

@@ -53,9 +53,6 @@ jobs:
       - name: Build Foundation
         run: lake build Foundation
 
-      - name: Build docs
-        run: lake build Foundation:docs
-
       - name: Pack project cache
         run: lake pack
       - name: Save project cache
@@ -66,6 +63,39 @@ jobs:
           path: .lake/Foundation-x86_64-unknown-linux-gnu.tar.gz
           key: ${{ steps.cache-restore.outputs.cache-primary-key }}
 
+  docs:
+    name: Build docs
+    runs-on: ubuntu-latest
+    needs: build
+    # Non-blocking: doc-gen4 tooling breakage must not gate a green library build.
+    continue-on-error: true
+    steps:
+      - uses: actions/checkout@v6
+      - name: Setup elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      # Reuse the library build cached by the `build` job (same key) so docs
+      # don't recompile Foundation.
+      - name: Get Mathlib cache
+        run: lake exe cache get
+      - name: Restore cache
+        id: cache-restore
+        uses: actions/cache/restore@v5
+        with:
+          path: .lake/Foundation-x86_64-unknown-linux-gnu.tar.gz
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref_name }}-${{ github.sha }}
+          restore-keys: |
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref_name }}
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+      - name: Unpack project cache
+        if: hashFiles('.lake/Foundation-x86_64-unknown-linux-gnu.tar.gz') != ''
+        run: lake unpack
+
+      - name: Build docs
+        run: cd docbuild && lake build Foundation:docs
+
       - uses: ts-graphviz/setup-graphviz@v2
       - name: Generate import graph
         run: |
@@ -78,7 +108,7 @@ jobs:
         with:
           name: lean-artifacts
           path: |
-            .lake/build/doc
+            docbuild/.lake/build/doc
             import_graph.png
             import_graph.pdf
             import_graph.html
@@ -123,7 +153,7 @@ jobs:
     runs-on: ubuntu-latest
     if: github.ref == 'refs/heads/master'
     needs:
-      - build
+      - docs
       - check-references
     environment:
       name: github-pages
@@ -138,7 +168,7 @@ jobs:
           name: lean-artifacts
       - name: Copy from artifacts to pages
         run: |
-          cp -r "$GITHUB_WORKSPACE/.lake/build/doc" pages/docs
+          cp -r "$GITHUB_WORKSPACE/docbuild/.lake/build/doc" pages/docs
           cp "$GITHUB_WORKSPACE/import_graph.png" \
              "$GITHUB_WORKSPACE/import_graph.pdf" \
              "$GITHUB_WORKSPACE/import_graph.html" \

Foundation.lean

@@ -1,4 +1,4 @@
-module  -- shake: keep-all
+module  -- shake: keep-all --deprecated_module: ignore
 
 public import Foundation.FirstOrder.Arithmetic.Basic
 public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy

Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean

@@ -315,7 +315,7 @@ set_option linter.flexible false in
 
 lemma exsClosure : {n : ℕ} → {φ : Semiformula L ξ n} → Hierarchy 𝚺 (s + 1) φ → Hierarchy 𝚺 (s + 1) (exsClosure φ)
   | 0, _, hp => hp
-  | n + 1, φ, hp => by simpa using exsClosure (hp.exs)
+  | n + 1, φ, hp => exsClosure (φ := ∃⁰ φ) hp.exs
 
 instance : LogicalConnective.AndOrClosed (Hierarchy Γ s : Semiformula L ξ k → Prop) where
   verum := verum _ _ _

Foundation/FirstOrder/Arithmetic/Exponential/Bit.lean

@@ -186,10 +186,10 @@ end model
 section model
 
 lemma mem_iff_mul_exp_add_exp_add {i a : V} : i ∈ a ↔ ∃ k, ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + Exp.exp i + r := by
-  simpa [mem_iff_bit, exp_succ] using lenbit_iff_add_mul (exp_pow2 i) (a := a)
+  simpa [mem_iff_bit, exp_succ] using! lenbit_iff_add_mul (exp_pow2 i) (a := a)
 
 lemma not_mem_iff_mul_exp_add {i a : V} : i ∉ a ↔ ∃ k, ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + r := by
-  simpa [mem_iff_bit, exp_succ] using not_lenbit_iff_add_mul (exp_pow2 i) (a := a)
+  simpa [mem_iff_bit, exp_succ] using! not_lenbit_iff_add_mul (exp_pow2 i) (a := a)
 
 section empty
 
@@ -239,13 +239,13 @@ instance : LawfulSingleton V V where
     i ∈ insert j a ↔ i = j ∨ i ∈ a := by
   by_cases h : j ∈ a <;> simp [h, insert_eq, bitInsert]
   · by_cases e : i = j <;> simp [h, e]
-  · simpa [exp_inj.eq_iff] using
+  · simpa [exp_inj.eq_iff] using!
       lenbit_add_pow2_iff_of_not_lenbit (exp_pow2 i) (exp_pow2 j) h
 
 @[simp] lemma mem_bitRemove_iff {i j a : V} :
     i ∈ bitRemove j a ↔ i ≠ j ∧ i ∈ a := by
   by_cases h : j ∈ a
-  · simpa [h, bitRemove, exp_inj.eq_iff] using
+  · simpa [h, bitRemove, exp_inj.eq_iff] using!
       lenbit_sub_pow2_iff_of_lenbit (exp_pow2 i) (exp_pow2 j) h
   · simp only [bitRemove, h, ↓reduceIte, ne_eq, iff_and_self]
     rintro _ rfl; contradiction
@@ -442,7 +442,7 @@ lemma nonempty_of_pos {a : V} (h : 0 < a) : ∃ i, i ∈ a := by
   simp [this] at h
 
 lemma eq_empty_or_nonempty (a : V) : a = ∅ ∨ ∃ i, i ∈ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp [emptyset_def]
   · right; exact nonempty_of_pos pos
 
@@ -457,7 +457,7 @@ lemma isempty_iff {s : V} : s = ∅ ↔ ∀ x, x ∉ s := by
 @[simp] lemma empty_subset (s : V) : ∅ ⊆ s := by intro x; simp
 
 lemma lt_of_lt_log {a b : V} (pos : 0 < b) (h : ∀ i ∈ a, i < log b) : a < b := by
-  rcases zero_le a with (rfl | apos)
+  rcases Arithmetic.zero_le a with (rfl | apos)
   · exact pos
   by_contra A
   exact not_lt_of_ge (log_monotone <| show b ≤ a by simpa using A) (h (log a) (log_mem_of_pos apos))

Foundation/FirstOrder/Arithmetic/Exponential/Log.lean

@@ -25,7 +25,7 @@ lemma log_exists_unique_pos {y : V} (hy : 0 < y) : ∃! x, x < y ∧ ∃ y' ≤
       exact ⟨x + 1, lt_of_lt_of_le (by simp [hxy]) (succ_le_double_of_pos (pos_of_gt hxy)),
         2 * y', by simpa using gey, Exponential.exponential_succ_mul_two.mpr H, by simpa using lty⟩
     case odd y IH =>
-      rcases (zero_le y : 0 ≤ y) with (rfl | pos)
+      rcases (Arithmetic.zero_le y : 0 ≤ y) with (rfl | pos)
       · simp
       · rcases (IH pos : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩
         exact ⟨x + 1, by simpa using lt_of_lt_of_le hxy (by simp),
@@ -62,7 +62,7 @@ lemma log_lt_self_of_pos {y : V} (pos : 0 < y) : log y < y :=
   ((Classical.choose!_spec (log_exists_unique y)).2 pos).1
 
 @[simp] lemma log_le_self (a : V) : log a ≤ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · exact le_of_lt <| log_lt_self_of_pos pos
 
@@ -121,9 +121,9 @@ lemma log_mul_pow2 {a p : V} (pos : 0 < a) (pp : Pow2 p) : log (a * p) = log a +
   simpa using log_mul_pow2_add_of_lt pos pp pp.pos
 
 lemma log_monotone {a b : V} (h : a ≤ b) : log a ≤ log b := by
-  rcases zero_le a with (rfl | posa)
+  rcases Arithmetic.zero_le a with (rfl | posa)
   · simp
-  rcases zero_le b with (rfl | posb)
+  rcases Arithmetic.zero_le b with (rfl | posb)
   · have := lt_of_lt_of_le posa h; simp_all
   rcases log_pos posa with ⟨a', ha', Ha, _⟩
   rcases log_pos posb with ⟨b', _, Hb, hb⟩
@@ -147,12 +147,12 @@ lemma length_eq_binaryLength (a : V) : ‖a‖ = if 0 < a then log a + 1 else 0
 lemma length_of_pos {a : V} (pos : 0 < a) : ‖a‖ = log a + 1 := by simp [length_eq_binaryLength, pos]
 
 @[simp] lemma length_le (a : V) : ‖a‖ ≤ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · simp [pos, length_of_pos, ←lt_iff_succ_le, log_lt_self_of_pos]
 
 lemma length_graph {i a : V} : i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = log a ∧ i = k + 1) ∧ (a = 0 → i = 0) := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · simp [length_of_pos, pos, pos_iff_ne_zero.mp pos]
 
@@ -174,7 +174,7 @@ lemma length_two_mul_of_pos {a : V} (pos : 0 < a) : ‖2 * a‖ = ‖a‖ + 1 :=
   simp [pos, length_of_pos, log_two_mul_of_pos]
 
 lemma length_two_mul_add_one (a : V) : ‖2 * a + 1‖ = ‖a‖ + 1 := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · simp [pos, length_of_pos, log_two_mul_add_one_of_pos]
 
@@ -185,7 +185,7 @@ lemma length_mul_pow2 {a p : V} (pos : 0 < a) (pp : Pow2 p) : ‖a * p‖ = ‖a
   simp [length_of_pos, pos, pp.pos, log_mul_pow2 pos pp, add_right_comm (log a) (log p) 1]
 
 lemma length_monotone {a b : V} (h : a ≤ b) : ‖a‖ ≤ ‖b‖ := by
-  rcases zero_le a with (rfl | posa)
+  rcases Arithmetic.zero_le a with (rfl | posa)
   · simp
   · simpa [length_of_pos posa, length_of_pos (lt_of_lt_of_le posa h)]
     using log_monotone h
@@ -208,13 +208,13 @@ lemma exponential_log_le_self {a b : V} (pos : 0 < a) (h : Exponential (log a) b
   assumption
 
 lemma lt_exponential_log_self {a b : V} (h : Exponential (log a) b) : a < 2 * b := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp at h; simp [h]
   rcases log_pos pos with ⟨_, _, H, _⟩; rcases H.uniq h
   assumption
 
 lemma lt_exp_len_self {a b : V} (h : Exponential ‖a‖ b) : a < b := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp at h; simp [h]
   have : Exponential (log a + 1) b := by simpa [length_of_pos pos] using h
   rcases Exponential.exponential_succ.mp this with ⟨b, rfl, H⟩
@@ -225,7 +225,7 @@ lemma le_iff_le_log_of_exp {x y a : V} (H : Exponential x y) (pos : 0 < a) : y 
    fun h ↦ by rcases log_pos pos with ⟨a', ha', Haa', _⟩; exact le_trans (Exponential.monotone_le H Haa' h) ha'⟩
 
 lemma le_iff_lt_length_of_exp {x y a : V} (H : Exponential x y) : y ≤ a ↔ x < ‖a‖ := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simpa using pos_iff_ne_zero.mp H.range_pos
   simp [le_iff_le_log_of_exp H pos, length_of_pos pos, ←le_iff_lt_succ]
 
@@ -242,7 +242,7 @@ lemma Exponential.le_log {x y : V} (H : Exponential x y) : x ≤ log y := (le_if
 lemma Exponential.lt_length {x y : V} (H : Exponential x y) : x < ‖y‖ := (le_iff_lt_length_of_exp H).mp (by rfl)
 
 lemma lt_exponential_length {a b : V} (h : Exponential ‖a‖ b) : a < b := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp at h; simp [h]
   have : Exponential (log a + 1) b := by simpa [length_of_pos pos] using h
   rcases Exponential.exponential_succ.mp this with ⟨b, rfl, H⟩
@@ -261,7 +261,7 @@ lemma sq_len_le_three_mul (a : V) : ‖a‖ ^ 2 ≤ 3 * a := by
       _           ≤ 3 * a + 2 * a + a     := by simp [←pos_iff_one_le, pos]
       _           = 3 * (2 * a)           := by simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul]
   case odd a IH =>
-    rcases zero_le a with (rfl | pos)
+    rcases Arithmetic.zero_le a with (rfl | pos)
     · simp [←two_add_one_eq_three]
     calc
       ‖2 * a + 1‖ ^ 2 = (‖a‖ + 1) ^ 2         := by rw [length_two_mul_add_one a]
@@ -380,7 +380,7 @@ lemma bexp_two_mul {a a' x : V} (hx : 2 * x < ‖a‖) (hx' : x < ‖a'‖) :
   bexp_eq_of_exp hx (exp_bexp_of_lt hx').bit_zero
 
 lemma bexp_two_mul_succ {a i : V} : bexp (2 * a) (i + 1) = 2 * bexp a i := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   rcases show i ≥ ‖a‖ ∨ i < ‖a‖ from le_or_gt ‖a‖ i with (h | h)
   · simp [bexp_eq_zero_of_le, h, show ‖2 * a‖ ≤ i + 1 from by simp [length_two_mul_of_pos pos, h]]
@@ -421,7 +421,7 @@ instance : Bounded₂ (fbit : V → V → V) := ⟨‘1’, λ _ ↦ by simp⟩
   simp [fbit, bexp_two_mul_add_one_succ, Arithmetic.div_mul]
 
 @[simp] lemma fbit_two_mul_zero_eq_zero (a : V) : fbit (2 * a) 0 = 0 := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · have : bexp (2 * a) 0 = 1 := bexp_eq_of_exp (by simp [pos]) (by simp)
     simp [fbit, this]

Foundation/FirstOrder/Arithmetic/Exponential/Pow2.lean

@@ -142,7 +142,7 @@ lemma not_lenbit_iff_rem {i a : V} : ¬LenBit i a ↔ (a / i) % 2 = 0 := by
 @[simp] lemma LenBit.self {a : V} (pos : 0 < a) : LenBit a a := by simp [LenBit.iff_rem, pos]
 
 lemma LenBit.mod {i a k : V} (h : 2 * i ∣ k) : LenBit i (a % k) ↔ LenBit i a := by
-  have : 0 ≤ i := zero_le i
+  have : 0 ≤ i := Arithmetic.zero_le i
   rcases (eq_or_lt_of_le this) with (rfl | pos)
   · simp
   rcases h with ⟨k', hk'⟩
@@ -159,7 +159,7 @@ lemma LenBit.mod {i a k : V} (h : 2 * i ∣ k) : LenBit i (a % k) ↔ LenBit i a
 @[simp] lemma LenBit.mod_two_mul_self {a i : V} : LenBit i (a % (2 * i)) ↔ LenBit i a := LenBit.mod (by simp)
 
 lemma LenBit.add {i a b : V} (h : 2 * i ∣ b) : LenBit i (a + b) ↔ LenBit i a := by
-  have : 0 ≤ i := zero_le i
+  have : 0 ≤ i := Arithmetic.zero_le i
   rcases (eq_or_lt_of_le this) with (rfl | pos)
   · simp
   rcases h with ⟨b', hb'⟩
@@ -308,7 +308,7 @@ lemma four_le {i : V} (hi : Pow2 i) (lt : 2 < i) : 4 ≤ i := by
 
 lemma mul_add_lt_of_mul_lt_of_pos {a b p q : V} (hp : Pow2 p) (hq : Pow2 q)
     (h : a * p < q) (hb : b < p) (hbq : b < q) : a * p + b < q := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp [hbq]
   have : p ∣ q :=
     dvd_of_le hp hq (le_of_lt <| lt_of_le_of_lt (le_mul_of_pos_left pos) h)

Foundation/FirstOrder/Arithmetic/HFS/Basic.lean

@@ -64,7 +64,7 @@ lemma sUnion_lt_of_pos {a : V} (ha : 0 < a) : ⋃ʰᶠ a < a :=
     exact lt_of_lt_of_le (lt_of_mem hi) (le_log_of_mem hx)
 
 @[simp] lemma sUnion_le (a : V) : ⋃ʰᶠ a ≤ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp [←emptyset_def]
   · exact le_of_lt (sUnion_lt_of_pos pos)