Conversation
github-actions
Bot
added
the
toolchain-available
Kha
force-pushed
the
push-kyxzlooxsuxy
branch
5 times, most recently
from
September 27, 2026 19:53
86d67db to
a1ee135
Compare
This PR adds generation-tracked environment extensions: every modification of an extension registered with `trackGen := true` bumps a generation counter, so that whether an extension was touched during a computation can be checked by comparing generations (`EnvExtension.getGen`). `Environment.recordGen` counts the modifications of all such extensions. Generations are branch-local, so tracked extensions must use `AsyncMode.local` or `.mainOnly`. Extensions also gain a `name` for diagnostics, set automatically for persistent extensions. The generations are stored in `Environment.extGens`, indexed by a dense per-extension index (`EnvExtension.genIdx?`), rather than alongside the extension states, so that `getState` is unaffected. Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This PR lets scoped environment extensions be generation-tracked (`trackGen`). Scope operations then bump the generation exactly when they change the state in effect: activating a namespace with entries for the extension, and popping a scope whose state received local entries, entries of a namespace activated in it, or a `ScopedEnvExtension.modifyState`, which each scope-stack state tracks (`ScopedEnvExtension.State.scopeChanged`). Pushing a scope and other neutral scope operations keep the generation. Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… unification hints change (#15354) This PR makes a type class resolution cache entry record the state of the instances and unification hints its search consulted, so that the entry is no longer served once they change, even through environment changes that do not clear the cache. For example, an instance added by a command run through `liftCommandElabM` is now found by later queries in the same computation, and so are scoped instances and unification hints activated at `CoreM` level. Apart from closing such edge cases, this is a necessary prerequisite for cross-command caching. The instance and unification-hint extensions become generation-tracked. A query records the generations it read (`recordExtGenAccess`) together with its option lookups, and an entry is only reused while they are unchanged; `Environment.trackedGen` short-circuits the check, and a validated entry is re-stamped with it. The generations roll back with the environment while `Meta.Cache` survives `SavedState.restore`, so `Meta.modifyEnv` still clears the cache and `liftCommandElabM` still documents the reset. Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… environment changes (#15355) This PR makes `SavedState.restore` drop the type class resolution cache entries that were recorded after a tracked environment change it rolls back. The generations validating an entry roll back with the environment while `Meta.Cache` survives the restore, so a different change made afterwards could bring the recorded generations back and let a stale entry be served; for example, an instance added and rolled back in a failed attempt could still be returned after a different instance was added. Apart from closing such edge cases, this is a necessary prerequisite for cross-command caching, whose entries must survive backtracking without being revalidated against a rolled-back state. Along one environment lineage `Environment.trackedGen` only grows, so the restore keeps exactly the entries stamped with at most the restored value (`SynthInstanceCache.rollBack`), preserving the fills made before the rollback point. A restore that rolls back no tracked change, the common case, keeps the cache unchanged. Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This PR makes entries of declaration-keyed environment extensions write-once: writing a second entry for a declaration panics, and giving a declaration a second docstring through `add_decl_doc` is an error. A failed redeclaration also no longer replaces the declaration ranges of the existing declaration, which misdirected go-to-definition. Apart from catching accidental overwrites, this is a necessary prerequisite for validating type class resolution cache entries against declaration-keyed registries, such as equation theorems, without recording every read of them. `MapDeclarationExtension.insert` takes an `allowOverwrite` flag for deliberate replacements; no caller in core needs it. Its guard only serves to catch bugs, as the type class resolution cache will record writes through `insert`; the registries below are not recorded, so there the cache will rely on the guard. `addDeclarationRanges` keeps the first ranges reported for a declaration, and docstrings otherwise still replace an existing one, as metaprograms such as cross-reference attributes write them before a declaration's own docstring is added. The declaration-keyed registries kept in other extensions (structures, equation theorems, match equations, sparse `casesOn` declarations, definition height overrides) get the same guard, allowing idempotent re-registration; `setStructureParents` remains the one sanctioned update of a structure's entry. A rejected write keeps the existing entries, and the checks only consult the state visible on the current environment branch, so that a write never waits for the branch elaborating the declaration. The guard caught docstrings in the standard library that were silently replaced: `add_decl_doc IterM.mk` after `structure Iter` meant `Iter.mk`, and `WellFounded.extrinsicFix`, its variants, `IterM.Total` and `Iter.Total` had placeholder docstrings, kept only to satisfy the missing-docs linter, that a later `add_decl_doc` referring to subsequent declarations replaced. These now opt out of the linter instead. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This PR assigns each constant added on an environment branch the value of a counter, `Environment.constGen`, at the time it becomes observable there: on synchronous `addDecl`, asynchronous registration, and merged realizations (`Environment.constAddedGen`). A consumer that captured `constGen` at some point knows that a constant with a larger `constAddedGen` did not exist then. Constants without a registered generation, in particular imported ones, have generation 0 and so count as older than anything captured, the conservative direction. A constant keeps the generation it got first, so one announced by `addConstAsync` keeps its announcement's generation when its asynchronous branch adds it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This PR adds opt-in change logging for environment extensions holding declaration-keyed facts: every write to an extension registered with `logWrites` must either name the declaration it is about, which appends it to the new `Environment.declChangeLog`, or be explicitly marked as unlogged; any other write panics. This is a necessary prerequisite for validating type class resolution cache entries against changes of such facts, such as a post-hoc `attribute [reducible]`, without recording every read of them. The extensions that resolution reads are marked, among them classes, structures, reducibility statuses, projections, auxiliary recursors and equation and matcher info. `MapDeclarationExtension.insert`, `TagDeclarationExtension.tag`, tag and parametric attributes and scoped-extension entries name their declaration automatically; the registries relying on being write-once and realized on demand are marked unlogged. A scoped extension names the declaration of each entry (`entryDecl?`), and scope operations log the declarations of the entries they add or remove when the state in effect changes. A change is only logged if some recording computation could have observed the previous state, i.e. for a declaration added before the most recent one started (`Environment.markRecordingStart`); `Environment.checkDeclChangeLog` tells whether a result recorded at a given log position is still valid. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…larations change This PR fixes the type class resolution cache serving a result after a declaration it could have observed changed, most notably through a later `attribute [reducible]` or a scoped or local reducibility attribute coming into or going out of effect. As the cache currently lives within a single command, this is rarely visible yet, but it is a necessary prerequisite for sharing the cache across commands, where such changes are routine. Cache entries now also record the position in `Environment.declChangeLog` and `Environment.constGen` when their query started, and are only reused while every change logged since is about a declaration added later; a reducibility attribute on a declaration's own definition thus keeps entries valid, while a later `attribute [reducible]` invalidates them. The fast path checks the log position alongside `trackedGen`, and `SavedState.restore` drops the entries a rollback invalidates: those recorded after a logged change it undoes, and those recorded after a constant it removes, as a constant of the same name added later would count as unobserved. It also carries the latest recording start over the rollback, so that changes to the declarations the surviving entries observed stay logged. Restoring a state with constants the current environment lacks, as `Term.observing` followed by `applyResult` does whenever the observed elaboration created a matcher, takes the cache saved with that state instead, so that the entries the preceding rollback dropped are not recomputed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ss resolution This PR makes reading an environment extension during type class resolution panic unless the read is accounted for by the dependencies the resolution cache records: a generation-tracked extension must be read with `(genRecorded := true)` after its generation was recorded (`recordExtGenAccess`), and any other extension must log its writes (`EnvExtension.logWrites`). A missed dependency thus fails loudly instead of letting a cache entry outlive a change it depends on, which is a necessary safeguard for sharing the cache across commands. Pure extension reads cannot see `Core.Context.isRecordingDeps`, so the marker is mirrored on the environment (`Environment.isRecordingDeps`) and cleared in message and pretty-printing contexts, which may read any extension. `tests/elab/tc_cache_covered_claims.lean` exercises the extensions resolution reads. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Kha
force-pushed
the
push-kyxzlooxsuxy
branch
from
September 29, 2026 15:09
a1ee135 to
b1e98e3
Compare
Kha
changed the title
|
The adaptation PR for this PR is leanprover/downstream-lean4#112. The adaptation PR will be created or updated once the toolchain is available. |
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
1 participant
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.
Probe of the type class resolution cache stack (#15352 through
wtzl) ondownstream-greenfor a Mathlib run, not for merging.