perf: special case single-child nodes in DiscrTree by robsimmons · Pull Request #14805 · leanprover/lean4

robsimmons · 2026-08-17T20:08:17Z

This PR adds a new branch to the DiscrTree data structure, giving a lighter-weight way of representing discrimination tree keys with no values and a single node. The value .child k v is treated as equivalent to .node #[] #[(k, v)].

Rationale: in many applications, many or most of the nodes in a trie are single-child-no-value-carrying nodes (the robot assistant claimed this was >80% in the case of the Simp post-tree for all of Mathlib, but I wouldn't stand behind that). Special-casing this common case is often an easy win for memory usage and for performance, and this PR is in part a generalization of the match optimization from #11889.

Builds on top of #14844, which modifies the semantics of DiscrTrie.mapArrays in order to simplify downstream adaptation.

Memory usage reduction

The big change not captured in benchmarking is that this PR makes it ~9% less expensive, in terms of unshared memory usage, for a file worker to import Lean, and about ~20% less expensive for a file worker to import Mathlib. To easily see the ~9% improvement on a linux/x86 system, you can create a lean file Mem.lean

import Lean
#eval do IO.println (← IO.FS.readFile "/proc/self/smaps_rollup")

and then run these commands:

elan run leanprover/lean4:nightly-2026-08-11 \
  lean Mem.lean | grep -E 'Pss_Anon|Private_Dirty'

elan run leanprover/lean4-pr-releases:pr-release-14805-08ea7af \
  lean Mem.lean | grep -E 'Pss_Anon|Private_Dirty'

(you may need to rerun it a few times until the Pss_Anon and Private_Dirty are close to each other, the number isn't stable right when the toolchain downloads for reasons I don't fully understand)

Full Glossy Claude Writeup if that interests you.

robsimmons · 2026-08-17T20:24:48Z

!bench

leanprover-radar · 2026-08-17T20:24:55Z

Benchmark results for bbd620d against 5594178 are in. There are significant results. @robsimmons

✅ build//instructions: -11.9G (-0.10%)

Medium changes (6✅, 1🟥)

🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +1.8G (+2.03%)
✅ compiled/incr_header_save//task-clock: -159ms (-10.88%)
✅ compiled/incr_header_save//wall-clock: -162ms (-10.89%)
✅ interpreted/identifier_completion//maxrss: -12MiB (-1.66%)
✅ lake/inundation/build/clean//instructions: -8.2G (-2.59%)
✅ lake/inundation/build/clean//task-clock: -4s (-5.13%)
✅ misc/import Lean//maxrss: -7MiB (-1.34%)

Small changes (240✅, 32🟥)

✅ build/module/Init.Data.Array.Sort//instructions: -4.0M (-0.78%)
✅ build/module/Init.Data.Array//instructions: -6.0M (-1.10%)
✅ build/module/Init.Data.ByteArray//instructions: -3.8M (-0.74%)
✅ build/module/Init.Data.Float.Model.Unpacked//instructions: -5.3M (-0.99%)
✅ build/module/Init.Data.Float.Model//instructions: -5.1M (-0.95%)
✅ build/module/Init.Data.FloatArray//instructions: -4.8M (-0.90%)
✅ build/module/Init.Data.Iterators.Lemmas.Combinators//instructions: -5.7M (-1.08%)
✅ build/module/Init.Data.Iterators.Lemmas//instructions: -5.6M (-1.05%)
✅ build/module/Init.Data.List.Scan//instructions: -3.2M (-0.63%)
✅ build/module/Init.Data.Range.Polymorphic//instructions: -11.4M (-1.90%)
✅ build/module/Init.Data.Range//instructions: -5.2M (-1.04%)
✅ build/module/Init.Data.SInt//instructions: -7.9M (-1.39%)
✅ build/module/Init.Data.String.Iter//instructions: -4.4M (-0.84%)
✅ build/module/Init.Data.String.Lemmas.Pattern.Split//instructions: -6.1M (-1.14%)
🟥 build/module/Init.Data.String.Substring//instructions: +20.3M (+0.55%)
✅ build/module/Init.Data.String//instructions: -5.3M (-0.96%)
✅ build/module/Init.Data.UInt//instructions: -4.4M (-0.86%)
✅ build/module/Init.Data.Vector//instructions: -14.1M (-2.20%)
✅ build/module/Init.Data//instructions: -21.0M (-2.78%) (reduced significance based on absolute threshold)
✅ build/module/Init.Grind.Homo//instructions: -9.4M (-1.67%)
and 252 more

mathlib-lean-pr-testing · 2026-08-17T20:30:19Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5594178cba78098b6b42b5a13c3506234b64f7a5 --onto 6e91fff236ea9c68465989c1ecdf79b60e2f6bff. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-17 20:30:19)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-17 21:20:37)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 13:14:55)
💥 Mathlib branch lean-pr-testing-14805 build failed against this PR. (2026-08-21 01:11:24) View Log

