sorry source is displayed in infoview with let

[edegeltje]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When using let, the source of a sorry is displayed in the infoview despite the pp.sorrySource option being false.

Context

The bug was noticed by @kmill on zulip, when i asked if the displayed [anonymous] for the source of a sorry inside a let should rather display a more readable value.

Steps to Reproduce

1. Paste the following code at live.lean-lang.org with Lean Nightly:

  let n : Nat := sorry
  -- hover here
  trivial

2. Hover at the comment, and look at the infoview for the assigned value of n.

Expected behavior:

The value of n is displayed as n : Nat := sorry.

Actual behavior:

The value of n is displayed as n : Nat := sorry «[anonymous]:2:17»`.

Versions

Lean 4.16.0-nightly-2025-01-20
Target: x86_64-unknown-linux-gnu

Additional Information

The lean playground uses (as of writing) no module name, which causes the source of the sorry to display as [anonymous] rather than something more useful like foo or foo.n. This bug or lack of feature is not part of this issue.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.