Confusing crash on infinite loop in metaprogram

[david-christiansen]

Description

For some infinite loops, executing them in the interpreter leads to a crash with the message libc++abi: terminating due to uncaught exception of type lean::exception: unreachable code.

Context

This happened to me when I was working on a fairly complicated metaprogram involving environment extensions. It took a long time to figure out that it was an infinite loop - I'd have expected a program that didn't terminate, or one that crashed with the explicit infinite loop error, rather than this message.

Steps to Reproduce

Enter the following code:

import Lean
open Lean Elab Command

elab "#oops" : command => do
  let mut n : Nat := 0
  repeat
    n := n + 1
  logInfo (toString n)

#oops

Expected behavior:

Either nontermination, a heartbeats error, a maximum recursion depth error, or the "deep recursion" crash from this program:

import Lean
open Lean Elab Command

elab "#oops" : command => do
  repeat
    pure ()

#oops

libc++abi: terminating due to uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system)
interpreter stacktrace:

Actual behavior:

The Lean language server crashes with libc++abi: terminating due to uncaught exception of type lean::exception: unreachable code. This makes it difficult to figure out what's actually wrong, even when looking at it with lldb.

Versions

"4.12.0" and "4.14.0-rc2" both exhibit this on macOS 14.6.1.

Impact

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