leanprover-bot · 2026-08-17T20:30:22Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5594178cba78098b6b42b5a13c3506234b64f7a5 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-17 20:30:21)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-17 21:20:39)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-20 13:14:57)
✅ Reference manual branch lean-pr-testing-14805 has successfully built against this PR. (2026-08-21 01:13:00) View Log
🟡 Reference manual branch lean-pr-testing-14805 build against this PR didn't complete normally. (2026-08-21 01:14:36) View Log

downstream-lean4 · 2026-08-17T20:38:41Z

The adaptation PR for this PR is leanprover/downstream-lean4#23.

robsimmons · 2026-08-18T03:26:35Z

!bench

leanprover-radar · 2026-08-18T03:26:42Z

Benchmark results for 380b07b against 7976735 are in. There are significant results. @robsimmons

✅ build//instructions: -11.8G (-0.10%)

Medium changes (4✅, 1🟥)

🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +2.2G (+2.41%)
✅ compiled/incr_header_save//task-clock: -143ms (-9.74%)
✅ elab/string_simp_ne//maxrss: -11MiB (-0.59%)
✅ lake/inundation/build/clean//instructions: -8.4G (-2.66%)
✅ misc/import Lean//maxrss: -8MiB (-1.50%)

Small changes (236✅, 34🟥)

✅ build/module/Init.Data.Array.Sort//instructions: -4.5M (-0.87%)
✅ build/module/Init.Data.Array//instructions: -6.4M (-1.17%)
✅ build/module/Init.Data.Char.Ordinal//instructions: -23.8M (-0.40%)
✅ build/module/Init.Data.Float.Model.Unpacked//instructions: -5.4M (-1.01%)
✅ build/module/Init.Data.FloatArray//instructions: -5.5M (-1.04%)
✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic//instructions: -3.6M (-0.70%)
✅ build/module/Init.Data.Iterators.Lemmas.Combinators//instructions: -5.5M (-1.05%)
✅ build/module/Init.Data.Iterators.Lemmas.Producers//instructions: -3.0M (-0.60%)
✅ build/module/Init.Data.Iterators.Lemmas//instructions: -6.2M (-1.17%)
✅ build/module/Init.Data.List.Scan//instructions: -3.0M (-0.60%)
✅ build/module/Init.Data.Nat//instructions: -4.9M (-0.93%)
✅ build/module/Init.Data.Range.Polymorphic//instructions: -11.3M (-1.90%)
✅ build/module/Init.Data.SInt//instructions: -8.5M (-1.49%)
✅ build/module/Init.Data.String.Iter//instructions: -4.4M (-0.84%)
🟥 build/module/Init.Data.String.Substring//instructions: +27.3M (+0.73%)
✅ build/module/Init.Data.UInt//instructions: -4.6M (-0.89%)
✅ build/module/Init.Data.Vector.FinRange//instructions: -7.7M (-0.65%)
✅ build/module/Init.Data.Vector//instructions: -13.9M (-2.17%)
✅ build/module/Init.Data//instructions: -20.4M (-2.69%) (reduced significance based on absolute threshold)
✅ build/module/Init.Grind.Homo.Int8//instructions: -10.1M (-1.74%)
and 250 more

robsimmons · 2026-08-19T20:34:24Z

!bench

leanprover-radar · 2026-08-19T20:34:32Z

Benchmark results for 08ea7af against a2d16ea are in. There are significant results. @robsimmons

✅ build//instructions: -29.3G (-0.25%)

Medium changes (6✅)

✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -1.3G (-1.46%)
✅ elab/delayed_sharing//maxrss: -13MiB (-0.71%)
✅ lake/inundation/build/clean//instructions: -8.4G (-2.64%)
✅ lake/inundation/build/clean//task-clock: -4s (-5.40%)
✅ misc/import Lean//instructions: -36.0M (-2.82%)
✅ misc/import Lean//maxrss: -7MiB (-1.36%)

Small changes (336✅, 5🟥)

