prettyprinting distinct sorries in `let`

Stream: lean4

[Edward van de Meent]

consider the following example:

theorem foo : True := by
  let n : Nat := sorry
  -- n : Nat := sorry `«[anonymous]:2:17»
  admit

does it make sense to prettyprint the name in this sorry as foo.n instead, somehow? because anonymous does not seem very informative to me...

[Kyle Miller]

[anonymous] means that somehow you're in a module with no name. That's fairly unusual.

[Kyle Miller]

It seems that there's also somehow a bug here. It should print as sorry in this context.

[Edward van de Meent]

should this be reported?

[Kyle Miller]

Yes please do

[Kyle Miller]

The issue seems to be that Lean.Widget.addInteractiveHypothesisBundle uses Lean.Widget.ppExprTagged for let values, but ppExprTagged sets pp.sorrySource to true, since I assumed this function was only being used for hovers.

Writing this here to remind me where to look when I get around to it (please link to this Zulip thread!)

[Edward van de Meent]

btw, should the issue mention only the fact that it displays the source when it shouldn't, or should it also mention the [anonymous] rather than foo.n?

[Kyle Miller]

That would be an rfc

[Edward van de Meent]

fwiw, i can't seem to get the playground to display anything other than [anonymous]?

[Edward van de Meent]

is that (like you said) due to the fact that the playground operates without a surrounding module?

[Kyle Miller]

Yeah. Maybe the playground should have a module name?

[Edward van de Meent]

lean4#6715

[Edward van de Meent]

where do i file a bug/rfc with the lean playground?

[Edward van de Meent]

https://github.com/leanprover-community/lean4web?

[Edward van de Meent]

alternatively, maybe the identifiers/names shouldn't become [anonymous] just because there is no module name

[Edward van de Meent]

(or both)