LEAN ASSERTION VIOLATION loading Lake Workspace

Prerequisites

• [ x ] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [ x ] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [ x ] 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

I am seeing a LEAN ASSERTION VIOLATION with following code, both on v4.26.0 & https://live.lean-lang.org/#project=lean-nightly

Context

Steps to Reproduce

Code:

import Lake.CLI.Main
open Lake

def loadWorkspaceIO : IO Workspace := do
  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
  let ws? ← (loadWorkspace config).toBaseIO
  match ws? with
  | some ws => return ws
  | none => throw <| IO.userError "failed to load workspace (see log output above)"

#eval (do
  let ws ← loadWorkspaceIO
  IO.println s!"root {ws.root.name}"
)

2. In VSCode / InfoView this triggers a message: "The Lean Server has stopped processing this file:"
3. In the Lean:Editor Output tab, I see the following:

LEAN ASSERTION VIOLATION
File: /Users/runner/work/lean4/lean4/src/library/ir_interpreter.cpp
Line: 924
fn_body_tag(decl_fun_body(e.m_decl)) != fn_body_kind::Unreachable
libc++abi: terminating due to uncaught exception of type lean::unreachable_reached: 'unreachable' code was reached
[Error - 3:58:32 PM] Request textDocument/completion failed.
  Message: Server process for file:///Users/nehal/src/learn-lean/FP.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902 

Expected behavior: [Clear and concise description of what you expect to happen]
Either the root package name should print or an informative error message

Actual behavior: [Clear and concise description of what actually happens]
Lean server crashes

Versions

https://live.lean-lang.org/#project=lean-nightly
and

Lean 4.26.0
Target: arm64-apple-darwin24.6.0 macOS

Additional Information

Originally noticed in vscode, can be triggered without vscode using:

 lake env lean --run Workspace.lean 
LEAN ASSERTION VIOLATION
File: /Users/runner/work/lean4/lean4/src/library/ir_interpreter.cpp
Line: 924
fn_body_tag(decl_fun_body(e.m_decl)) != fn_body_kind::Unreachable
libc++abi: terminating due to uncaught exception of type lean::unreachable_reached: 'unreachable' code was reached

(Workspace.lean is the file above)

Other variations:
If I add to my lakefile.lean:

lean_exe ws where
  root := `Workspace
  -- Export interpreter symbols so the executable can still run Lean code if needed.
  supportInterpreter := true

Then:

lake exe ws
✖ [2/4] Building Workspace
trace: .> LEAN_PATH=/Users/nehal/src/learn-lean/.lake/packages/Cli/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/batteries/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/Qq/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/aesop/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/importGraph/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/plausible/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/packages/mathlib/.lake/build/lib/lean:/Users/nehal/src/learn-lean/.lake/build/lib/lean /Users/nehal/.elan/toolchains/leanprover--lean4---v4.26.0/bin/lean /Users/nehal/src/learn-lean/Workspace.lean -o /Users/nehal/src/learn-lean/.lake/build/lib/lean/Workspace.olean -i /Users/nehal/src/learn-lean/.lake/build/lib/lean/Workspace.ilean -c /Users/nehal/src/learn-lean/.lake/build/ir/Workspace.c --setup /Users/nehal/src/learn-lean/.lake/build/ir/Workspace.setup.json --json
info: stderr:
LEAN ASSERTION VIOLATION
File: /Users/runner/work/lean4/lean4/src/library/ir_interpreter.cpp
Line: 924
fn_body_tag(decl_fun_body(e.m_decl)) != fn_body_kind::Unreachable
libc++abi: terminating due to uncaught exception of type lean::unreachable_reached: 'unreachable' code was reached
error: Lean exited with code 134
Some required targets logged failures:
- Workspace
error: build failed

If I rework to not use #eval:

-- Workspace2.lean
import Lake.CLI.Main
open Lake

def loadWorkspaceIO : IO Workspace := do
  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
  let ws? ← (loadWorkspace config).toBaseIO
  match ws? with
  | some ws => return ws
  | none => throw <| IO.userError "failed to load workspace (see log output above)"

def main  : IO Unit := do
  let ws ← loadWorkspaceIO
  IO.println s!"root {ws.root.name}"

And add:

lean_exe ws2 where
  root := `Workspace2
  -- Export interpreter symbols so the executable can still run Lean code if needed.
  supportInterpreter := true

the lake exe ws2 does work as expected ( no errors, prints root package name)

Impact

minor

Start at src/library/ir_interpreter.cpp line 924 and reproduce with lake env lean --run Workspace.lean using the minimal example in the issue. Compare the failing #eval path with the working lake exe ws2 variant using supportInterpreter. Done means the workspace loader no longer crashes and either prints the root package name or reports an informative error.