✅ build/module/Init.Data.Array.Sort//instructions: -4.0M (-0.76%)
✅ build/module/Init.Data.Array//instructions: -5.6M (-1.02%)
✅ build/module/Init.Data.Char.Ordinal//instructions: -25.2M (-0.43%)
✅ build/module/Init.Data.Dyadic//instructions: -4.1M (-0.79%)
✅ build/module/Init.Data.Float.Model.Format.Valid//instructions: -6.6M (-1.17%)
✅ build/module/Init.Data.Float.Model.Unpacked//instructions: -4.9M (-0.92%)
✅ build/module/Init.Data.Float.Model//instructions: -5.5M (-1.03%)
✅ build/module/Init.Data.FloatArray//instructions: -5.2M (-0.98%)
✅ build/module/Init.Data.Int//instructions: -5.4M (-1.01%)
✅ build/module/Init.Data.Iterators.Consumers//instructions: -3.6M (-0.72%)
✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic//instructions: -3.8M (-0.74%)
✅ build/module/Init.Data.Iterators.Lemmas.Combinators//instructions: -4.8M (-0.91%)
✅ build/module/Init.Data.Iterators.Lemmas//instructions: -5.8M (-1.09%)
✅ build/module/Init.Data.Nat//instructions: -4.1M (-0.78%)
✅ build/module/Init.Data.Range.Polymorphic//instructions: -11.3M (-1.90%)
✅ build/module/Init.Data.SInt//instructions: -9.6M (-1.69%)
✅ build/module/Init.Data.Slice.Array//instructions: -5.4M (-1.04%)
✅ build/module/Init.Data.String.Iter//instructions: -3.5M (-0.67%)
✅ build/module/Init.Data.String.Lemmas.Pattern.Find.Basic//instructions: -13.2M (-0.58%)
✅ build/module/Init.Data.String.Lemmas.Pattern.Find.Char//instructions: -17.8M (-0.60%)
and 321 more

nomeata · 2026-08-19T21:46:33Z

Related attempt: #12838

robsimmons · 2026-08-19T22:07:45Z

!bench mathlib

leanprover-radar · 2026-08-19T22:07:52Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@ad7f730 against leanprover-community/mathlib4-nightly-testing@5a95bed are in. There are significant results. @robsimmons

🟥 main exited with code 1

No significant changes detected.

robsimmons · 2026-08-19T22:09:34Z

Aah cool @nomeata! This is intentionally trying to be less ambitious, and @Vtec234 convinced me that there were some reasons to be cautious about the path construct — depending on insertion patterns some things might go quadratic there. If you read the claude report, it seemed convinced that given the shape of mathlib's simp data, special casing chains of stars, instead of arrays of arbitrary keys, would be a neater win.

I think your separation of leaf nodes (values) from path/branch nodes also really makes sense, but from a "that's a good refactor that makes the data structure operations clearer" sense, I doubt it would be a huge optimization.

This PR ensures that `DiscrTree` operations collapse any trie nodes that end up empty. This change allows `mapArraysM` to properly implement Aesop's filterDiscrTreeM in the [downstream adaptation PR](leanprover/downstream-lean4#24), which also deprecates `Trie.isEmptyTrie` in favor of the now-upstreamed `Trie.isEmptyNode`. Following Aesop's lead, this PR also adds @[specialize] annotations to the recursive portion of for mapArraysM and to the similarly-patterned foldM and foldValuesM. Three new test files provide coverage of these and other DiscrTree operations. This PR (and the tests) are intended to lay groundwork for leanprover#14805.

more tests, mapArrays fix and test cases better test coverage for basic discrimination tree options refactor getMatchLoop(s) for .chain Add public interface Trie.mkNode / Trie.asNode for downstream's sake formatting

