recover better from deterministic timeout

Stream: lean4

[Floris van Doorn]

I think it would be nice if Lean deals a bit better when it reaches a deterministic timeout. In a typical case my timeout is in the proof of a theorem, and I would like Lean to still treat that declaration as if there was a sorry/other error in the proof
In particular:

• It should show mouse-over information over the term that it parsed
• It should add the declaration (with proof sorry'd) to the environment if the type was elaborated successfully

[Geoffrey Irving]

This would be amazing.

[Kim Morrison]

RFC please! :-)

[Floris van Doorn]

lean4#3554

[Floris van Doorn]

Apparently in simple cases Lean already does this, see Leo's comment at lean4#3554. @Yaël Dillies @Geoffrey Irving if you have an example where Lean doesn't do this yet (preferably minimized), please post it there.

[Floris van Doorn]

I just tried to recreate the timeout I had in a file where I had it earlier, but I didn't manage to do that quickly.

[Floris van Doorn]

I came across this behavior again, this time with a different Lean error. I managed to find a MWE for the original issue:

def foo : Nat → Nat
| 0 => 0
| n+1 => foo n + 1

set_option maxHeartbeats 100 in /- note: when we remove this, there is a max recursion depth error,
and that also causes bar to not be added to the environment -/
theorem bar : True := by
  simp [show foo 1000 = 1000 from rfl] -- (deterministic) timeout

#print bar -- unknown constant 'bar'

The problem seems to be "if there is an error during elaboration of terms in a tactic, some tactics (like apply and simp) don't tag the term with term info anymore, so that hovers and jump-to-definition don't work anymore.
I opened this issue as lean4#3831, but afterwards I realized this is probably caused by the same code as lean4#3554.