Undesired "panic" during initialization

Stream: lean4

[Yicheng Qian]

I came across an unexpected "panic" issue when working on a project. I've managed to reduce the problem to a mwe

1. SetprecompileModules to true in lakefile (I'm not sure whether this matters)

2. Put
   def should_not_panic : Nat := Id.run <| do while true do if 1 < 2 then return 10 panic! "Unexpected error"
   in A.lean

3. Import A.lean from B.lean

4. Open A.lean in VSCode, and the panic in should_not_panic is triggered

The problem only occurs when the panic is closed. For example the following modification of should_not_panic does not cause the above problem
def should_not_panic (q : Nat) : Nat := Id.run <| do while true do if 1 < 2 then return 10 panic! s!"Unexpected error when processing {q}"

[Yicheng Qian]

The lean version is leanprover/lean4:nightly-2023-08-19.