From 8562dc067a8ab1db92f07351d564c6beabcb8106 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 1 Jan 2026 11:33:42 +0800 Subject: [PATCH 1/6] chore: bump toolchain to v4.26.0 --- Algorithm/Graph/Dijkstra.lean | 26 ++++--- docbuild/lake-manifest.json | 142 ---------------------------------- docbuild/lakefile.toml | 2 +- docbuild/lean-toolchain | 2 +- lake-manifest.json | 24 +++--- lakefile.lean | 2 +- lean-toolchain | 2 +- 7 files changed, 31 insertions(+), 169 deletions(-) delete mode 100644 docbuild/lake-manifest.json diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean index 8dbe3ee..de968b9 100644 --- a/Algorithm/Graph/Dijkstra.lean +++ b/Algorithm/Graph/Dijkstra.lean @@ -6,11 +6,12 @@ Authors: Yuyang Zhao import Algorithm.Data.Classes.ToList import Algorithm.Data.Classes.IndexedMinHeap import Algorithm.Data.Graph.AdjList +import Mathlib.Algebra.Order.Monoid.Canonical.Defs import Mathlib.Algebra.Order.Monoid.WithTop import Mathlib.Data.Finset.Card import Mathlib.Data.Fintype.Basic import Mathlib.Data.Set.Lattice -import Mathlib.Algebra.Order.Monoid.Canonical.Defs +import Mathlib.Tactic.Order section -- should be in mathlb variable {γ : Type*} @@ -415,7 +416,7 @@ lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType) (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) : (dijkstraStep g c heap res hMinIdx).2[v] = ⊤ ↔ v ≠ minIdx heap ∧ res[v] = ⊤ := by - letI : DecidableEq V := by classical infer_instance + let +nondep : DecidableEq V := by classical infer_instance simp [dijkstraStep_snd_getElem] split_ifs with h · simpa [h] @@ -493,7 +494,7 @@ lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType) · rintro ⟨x, hx, rfl, rfl, rfl⟩ exact ⟨homOfStar x hx, rfl⟩ · rintro ⟨⟨⟨v, x, hx⟩, ⟨fste, snde⟩⟩, rfl⟩ - simp at fste snde; subst fste snde + simp only [EmbeddingLike.apply_eq_iff_eq] at fste snde; subst fste snde exact ⟨x, hx, rfl, rfl⟩ lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType) @@ -504,8 +505,8 @@ lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType) (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) : (dijkstraStep g c heap res hMinIdx).1[v] = ⊤ ↔ (heap[v] = ⊤ ∧ v ∉ g..succSet {minIdx heap}) ∨ v = minIdx heap ∨ res[v] ≠ ⊤ := by - letI : DecidableEq V := by classical infer_instance - letI : DecidableEq Info := by classical infer_instance + let +nondep : DecidableEq V := by classical infer_instance + let +nondep : DecidableEq Info := by classical infer_instance dsimp rw [dijkstraStep_fst_getElem (spec₁ := spec₁)] simp? [hMinIdx, - not_or] says @@ -542,8 +543,8 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) (h : dijkstraStep.Spec g c init heap res) (hMinIdx : heap[minIdx heap] ≠ ⊤) : dijkstraStep.Spec g c init (dijkstraStep g c heap res hMinIdx).1 (dijkstraStep g c heap res hMinIdx).2 := by - letI : DecidableEq V := by classical infer_instance - letI : DecidableEq Info := by classical infer_instance + let +nondep : DecidableEq V := by classical infer_instance + let +nondep : DecidableEq Info := by classical infer_instance obtain ⟨h₁, h₂, h₃, h₄⟩ := h have rMinIdx : res[minIdx heap] = ⊤ := (h₁ _).resolve_left hMinIdx constructor @@ -655,11 +656,14 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) exact ⟨v, t, hv, ht, p, e, .nil, rfl⟩ obtain ⟨v, w, hv, hw, psv, evw, pwt, rfl⟩ := this _ rMinIdx p simp only [Quiver.Path.cost_comp, Quiver.Path.cost_cons, WithTop.coe_add, ← add_assoc] - apply le_add_right obtain ⟨d, hd, (⟨rfl, h₂⟩ | ⟨-, h₂⟩)⟩ := h₂ w hw; · exact (h₂ v hv).elim evw replace h₃ := (h₃ v hv).2 s inits psv - exact (getElem_minIdx_le heap w).trans <| hd.symm ▸ - (min_le_right _ _).trans <| (h₂ v hv evw).trans (add_le_add_right h₃ _) + calc + heap[minIdx heap] + ≤ heap[w] := getElem_minIdx_le heap w + _ ≤ d := by order only [hd] + _ ≤ res[v] + c (evw : E g).info := h₂ v hv evw + _ ≤ _ := by grw [h₃]; exact self_le_add_right _ _ · intro v -- simp? [dijkstraStep_snd_getElem_eq_top, dijkstraStep_fst_getElem_eq_top (spec₁ := h₁), h₄] simp only [ne_eq, h₄, dijkstraStep_snd_support, @@ -690,7 +694,7 @@ where else let hr := g..dijkstraStep c heap res hh have : Fintype.card {v : V | hr.2[v] = ⊤} < Fintype.card {v : V | res[v] = ⊤} := by - letI : DecidableEq V := by classical infer_instance + let +nondep : DecidableEq V := by classical infer_instance simp only [dijkstraStep_snd_getElem_eq_top, ne_eq, Set.coe_setOf, hr] exact Fintype.card_lt_of_injective_of_notMem (fun ⟨v, hv⟩ ↦ ⟨v, hv.2⟩) (by intro ⟨v, hv⟩ ⟨w, hw⟩; simp) diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json deleted file mode 100644 index 5f70058..0000000 --- a/docbuild/lake-manifest.json +++ /dev/null @@ -1,142 +0,0 @@ -{"version": "1.1.0", - "packagesDir": "../.lake/packages", - "packages": - [{"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "2679356b3372d52f76d6d984eef16cade7956e0c", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0-rc2", - "inherited": false, - "configFile": "lakefile.lean"}, - {"type": "path", - "scope": "", - "name": "algorithm", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../", - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "106abeac8ee53a047b238976281b0e5017bded8a", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "3ab4379b2b92448717de66b7d3e254ac1487aede", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "d5c9558e75342a10d6321e6a8c798a14f68ae23c", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0-rc2", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "74835c84b38e4070b8240a063c6417c767e551ae", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.82", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "9c70abdd9215b76019340fad65138e2e8d21843e", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "afe9302d9243cee630b0be95322b38b90342ddbf", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "docbuild", - "lakeDir": ".lake"} diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml index 520fd23..26784eb 100644 --- a/docbuild/lakefile.toml +++ b/docbuild/lakefile.toml @@ -10,4 +10,4 @@ path = "../" [[require]] scope = "leanprover" name = "doc-gen4" -rev = "v4.26.0-rc2" +rev = "v4.26.0" diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain index be1fbc3..e59446d 100644 --- a/docbuild/lean-toolchain +++ b/docbuild/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0-rc2 +leanprover/lean4:v4.26.0 diff --git a/lake-manifest.json b/lake-manifest.json index 7c79f12..c2c7d5f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d5c9558e75342a10d6321e6a8c798a14f68ae23c", + "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0-rc2", + "inputRev": "v4.26.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "74835c84b38e4070b8240a063c6417c767e551ae", + "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", + "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3", + "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710", + "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.82", + "inputRev": "v0.0.83", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9c70abdd9215b76019340fad65138e2e8d21843e", + "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3", + "rev": "9312503909aa8e8bb392530145cc1677a6298574", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "afe9302d9243cee630b0be95322b38b90342ddbf", + "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9", + "rev": "933fce7e893f65969714c60cdb4bd8376786044e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0-rc2", + "inputRev": "v4.26.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "algorithm", diff --git a/lakefile.lean b/lakefile.lean index 3bc251b..a164bde 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require "leanprover-community" / "mathlib" @ git "v4.26.0-rc2" +require "leanprover-community" / "mathlib" @ git "v4.26.0" abbrev algorithmOnlyLinters : Array LeanOption := #[ ⟨`linter.mathlibStandardSet, true⟩, diff --git a/lean-toolchain b/lean-toolchain index be1fbc3..e59446d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0-rc2 +leanprover/lean4:v4.26.0 From baa3f31fff28520f4ff82a6de8084ba26ce08080 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 1 Jan 2026 14:21:17 +0800 Subject: [PATCH 2/6] fix --- Algorithm/Data/Classes/MultiBag.lean | 10 ++++------ Algorithm/Data/DFinsupp'/Defs.lean | 3 ++- Algorithm/Data/UnionFind.lean | 5 +++-- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Algorithm/Data/Classes/MultiBag.lean b/Algorithm/Data/Classes/MultiBag.lean index d17973a..8e0d15c 100644 --- a/Algorithm/Data/Classes/MultiBag.lean +++ b/Algorithm/Data/Classes/MultiBag.lean @@ -29,12 +29,10 @@ attribute [simp] count_eq_count_toMultiset toMultiset_insert section MultiBag.ReadOnly variable {C α : Type*} [MultiBag.ReadOnly C α] (c : C) -variable [DecidableEq α] +theorem count_eq_zero {a : α} {c : C} : count a c = 0 ↔ a ∉ c := by + classical exact count_eq_count_toMultiset a c ▸ count_toMultiset_eq_zero -theorem count_eq_zero {a : α} {c : C} : count a c = 0 ↔ a ∉ c := - count_eq_count_toMultiset a c ▸ count_toMultiset_eq_zero - -theorem count_ne_zero {a : α} {c : C} : count a c ≠ 0 ↔ a ∈ c := - count_eq_count_toMultiset a c ▸ count_toMultiset_ne_zero +theorem count_ne_zero {a : α} {c : C} : count a c ≠ 0 ↔ a ∈ c := by + classical exact count_eq_count_toMultiset a c ▸ count_toMultiset_ne_zero end MultiBag.ReadOnly diff --git a/Algorithm/Data/DFinsupp'/Defs.lean b/Algorithm/Data/DFinsupp'/Defs.lean index 54d832a..b22e3e3 100644 --- a/Algorithm/Data/DFinsupp'/Defs.lean +++ b/Algorithm/Data/DFinsupp'/Defs.lean @@ -542,7 +542,8 @@ instance decidableDefault : DecidablePred (Eq (default : Π₀' i, [β i, d i])) theorem support_subset_iff {s : Set ι} {f : Π₀' i, [β i, d i]} : ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = d i := by - simp [Set.subset_def]; exact forall_congr' fun i => not_imp_comm + simp? [Set.subset_def] says simp only [Set.subset_def, SetLike.mem_coe, mem_support_toFun, ne_eq] + exact forall_congr' fun i => not_imp_comm theorem support_single_ne {i : ι} {b : β i} (hb : b ≠ d i) : (single d i b).support = {i} := by diff --git a/Algorithm/Data/UnionFind.lean b/Algorithm/Data/UnionFind.lean index f86e787..0b1dbfe 100644 --- a/Algorithm/Data/UnionFind.lean +++ b/Algorithm/Data/UnionFind.lean @@ -172,6 +172,7 @@ lemma find_snd_root (self : UnionFind ι P S) (i : ι) : (self.find i).snd.root = self.root := rootCore_findAux_snd self.parent self.wf i _ +omit [DecidableEq ι] in lemma wellFounded_assocArraySet (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) (i r : ι) (hr : parent[r] = r) : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[i ↦ r][k] := by @@ -179,6 +180,7 @@ lemma wellFounded_assocArraySet (parent : P) (wf : WellFounded fun j k : ι ↦ induction x using wf.induction with | h x ih => refine ⟨x, fun p ⟨hpx, h⟩ ↦ ?_⟩ + classical simp only [all_valid, getElem_setElem] at h split_ifs at h with hx · subst hx h @@ -226,7 +228,6 @@ lemma setParent_root (parent : P) (size : S) (wf : WellFounded fun i j : ι ↦ unfold rootCore dsimp split_ifs <;> aesop - termination_by wf.wrap k decreasing_by simp_wf; tauto @@ -470,7 +471,7 @@ def union (self : UnionFind ι P S) (i j : ι) : UnionFind ι P S := MutableQuotient.map self (fun x ↦ x.union i j) fun _ _ h ↦ by simp only [UnionFindImpl.UnionFindWF.union_root] congr! 1 - simp [h] -- `simp only [h]` made no progress + generalize_proofs h₁ h₂ h₃ h₄; revert h₁ h₂ h₃ h₄; rw [h]; intros rw [UnionFindImpl.UnionFindWF.size_eq_of_root_eq (h := h)] rw [UnionFindImpl.UnionFindWF.size_eq_of_root_eq (h := h)] From 86229ca852dc3d7a825d15fec4809bc3f259746c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 1 Jan 2026 14:23:57 +0800 Subject: [PATCH 3/6] fix --- .github/workflows/docs.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 82c3cce..7c77e49 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -26,6 +26,7 @@ jobs: run: | lake exe graph ./docbuild/algorithm.html cd docbuild + lake exe cache get lake build Algorithm:docs lake build Algorithm:docsHeader - name: Setup Pages From b4ebabc5671cdbe8c26458884f947fd7c476e278 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 1 Jan 2026 14:49:13 +0800 Subject: [PATCH 4/6] Update noshake.json --- scripts/noshake.json | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/scripts/noshake.json b/scripts/noshake.json index 3ac0266..005a28e 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -137,6 +137,7 @@ "Mathlib.Tactic.NormNum.Eq", "Mathlib.Tactic.NormNum.Ineq", "Mathlib.Tactic.NthRewrite", + "Mathlib.Tactic.Order", "Mathlib.Tactic.PPWithUniv", "Mathlib.Tactic.Peel", "Mathlib.Tactic.Polyrith", @@ -193,6 +194,4 @@ "Mathlib.Util.WithWeakNamespace", "Qq"], "ignoreAll": - ["Batteries.Tactic.Basic", "Mathlib.Mathport.Syntax", "Mathlib.Tactic.Linter"], - "ignore": - {}} + ["Batteries.Tactic.Basic", "Mathlib.Mathport.Syntax", "Mathlib.Tactic.Linter"]} From c26fb270efc37757a0d32b6ed4d7c3dc3463f94c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 1 Jan 2026 15:31:19 +0800 Subject: [PATCH 5/6] try --- .github/workflows/docs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 7c77e49..91365d3 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -26,7 +26,7 @@ jobs: run: | lake exe graph ./docbuild/algorithm.html cd docbuild - lake exe cache get + MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 lake build Algorithm:docs lake build Algorithm:docsHeader - name: Setup Pages From c5390f07cc00c43114413595f3148c12cc700cdd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 1 Jan 2026 16:03:35 +0800 Subject: [PATCH 6/6] Update docs.yml --- .github/workflows/docs.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 91365d3..e5b71d2 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -28,7 +28,6 @@ jobs: cd docbuild MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 lake build Algorithm:docs - lake build Algorithm:docsHeader - name: Setup Pages uses: actions/configure-pages@v4 - name: Upload artifact