Repository navigation
Conversation
Member
Author
|
!bench |
|
Benchmark results for 731a182 against f68d6e9 are in. There are significant results. @Kha
New metrics (2✅, 3🟥)
Large changes (31✅, 3🟥)
Medium changes (30✅, 6🟥)
Small changes (2215✅, 52🟥)
|
github-actions
Bot
added
the
toolchain-available
Member
Author
|
!bench |
|
Benchmark results for 10c41ce against f68d6e9 are in. There are significant results. @Kha
New metrics (1✅, 4🟥)
Large changes (36✅, 2🟥)
Medium changes (32✅, 1🟥)
Small changes (2309✅, 17🟥)
|
robsimmons
added a commit
that referenced
this pull request
Oct 26, 2026
Kha
force-pushed
the
lazy-simp-discrtree
branch
from
November 7, 2026 13:40
10c41ce to
651c8d5
Compare
This adds `DiscrTree.moduleRootsOf`, which builds the tree of a single module's entries in a form suitable for storing in its olean, and `DiscrTree.ofModuleRoots`, which merges such per-module trees into one. Only the root map is built eagerly: subtrees occurring in a single module are shared with the given tries, and nodes shared between modules become the new `Trie.lazy` constructor, merged one level at a time on first access. The merged tree equals the one obtained by inserting all entries in module order, including the order of values at each node (with in-place replacement of `==`-equal values) and the iteration order of the root map. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This adds `ScopedEnvExtension.Descr.moduleIndex?` (also on `SimpleScopedEnvExtension.Descr`): a `ModuleIndex` summarizes the global entries a module exports at each olean level into a single value stored in front of them as the new `Entry.index`. On import, the summaries of all modules initialize the state, after which each global entry is added with `ModuleIndex.addImportedEntry` in place of `addEntry`, so that work covered by the summaries is not repeated per entry. For modules exported without a summary, e.g. by an older stage during bootstrapping, it is built from their entries at import. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This makes importing simp sets cheaper by storing each module's simp theorem trees in its olean (`SimpModuleIndex`) and merging them lazily on import using `DiscrTree.ofModuleRoots`, instead of inserting every imported simp theorem into the `pre`/`post` trees. Imported theorems are still replayed in order for `lemmaNames`, `erased` and the declarations to unfold, so the resulting simp sets are unchanged, including the order of theorems. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This avoids building the set of all imported simp theorem names (`SimpTheorems.lemmaNames`) when importing simp sets. `lemmaNames` now has type `SimpLemmaNames`, which offers the `contains`, `insert`, `erase`, `isEmpty`, `fold` and `toList` operations of the `PHashSet` it replaces. Imported origins are looked up in a sorted array of the module declaring their constant, found using the imported constants; origins of theorems added outside that module, or about constants with reserved names (which several modules may realize), are kept in a small set. Only if some constant is a simp theorem in both directions are all imported entries replayed in order, as adding a theorem erases its converse. `ScopedEnvExtension.ModuleIndex.addImported` now receives the summaries together with the entries of each module and adds all imported global entries, replacing `addImportedEntry`; `build` receives the environment and the module being summarized. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This moves the representation of imported simp lemma names, which looks up an entry about a constant in the array of the module declaring it and keeps only the remaining entries in a hash map, into the generic `ImportedDeclMap`, plus `DeclMap` for the changes made since the import. `SimpLemmaNames` now extends `DeclMap Origin Unit` and keeps its API. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This makes importing instances cheaper in the same way as simp sets: each module stores its instance discrimination tree and named instance entries in its olean (`InstanceModuleIndex`), and importing merges the trees lazily using `DiscrTree.ofModuleRoots` instead of inserting every instance. `Instances.instanceNames` now has type `DeclMap Name InstanceEntry`, which offers the `find?`, `contains`, `insert` and `erase` operations of the `PHashMap` it replaces; imported names are looked up in the module declaring the instance. The imported instances are unchanged, including the order in which instances of equal priority are tried. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This shrinks the per-module data of `ImportedDeclMap` in oleans by storing the keys and values of the entries a module owns as two parallel arrays (`ownedKeys`, `ownedVals`) instead of an array of pairs, and omitting the values when they are all `default`, as for simp lemma names. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This adds `Trie.suffix keys i v`, which represents the path of a single value through the remaining keys `keys[i:]` and is equivalent to `.chain` nodes for these keys ending in `.node #[v] #[]`. Insertion now creates such a leaf for the unshared tail of a path, pointing into the key array that callers usually share with the value (e.g. `SimpTheorem.keys`), instead of one `.chain` node per key. This shrinks discrimination trees in memory and the per-module trees stored in oleans, where such tails make up most nodes. `getMatch`, `getUnify` and the `Sym` matcher walk suffix leaves without allocating; other traversals unfold them one key at a time via `Trie.force`, and formatting prints them as chains. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Building the missing `ScopedEnvExtension.ModuleIndex` summaries of modules exported without one at import time is more expensive than adding their entries one by one, which made importing the stage-1 library, whose oleans are exported by stage 0, slower than before. If some imported module with global entries has no summary, all entries are now added one by one, as without `moduleIndex?`. `ModuleIndex.build` accordingly only summarizes the current module. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This adds the `Trie` accessors `hasChildren`, `starChild?`, `findChild?` and `foldChildrenM`, which view a node through `Trie.force`, and implements `getMatch`, `getUnify`, `getAllValuesForKey`, the `Sym` matcher, `Trie.foldM`, `Trie.foldValuesM` and `Trie.size` with them, so that these traversals no longer handle `chain`, `node` and `lazy` nodes separately. They still walk `suffix` leaves in dedicated loops, as unfolding a suffix allocates. `Trie.force` unfolds suffixes out of line so that the accessors inline to a tag check and do not allocate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
`mergeTries` and `mergeGroup` are now defined by well-founded recursion instead of being `partial`, so that their behavior can be verified. The termination measure is the maximal `Trie.weight` of the merged tries, which counts the remaining keys of a `suffix` as nodes. `groupByKey` records for each group that it is nonempty and that its tries satisfy a given predicate (as erased proofs), which `mergeTries` uses to show that the children it groups are lighter than the tries it merges. The values and children of a node are now taken from the new `Trie.unfold` instead of `Trie.force`; as module tries contain no `lazy` nodes, the results are unchanged, and the recursive merge is still deferred to a `Thunk`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This adds `tests/elab/discrTreeMergeSpec.lean`, which proves that forcing all `lazy` nodes of the trie under any root key of `ofModuleRoots (mods.map moduleRootsOf)` gives exactly the trie under this key after inserting the entries of all modules in order with `insertKeyValue` (`ofModuleRoots_spec`), provided all key sequences are nonempty and `==` on values is symmetric and transitive (`PartialEquivBEq`). Sequential insertion (`insertAux_den`) and the merge (`mergeTries_spec`) are both characterized by the same relation `Den` between entries and tries. As the operations of `PersistentHashMap` are `partial`, the end-to-end theorem assumes their lookup laws. An example shows that the merge drops values for a `==` that is not transitive. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This replaces `ScopedEnvExtension.ModuleIndex` and the `Entry.index` constructor by a single option on scoped environment extensions, `Descr.addImportedGlobals?`, which lets an extension add all imported global entries to its initial state itself (or decline, falling back to adding them one by one). The per-module summaries now live in a separate, typed persistent extension registered by the new `registerSimpleScopedEnvExtensionWithIndex`, which also implements the fallback for imports with modules exported without summaries. `Entry` and `exportEntriesFn` are unchanged from before the summaries were introduced. Simp extensions and the instance extension use the new function. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
`ImportedDeclMap.isOwned` decides at export which module owns an entry, and `ImportedDeclMap.ofModules` later looks up entries in the module that declares their constant according to the private view of the imported constants. Classifying in the private view as well keeps the two consistent independently of whether the environment is exporting when the summaries are built. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Kha
force-pushed
the
lazy-simp-discrtree
branch
from
November 7, 2026 13:45
651c8d5 to
301329b
Compare
Member
Author
|
!bench |
|
Benchmark results for 301329b against d4cada4 are in. There are significant results. @Kha
Large changes (50✅)
Medium changes (30✅, 2🟥)
Small changes (2082✅, 58🟥)
|
This replaces the `Descr.addImportedGlobals?` option of scoped environment extensions, which could take over adding the imported global entries or decline, by the field `Descr.importGlobals`, which creates the initial state at import from the global entries of all imported modules. Its default, the new `ScopedEnvExtension.addImportedGlobals`, adds them one by one to `mkInitial` as before; `registerSimpleScopedEnvExtensionWithIndex` falls back to it when summaries are missing. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This adds explicit cases for `DiscrTree.getMatch`, `getMatchWithExtra`, `getUnify` and `Sym.getMatch` on tries whose paths end in suffix leaves, which these lookups traverse without unfolding: suffixes starting after a branch, a `.star` inside a suffix matching a subterm with arguments, metavariables in the query skipping subterms of a suffix, and partial applications ending in a suffix matched with extra arguments. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Kha
force-pushed
the
lazy-simp-discrtree
branch
from
November 7, 2026 13:58
301329b to
61b72c2
Compare
…ries `registerSimpleScopedEnvExtensionWithIndex` connected the main extension and its summary extension through an `IO.Ref`, which together with the summary extension's export function referencing the main extension formed a cycle reachable from the environment (e.g. through attribute implementations). The object compactor recurses forever on cycles, so saving a header snapshot with `--incr-header-save` overflowed the stack. The main extension now looks up the summary extension by name at import. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 0c7651e against d4cada4 are in. There are significant results. @Kha
Large changes (47✅, 7🟥)
Medium changes (28✅, 2🟥)
Small changes (2084✅, 69🟥)
|
Kha
marked this pull request as ready for review
November 7, 2026 14:19
|
The adaptation PR for this PR is leanprover/downstream-lean4#196. |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR makes importing simp sets and instances cheaper by storing each module's discrimination trees and declaration names in its olean and merging them lazily on import, instead of adding every imported entry one by one. On
import Lean, importing the simp sets takes 94% fewer instructions (191M to 11M) and importing the instances 93% fewer (90M to 6M). The imported simp sets and instances are unchanged, including the order in which theorems and instances of equal priority are tried.DiscrTree.moduleRootsOfbuilds the tree of a single module's entries in a form suitable for storing in its olean;DiscrTree.ofModuleRootsmerges such per-module trees. Only the root map is built eagerly: subtrees occurring in a single module are shared with the olean, and nodes shared between modules become the newTrie.lazyconstructor, merged one level at a time on first access. The merged tree equals the one obtained by inserting all entries in module order, including the order of values at each node and the iteration order of the root map (PersistentHashMap.altermoves updated keys to the end of their collision node, so root keys are inserted in order of last insertion).ScopedEnvExtension.Descr.moduleIndex?(also onSimpleScopedEnvExtension.Descr) lets a scoped extension store a summary of each module's global entries in front of them (the newEntry.index) and import all global entries from these summaries. For modules exported without a summary, e.g. by an older stage during bootstrapping, it is built at import.ImportedDeclMaprepresents imported entries keyed by declarations without inserting each of them: an entry about a constant declared in the module that added it is looked up in that module's sorted array, found using the imported constants, and only the remaining entries (added by other modules, or about constants with reserved names, which several modules may realize) are kept in a hash map.DeclMapadds the changes made since the import.pre/postroots, the remaining non-theorem entries, and the theorem origins.SimpTheorems.lemmaNamesnow has typeSimpLemmaNames(aDeclMap Origin Unit), which offers thecontains,insert,erase,isEmpty,fold,foldMandtoListoperations of thePHashSetit replaces. Only if some constant is a simp theorem in both directions are all imported entries replayed in order, as adding a theorem erases its converse; this does not happen in core or Mathlib.Instances.instanceNamesnow has typeDeclMap Name InstanceEntry, which offers thefind?,contains,insertanderaseoperations of thePHashMapit replaces.getMatch/getUnifyresult order), that the simp sets and instances afterimport Leanequal sequentially built ones, and, in a package test with indices stored in oleans, priority replacement, backward theorems, re-added and newly added instances, scoped entries and private entries at both olean levels.🤖 Generated with Claude Code