Correct way to use `runFrontend`

Stream: lean4

[Yves Jäckle]

What's the correct way to use runFrontend ?
Consider the following MWE:

import Lean

open Lean IO FS System Elab

unsafe def sanity1 : IO Unit := do
  let path := ".lake/packages/mathlib/Mathlib/Combinatorics/Pigeonhole.lean"
  let raw ← readFile (FilePath.join (← IO.currentDir) ⟨path⟩)
  Lean.initSearchPath (← Lean.findSysroot)
  enableInitializersExecution
  let .some env ← runFrontend raw {} "dummy" `dummy | IO.println "oh noo"
  match env.find? `Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum with
  | .none => IO.println "why"
  | .some .. => IO.println "good"

--#eval sanity1

#check setEnv


unsafe def sanity2 : CoreM Unit := do
  let path := ".lake/packages/mathlib/Mathlib/Combinatorics/Pigeonhole.lean"
  let raw ← readFile (FilePath.join (← IO.currentDir) ⟨path⟩)
  Lean.initSearchPath (← Lean.findSysroot)
  enableInitializersExecution
  let env ← importModules #[⟨`Mathlib.Combinatorics.Pigeonhole,true,false⟩] {} 0 (leakEnv := true)
  setEnv env
  let .some env ← runFrontend raw {} "dummy" `dummy | IO.println "oh noo"
  match env.find? `Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum with
  | .none => IO.println "why"
  | .some .. => IO.println "good"

--#eval sanity2

On live.lean, the first eval panics, and the second one doesn't. Both print "good".
On 4.18 (where we set runtimeOnly := false), the second eval seems to work fine, until it is commented-out again, at which stage we get the panic. This is not the case in the current live.lean version.
Has anyone encountered a similar phenomenon ?
What could be the cause of this ?
I didn't test if this occurs when not using eval, but by compiling...