Custom Lean Server cannot find native code

Stream: lean4

[Alexander Bentkamp]

Hi, for a Lean4 version of the Natural Number Game, I am trying to modify the Lean server to accept only a series of tactics instead of a complete Lean file. It's working quite well, but fails when I try to import Mathlib4. With Mathlib4 imported, when I run the rw tactic, I get

Lean Server Server: libc++abi: terminating with uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'Mathlib.Tactic.reflExt' in the same module

I suspect that the issue is not really related to [init] declarations, but probably my custom Lean server simply cannot find the native code for the init declarations of Mathlib. Which part of Lean/Server/FileWorker.lean is responsible for loading native code?

[Sebastian Ullrich]

I think you're looking for https://leanprover-community.github.io/mathlib4_docs/Lean/ImportingFlag.html#Lean.enableInitializersExecution