proofStep discards the message log on failure, so elaboration errors surface only as `internal exception #N`

[haeliotang]

Summary

When a tactic fails during elaboration, the real diagnostic is written to the message log and an Exception.internal (the tactic-abort exception) is thrown to unwind. runProofStep's error path converts that exception to a string and never reads the message log, so the diagnostic is lost.

The same tactic through cmd reports the error precisely. The information exists; only the proofStep path drops it.

Reproduction

Lean v4.30.0-rc2, repl at f0a88bf, Mathlib pinned to match.

A — command mode

{"cmd": "theorem probeA (n : Nat) : n + 0 = n := by rw [Nat.totally_made_up_lemma]", "env": 0}

{"env": 1, "messages": [
  {"severity": "error", "data": "Unknown constant `Nat.totally_made_up_lemma`"},
  {"severity": "error", "data": "unsolved goals\nn : ℕ\n⊢ n + 0 = n"}
]}

B — proofStep mode, same tactic, same environment

{"cmd": "theorem probeB (n : Nat) : n + 0 = n := by sorry", "env": 0}
{"tactic": "rw [Nat.totally_made_up_lemma]", "proofState": 0}

{"message": "Lean error:\ninternal exception #5"}

That is the entire response — no messages, no position.

The same happens for a real lemma applied with arguments that do not unify (e.g. rw [Nat.divisors_prime_pow hp hk] where the hypotheses do not match). A parse error, by contrast, is reported correctly and with a position: rw [ gives <input>:1:4: unexpected end of input; expected ']'.

Where it happens

REPL/Main.lean, runProofStep:

try
  let proofState' ← proofState.runString s.tactic
  return .inl (← createProofStepReponse proofState' proofState)
catch ex =>
  return .inr ⟨"Lean error:\n" ++ ex.toString⟩

The success path calls createProofStepReponse, which collects proofState.newMessages old?. The catch branch returns only ex.toString.

For an Exception.internal that string is necessarily uninformative — Snapshots.lean renders it as "internal exception #" ++ toString id.idx, which is the only thing available, since internal exceptions carry an id and no message by design. The problem is not that rendering; it is that the messages accumulated before the abort are never looked at.

Why it is worth fixing

Consumers that classify prover failures cannot separate "the model named a constant that does not exist" from a genuine internal error, so the bucket reads as harness instability.

Concretely: in a corpus of 2,256 prover attempts I classified every internal exception #5 as infrastructure and reported REPL problems at 12% of errors on one problem source against 3% on another — and proposed investigating the harness. They were model errors, of the single most common kind (hallucinated lemma names). After reclassification, model-attributable errors went from 98.1% to 99.7% and genuine infrastructure failures from 1.9% to 0.3%. Measurement record: https://github.com/haeliotang/lean-corpus-audit/blob/main/findings/F6_repl_error_attribution.json

Any error taxonomy built on proofStep inherits this bias, and it points suspicion at the tooling rather than the model.

Suggested fix

In the catch branch, return the accumulated messages alongside the error string — the same proofState.newMessages the success path already collects. The abort exception itself can keep its current rendering; the logged diagnostics are what callers need.

Happy to test a patch against the reproduction above.