This PR creates an additional view abstraction on `DiscrTree.Trie` nodes that allows nodes to be viewed and inspected without direct case analysis. This interface allows downstream code to tolerate future minor changes to DiscrTree representations (e.g. leanprover#12838 or leanprover#14805) more gracefully than is currently possible.

robsimmons force-pushed the smaller-discr-tree branch from 38be04a to bbd620d Compare August 17, 2026 20:24

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 17, 2026

robsimmons added the downstream Request a downstream-lean4 adaptation PR. label Aug 17, 2026

robsimmons force-pushed the smaller-discr-tree branch 3 times, most recently from 1e5a4d6 to 3048b87 Compare August 17, 2026 20:58

downstream-lean4 Bot mentioned this pull request Aug 17, 2026

[#14805] feat: special case single-child nodes in DiscrTree leanprover/downstream-lean4#23

Open

robsimmons force-pushed the smaller-discr-tree branch 2 times, most recently from 8c23b20 to 08ea7af Compare August 19, 2026 20:33

robsimmons changed the base branch from master to trie-map-collapse August 19, 2026 20:34

robsimmons force-pushed the trie-map-collapse branch from a2d16ea to 020ac29 Compare August 20, 2026 12:45

robsimmons force-pushed the smaller-discr-tree branch from ca29358 to d62a3fd Compare August 20, 2026 12:45

robsimmons mentioned this pull request Aug 20, 2026

fix: collapse empty DiscrTree tries #14844

Merged

robsimmons force-pushed the trie-map-collapse branch from 020ac29 to 9bd1c68 Compare August 21, 2026 00:35

robsimmons force-pushed the smaller-discr-tree branch from d62a3fd to c6f7c1a Compare August 21, 2026 00:35

github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Aug 21, 2026

mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Aug 21, 2026

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Aug 21, 2026

robsimmons force-pushed the trie-map-collapse branch from 9bd1c68 to 1be6c1f Compare August 21, 2026 02:46

robsimmons force-pushed the smaller-discr-tree branch 3 times, most recently from 73da2fd to ef67942 Compare August 23, 2026 02:42

robsimmons changed the base branch from trie-map-collapse to master August 23, 2026 02:43

robsimmons and others added 8 commits August 24, 2026 08:49

feat: create asNode/mkNode abstraction for DiscrTree

e99ccf6

Add .chain branch without use, panic everywhere

e5b0f37

introduce chain nodes; minimal changes to make some tests work

b78d4a3

fix bugs demanded by test cases

f03f6ff

more tests, mapArrays fix and test cases better test coverage for basic discrimination tree options refactor getMatchLoop(s) for .chain Add public interface Trie.mkNode / Trie.asNode for downstream's sake formatting

fix mapArraysM behavior

9770b75

finish specializing code

a8a7e9a

simplify mapArraysM

6c50064

remove TODOs, fix tests reliant on Trie.format

4ffd4cf

robsimmons force-pushed the smaller-discr-tree branch from 73da2fd to 4ffd4cf Compare August 24, 2026 12:51

robsimmons mentioned this pull request Aug 24, 2026

feat: create asNode/mkNode abstraction for DiscrTree #14911

Merged

robsimmons changed the title ~~feat: special case single-child nodes in DiscrTree~~ perf: special case single-child nodes in DiscrTree Aug 25, 2026

robsimmons mentioned this pull request Aug 26, 2026

chore: deprecate Lean.Meta.DiscrTree.elements leanprover-community/batteries#1952

Merged

Navigation Menu

Uh oh!

perf: special case single-child nodes in DiscrTree - #14805

perf: special case single-child nodes in DiscrTree#14805
robsimmons wants to merge 8 commits into
masterfrom
smaller-discr-tree

robsimmons commented Aug 17, 2026 •

edited

Loading

Uh oh!

robsimmons commented Aug 17, 2026

Uh oh!

leanprover-radar commented Aug 17, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing Bot commented Aug 17, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Aug 17, 2026 •

edited

Loading

Uh oh!

downstream-lean4 Bot commented Aug 17, 2026 •

edited

Loading

Uh oh!

robsimmons commented Aug 18, 2026

Uh oh!

leanprover-radar commented Aug 18, 2026 •

edited

Loading

Uh oh!

robsimmons commented Aug 19, 2026

Uh oh!

leanprover-radar commented Aug 19, 2026 •

edited

Loading

Uh oh!

nomeata commented Aug 19, 2026

Uh oh!

robsimmons commented Aug 19, 2026

Uh oh!

leanprover-radar commented Aug 19, 2026 •

edited

Loading

Uh oh!

robsimmons commented Aug 19, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

robsimmons commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Memory usage reduction

Uh oh!

robsimmons commented Aug 17, 2026

Uh oh!

leanprover-radar commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing Bot commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

downstream-lean4 Bot commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robsimmons commented Aug 18, 2026

Uh oh!

leanprover-radar commented Aug 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robsimmons commented Aug 19, 2026

Uh oh!

leanprover-radar commented Aug 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Aug 19, 2026

Uh oh!

robsimmons commented Aug 19, 2026

Uh oh!

leanprover-radar commented Aug 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robsimmons commented Aug 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

robsimmons commented Aug 17, 2026 •

edited

Loading

leanprover-radar commented Aug 17, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Aug 17, 2026 •

edited

Loading

leanprover-bot commented Aug 17, 2026 •

edited

Loading

downstream-lean4 Bot commented Aug 17, 2026 •

edited

Loading

leanprover-radar commented Aug 18, 2026 •

edited

Loading

leanprover-radar commented Aug 19, 2026 •

edited

Loading

leanprover-radar commented Aug 19, 2026 •

edited

Loading

robsimmons commented Aug 19, 2026 •

edited

Loading