perf: do not reference the input string from recursive-call annotations

[leodemoura]

This PR fixes a quadratic slowdown when elaborating files with many recursive definitions. The share common exprs step of definition elaboration hashed the whole input file once per recursive call, so a file with thousands of structurally or well-founded recursive definitions could spend most of its elaboration time there.

Recursive calls are annotated with their Syntax via mkRecAppWithSyntax, so that WF and Structural can report errors at the call site. Every token of that syntax carries a SourceInfo.original whose leading and trailing substrings share the whole input string, and identifiers additionally carry rawVal, another substring of it. The annotated expression is later hash-consed by ShareCommon.shareCommon' in shareCommonPreDefs, a traversal that follows every pointer and has no identity cache for strings. It therefore reached the input string once per substring and hashed it every time. The cost per definition was proportional to the file size, and the cost per file was quadratic in the number of recursive definitions.

mkRecAppWithSyntax now stores a copy of the syntax that does not reference the input string. SourceInfo.original becomes SourceInfo.synthetic with the same range and canonical := true, and identifiers get a fresh copy of their raw value. All consumers of the annotation use it through withRef, which only needs the source range, so error positions are unchanged. The syntax tree is kept rather than reduced to a position because the partial_fixpoint error message prints the recursive call, and syntax produced by quotations may have no position to recover the text from. The only observable difference is that a comment written inside a recursive call no longer appears in that message.

The cost of the bug was (number of recursive calls) × (size of the input string). The two experiments below vary each factor separately.

The new benchmark tests/elab_bench/share_common_rec_app.lean generates the input as a string and elaborates it with Lean.Elab.process, so the source infos point at that generated string. It measures the wall-clock time of elaborating the whole input. Both rows contain the same 2000 recursive definitions; the second row appends a 4 MB comment, which is inert but makes the input string large.

Input	Before	After	Speedup
2000 recursive defs, 112 KB	5.2 s	4.9 s	1.06x
2000 recursive defs + 4 MB comment, 4.1 MB	12.2 s	5.2 s	2.3x

The first row barely changes because a 112 KB file is small, so the hashing was a small part of the 5 s of ordinary elaboration. The second row shows the bug: the comment alone cost 7 s before the fix. After the fix the two rows are equal, that is, the input size no longer matters. If this annotation ever references the input string again, the second row will jump.

The second experiment isolates the affected step. The numbers are the profiler's share common exprs time summed over all declarations of a generated file, not the whole elaboration time.

Input	Before	After	Speedup
1000 recursive defs, 56 KB	0.19 s	0.015 s	13x
8000 recursive defs, 450 KB	6.05 s	0.25 s	24x
1000 recursive defs + 2 MB comment, 2.1 MB	2.76 s	0.016 s	172x
8000 non-recursive match defs, 450 KB	0.15 s	0.17 s	none

After the fix the step costs about 0.02 ms per definition regardless of the input size: 1000 definitions take 0.015 s with or without the 2 MB comment, and 8000 take 0.25 s. Before the fix the same step grew with the input size: the 2 MB comment turned 0.19 s into 2.76 s for identical definitions, and going from 1000 to 8000 definitions multiplied the cost by 32 rather than 8, because the file grew with the definitions. The last row has no recursive calls, hence no annotation, and shows that this step was never slow on its own.

🤖 Generated with Claude Code

[leodemoura]

!bench

[leanprover-radar]

Benchmark results for 7932934 against 6d7e348 are in. There are significant results. @leodemoura

• ✅ build//instructions: -6.9G (-0.06%)

Large changes (1✅)

• ✅ misc/import Init.Prelude//instructions: -282.4M (-2.67%)

Medium changes (2✅)

• ✅ build/profile/share common exprs//wall-clock: -548ms (-7.35%)
• ✅ size/Init/.olean.private//bytes: -1MiB (-0.52%)

Small changes (96✅, 3🟥)

• 🟥 build/module/Init.Control.Lawful.MonadAttach.Lemmas//instructions: +2.6M (+0.28%)
• ✅ build/module/Init.Data.Array.Basic//instructions: -163.5M (-1.57%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.BitVec.Bitblast//instructions: -62.8M (-0.13%)
• ✅ build/module/Init.Data.FloatArray.Basic//instructions: -3.1M (-0.24%)
• ✅ build/module/Init.Data.Format.Basic//instructions: -10.9M (-0.50%)
• ✅ build/module/Init.Data.Int.Linear//instructions: -55.0M (-0.23%)
• ✅ build/module/Init.Data.Iterators.Consumers.Monadic.Loop//instructions: -15.1M (-0.37%)
• ✅ build/module/Init.Data.List.Basic//instructions: -146.8M (-1.18%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.Control//instructions: -7.1M (-0.28%)
• ✅ build/module/Init.Data.List.Impl//instructions: -19.2M (-0.28%)
• ✅ build/module/Init.Data.List.Lemmas//instructions: -106.5M (-0.30%)
• ✅ build/module/Init.Data.Nat.Basic//instructions: -20.6M (-0.31%)
• ✅ build/module/Init.Data.Nat.Fold//instructions: -13.5M (-0.17%)
• ✅ build/module/Init.Data.Nat.Lemmas//instructions: -46.7M (-0.20%)
• ✅ build/module/Init.Data.Range.Polymorphic.RangeIterator//instructions: -58.7M (-0.32%)
• ✅ build/module/Init.Data.String.Basic//instructions: -116.6M (-0.55%)
• ✅ build/module/Init.Data.String.Pattern.String//instructions: -86.6M (-0.84%)
• ✅ build/module/Init.Grind.Ring.CommSolver//instructions: -161.9M (-0.50%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Meta.Defs//instructions: -129.4M (-1.30%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Prelude//instructions: -284.0M (-2.40%) (reduced significance based on absolute threshold)
• and 79 more