EnvExtension crash

Stream: lean4

[Utensil Song]

The following #mwe keeps crashing:

import Lean
import Std.Util.TermUnsafe

open Lean Meta Elab Command Tactic

abbrev Entry := String
abbrev EntryList := List Entry

initialize myExt : SimplePersistentEnvExtension Entry EntryList ←
  registerSimplePersistentEnvExtension {
    addEntryFn := (·.concat)
    addImportedFn := mkStateFromImportedEntries (·.concat) {}
  }

elab (name := Proof) "Proof" _desc:interpolatedStr(term)* ":" t:tacticSeq : tactic => do
  unsafe enableInitializersExecution

  modifyEnv fun env =>
    myExt.addEntry env ""

theorem foo : 1 + 2 = 3 := by
  Proof "trivial":
    rfl

Error:

libc++abi: terminating due to uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'myExt' in the same module

Adding unsafe enableInitializersExecution following suggestions starting here didn't fix the issue.

[Scott Morrison]

Try splitting into multiple files. You can't use the extension in the same file you initialize it.

[Utensil Song]

Thanks, the comment on where this exception is thrown from suggests that in order to avoid possible bugs, this should be forbidden. I wonder if throwing an uncaught exception (when user is experimenting something wild) is common practice and should not be considered a bug.

[Scott Morrison]

Sorry, I didn't understand your reply. If you're saying that a better error message is needed here, then yes, absolutely! :-)

[Utensil Song]

Not exactly, although that's also implied. My question is: is it expected to let libc++abi to terminate Lean, or should this be a Lean level panic handling? If I'm told for the short term the former is expected then I'm comfortable with it for the time being, but I assume the latter is more expected in the long run, for a general purpose programming languages?

[Sebastian Ullrich]

This is not in the general purpose programming but metaprogramming fragment of Lean. Perhaps it would be nicer to use a common fatal panic handler but the difference in practice seems negligible.

[Utensil Song]

Yes, thanks for the clarification.