perf: do not reference the input string from recursive-call annotations (#15223)

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](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

Author: leodemoura

src/Lean/Elab/App.lean

@@ -2270,12 +2270,11 @@ private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array A
 
 /--
   We annotate recursive applications with their `Syntax` node to make sure we can produce error messages with
-  correct position information at `WF` and `Structural`.
+  correct position information at `WF` and `Structural`. `mkRecAppWithSyntax` stores a copy of the syntax that
+  does not reference the input string; otherwise, `Expr` traversals such as hash-consing would visit the whole
+  input string once per recursive application. The annotation must be erased before the definition is sent to
+  the kernel.
 -/
--- TODO: It is overkill to store the whole `Syntax` object, and we have to make sure we erase it later.
--- We should store only the position information in the future.
--- Recall that we will need to have a compact way of storing position information in the future anyway, if we
--- want to support debugging information
 private def annotateIfRec (stx : Syntax) (e : Expr) : TermElabM Expr := do
   if (← read).saveRecAppSyntax then
     let resultFn := e.getAppFn

src/Lean/Elab/RecAppSyntax.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+import Init.Data.String.Substring
 public import Lean.Expr
 
 public section
@@ -15,16 +16,42 @@ namespace Lean
 private def recAppKey := `_recApp
 private def recAppPosKey := `_recAppPos
 
+private def detachSourceInfo : SourceInfo → SourceInfo
+  | .original _ pos _ endPos => .synthetic pos endPos (canonical := true)
+  | info => info
+
+/--
+Copy of `stx` that does not reference the input string: every `SourceInfo.original` becomes a
+`SourceInfo.synthetic` with the same range, and identifiers get a fresh copy of their raw value.
+
+The syntax stored at a recursive application lives inside an `Expr`, so `Expr` traversals that
+follow every pointer (e.g. `ShareCommon.shareCommon'`) visit it too. The `leading` and `trailing`
+substrings of `SourceInfo.original` and the `rawVal` of identifiers all share the whole input
+string, so storing `stx` itself would make such traversals visit, and hash, the input string once
+per substring. With thousands of recursive definitions in a file, this dominates elaboration time.
+
+We keep the syntax tree instead of just its source range because error messages print the
+recursive call (see `PartialFixpoint`), and syntax produced by quotations may not have a position
+to recover the text from.
+-/
+private partial def detachSyntax : Syntax → Syntax
+  | .node info kind args => .node (detachSourceInfo info) kind (args.map detachSyntax)
+  | .atom info val => .atom (detachSourceInfo info) val
+  | .ident info rawVal val pre => .ident (detachSourceInfo info) rawVal.toString.toRawSubstring val pre
+  | .missing => .missing
+
 /--
 We store the syntax at recursive applications to be able to generate better error messages
-when performing well-founded and structural recursion.
+when performing well-founded and structural recursion. The stored syntax is detached from the
+input string, see `detachSyntax`.
 
 We additionally store the source position as an extra key, so that two recursive applications
 that are structurally identical as `Syntax` but originate from different source positions
 still produce distinct `MData`. Otherwise hashconsing or simplification can merge them and
 attribute an error to the wrong call site (issue #13444).
 -/
 def mkRecAppWithSyntax (e : Expr) (stx : Syntax) : Expr :=
+  let stx := detachSyntax stx
   let m := KVMap.empty.insert recAppKey (.ofSyntax stx)
   let m := match stx.getPos? with
     | some p => m.insert recAppPosKey (.ofNat p.byteIdx)

tests/elab_bench/share_common_rec_app.lean

@@ -0,0 +1,49 @@
+import Lean
+
+/-!
+Benchmark: hash-consing of pre-definitions (`share common exprs`) on a file with many
+recursive definitions.
+
+Recursive calls are annotated with their `Syntax`. The annotated expressions are traversed by
+`ShareCommon.shareCommon'`, which visits every object reachable from them. If the stored syntax
+kept `SourceInfo.original` infos, every one of them would point at the whole input string, and
+each recursive call would cost a hash of the whole file. The total would then be quadratic in
+the file size.
+
+The input is generated as a string and elaborated with `Lean.Elab.process`, so the source infos
+point at the generated input, not at this file. The input ends with a large comment that makes
+the input much bigger than the declarations themselves. If the cost depends on the input size,
+the padded run is much slower than the unpadded one.
+-/
+
+open Lean Elab
+
+/--
+`numDefs` structurally recursive definitions on a small inductive type, followed by a comment
+of `padding` characters.
+-/
+def mkInput (numDefs padding : Nat) : String := Id.run do
+  let mut s := "inductive N | Z | S (n : N)\n"
+  for i in [0:numDefs] do
+    s := s ++ s!"def g{i} : N → N\n  | .Z => .Z\n  | .S q => .S (g{i} q)\n"
+  s := s ++ "/-\n" ++ "".pushn 'x' padding ++ "\n-/\n"
+  return s
+
+def runBench (numDefs padding : Nat) : CoreM Unit := do
+  let input := mkInput numDefs padding
+  let t0 ← IO.monoMsNow
+  let (_, msgs) ← Lean.Elab.process input (← getEnv) {}
+  let t1 ← IO.monoMsNow
+  if msgs.hasErrors then
+    for msg in msgs.toArray do
+      IO.println (← msg.toString)
+    throwError "unexpected errors"
+  IO.println s!"measurement: defs_{numDefs}_pad_{padding} {(t1 - t0).toFloat / 1000.0} s"
+
+#eval show CoreM Unit from do
+  let bench := (← IO.getEnv "TEST_BENCH") == some "1"
+  if bench then
+    runBench 2000 0
+    runBench 2000 4000000
+  else
+    runBench 20 100000

tests/elab_bench/share_common_rec_app.lean.out.expected

@@ -0,0 +1 @@
+measurement: defs_20_pad_100000 ...