From 182ac126840998eeac884040454fac237c8b5c0d Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 17:46:07 +0000 Subject: [PATCH 01/12] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 7cd7ead2e..d9b09f15a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-08-19 +leanprover/lean4-pr-releases:pr-release-14844-4853259 From 2268270d4fa42c69aede6a7aa8ed33684bcb588d Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 19 Aug 2026 18:19:07 +0000 Subject: [PATCH 02/12] reimplement filterDiscrTreeM in terms of upstream mapArraysM --- aesop/Aesop/Util/Basic.lean | 48 +++++++++++-------------------------- 1 file changed, 14 insertions(+), 34 deletions(-) diff --git a/aesop/Aesop/Util/Basic.lean b/aesop/Aesop/Util/Basic.lean index 2961f0f7d..9432dec68 100644 --- a/aesop/Aesop/Util/Basic.lean +++ b/aesop/Aesop/Util/Basic.lean @@ -72,30 +72,9 @@ def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) := -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they -- turn into `Key.star`) but not fvars. -def isEmptyTrie : Trie α → Bool - | .node vs children => vs.isEmpty && children.isEmpty - -@[specialize] -private partial def filterTrieM [Monad m] [Inhabited σ] (f : σ → α → m σ) - (p : α → m (ULift Bool)) (init : σ) : Trie α → m (Trie α × σ) - | .node vs children => do - let (vs, acc) ← vs.foldlM (init := (#[], init)) λ (vs, acc) v => do - if (← p v).down then - return (vs.push v, acc) - else - return (vs, ← f acc v) - let (children, acc) ← go acc 0 children - let children := children.filter λ (_, c) => ! isEmptyTrie c - return (.node vs children, acc) - where - go (acc : σ) (i : Nat) (children : Array (Key × Trie α)) : - m (Array (Key × Trie α) × σ) := do - if h : i < children.size then - let (key, t) := children[i]'h - let (t, acc) ← filterTrieM f p acc t - go acc (i + 1) (children.set i (key, t)) - else - return (children, acc) +@[deprecated Trie.isEmptyNode (since := "2026-08-19")] +def isEmptyTrie (t : Trie α) := + t.isEmptyNode /-- Remove elements for which `p` returns `false` from the given `DiscrTree`. @@ -103,16 +82,17 @@ The removed elements are monadically folded over using `f` and `init`, so `f` is called once for each removed element and the final state of type `σ` is returned. -/ -@[specialize] -def filterDiscrTreeM [Monad m] [Inhabited σ] (p : α → m (ULift Bool)) +@[inline] +def filterDiscrTreeM [Monad m] (p : α → m Bool) (f : σ → α → m σ) (init : σ) (t : DiscrTree α) : - m (DiscrTree α × σ) := do - let (root, acc) ← - t.root.foldlM (init := (.empty, init)) λ (root, acc) key t => do - let (t, acc) ← filterTrieM f p acc t - let root := if isEmptyTrie t then root else root.insert key t - return (root, acc) - return (⟨root⟩, acc) + m (DiscrTree α × σ) := + StateT.run (s := init) do + t.mapArraysM (·.filterMapM (fun v => do + if ← p v then + return .some v + else + set (← f (← get) v) + return .none)) /-- Remove elements for which `p` returns `false` from the given `DiscrTree`. @@ -121,7 +101,7 @@ once for each removed element and the final state of type `σ` is returned. -/ def filterDiscrTree [Inhabited σ] (p : α → Bool) (f : σ → α → σ) (init : σ) (t : DiscrTree α) : DiscrTree α × σ := Id.run $ - filterDiscrTreeM (λ a => pure ⟨p a⟩) (λ s a => pure (f s a)) init t + filterDiscrTreeM (λ a => pure (p a)) (λ s a => pure (f s a)) init t end DiscrTree From 96255b884455fe28db8d72c4ebfa97b42c8abc8f Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 19:25:16 +0000 Subject: [PATCH 03/12] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index d9b09f15a..bdf620ced 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-4853259 +leanprover/lean4-pr-releases:pr-release-14844-7b84a7f From 01b84e3e38abf4aea946159d9402b2128515e4f1 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 19 Aug 2026 19:36:33 +0000 Subject: [PATCH 04/12] Add inline annotations, remove inhabited constraint --- aesop/Aesop/Util/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/aesop/Aesop/Util/Basic.lean b/aesop/Aesop/Util/Basic.lean index 9432dec68..ee12220f8 100644 --- a/aesop/Aesop/Util/Basic.lean +++ b/aesop/Aesop/Util/Basic.lean @@ -99,7 +99,8 @@ Remove elements for which `p` returns `false` from the given `DiscrTree`. The removed elements are folded over using `f` and `init`, so `f` is called once for each removed element and the final state of type `σ` is returned. -/ -def filterDiscrTree [Inhabited σ] (p : α → Bool) (f : σ → α → σ) (init : σ) +@[inline] +def filterDiscrTree (p : α → Bool) (f : σ → α → σ) (init : σ) (t : DiscrTree α) : DiscrTree α × σ := Id.run $ filterDiscrTreeM (λ a => pure (p a)) (λ s a => pure (f s a)) init t From ade1e2a51c079313b3619a605fbf3c59cb243006 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 19:44:50 +0000 Subject: [PATCH 05/12] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index bdf620ced..9797f55d7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-7b84a7f +leanprover/lean4-pr-releases:pr-release-14844-f1ca8f9 From 81ad7218b9b23a5a421dcd9a41e7c6132b11b6f5 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 20:18:40 +0000 Subject: [PATCH 06/12] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 9797f55d7..1a9e727d2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-f1ca8f9 +leanprover/lean4-pr-releases:pr-release-14844-a2d16ea From c47045a3c2e7c640b9409c55d5040e8c53004a24 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Thu, 20 Aug 2026 10:11:54 +0000 Subject: [PATCH 07/12] downstream: update repo batteries downstream-repo: batteries downstream-url: https://github.com/leanprover-community/batteries downstream-rev: nightly-testing downstream-sha: 6f9327fde05a7b7f8475971a11d8dae0d38d7eb5 From a1d45b74936cd5ec149c63cf36c5b75eb049e4c0 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Thu, 20 Aug 2026 10:13:06 +0000 Subject: [PATCH 08/12] downstream: update repo mathlib4 downstream-repo: mathlib4 downstream-url: https://github.com/leanprover-community/mathlib4-nightly-testing downstream-rev: nightly-testing downstream-sha: b878dd3f7ab9bf9046ef1c1dac56d94b8b29c9c4 From 2a243cf56a798c3e82b52abb6d1532782ca9d24d Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Thu, 20 Aug 2026 10:13:33 +0000 Subject: [PATCH 09/12] downstream: update repo verso downstream-repo: verso downstream-url: https://github.com/leanprover/verso downstream-rev: nightly-testing downstream-sha: ad4748a221f2ad0491b1045e7ca1dc25dcfa6eb0 From f48251db005676c6fb4d37878d0307b42b31e489 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Fri, 21 Aug 2026 01:07:02 +0000 Subject: [PATCH 10/12] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 1a9e727d2..bac38ec18 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-a2d16ea +leanprover/lean4-pr-releases:pr-release-14844-9bd1c68 From 0ce3f12b713ce96e596b008641d2832898257cfa Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Fri, 21 Aug 2026 03:16:06 +0000 Subject: [PATCH 11/12] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index bac38ec18..d58f07e73 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-9bd1c68 +leanprover/lean4-pr-releases:pr-release-14844-1be6c1f From 8a759936acba5fcc9def3bc1a0ce2382e5061129 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Sat, 22 Aug 2026 08:43:15 +0000 Subject: [PATCH 12/12] downstream: undo overrides --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index d58f07e73..7cd7ead2e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-1be6c1f +leanprover/lean4:nightly-2026-08-19