Repository navigation
Raise emitter runtime recursion depth - #22
Merged
Merged
Conversation
Setting `maxRecDepth := 0` on the emitter's `Core.Context` was correct in
intent and had no effect. `emitOne` renders every type and every def body
inside `withOptions (fun _ => ppOpts)`, and `Core.withOptions` rebuilds the
context field from the options it is handed:
maxRecDepth := maxRecDepth.get options
`ppOpts` deliberately discards ambient options, so that recomputation restored
the option default for exactly the `PrettyPrinter.ppExpr` call that overflows.
Measured rather than assumed: `maxRecDepth.get ({} : Options)` is 512, while
the `Core.Context` field it replaces defaults to 1000 -- entering the block did
not merely fail to raise the depth, it lowered it.
The evidence that the previous commit did not work is direct: a
derived-alg-geo-lean CI run whose log shows `MathFormalContract: checking out
revision 'b90d0d97'`, built fresh, still died with `mfc-emit: maximum
recursion depth has been reached`.
Set through the registered option's own `set` rather than a quoted key, so it
uses the same accessor `Core.withOptions` reads it back with. The context-level
setting stays: it covers the traversal outside the pretty-printing block.
`ppOptsJson` gains the matching entry, because that record exists so the
artifact cannot claim a setting the emitter did not use. The emission schema
already admits integer `pp_options` values, so no schema change is needed.
chris-dare-dev
force-pushed
the
agent/emitter-max-rec-depth
branch
from
September 20, 2026 02:12
ed71fbb to
fb4de1b
Compare
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.
Summary
Verification
LEAN_NUM_THREADS=2 lake build MathFormalContract.EmitMotivation
The downstream derived-alg-geo-lean environment builds successfully, but three combined-emission CI runs exited with
maximum recursion depth has been reachedafter the previous finite increase to 10000. Any finite emitter depth becomes an input-size completeness ceiling: on failure no artifact is written, so the downstream vacuous-pass guard cannot evaluate the build at all.This override belongs only to the emitter's fresh process. A process failure remains possible and explicit; no partial artifact is accepted.