withImportModules include Init

Stream: lean4

[James Gallicchio]

I am trying to write a program that builds some syntax, formats it, and outputs the formatted Lean to a file. But it seems the environment I am constructing does not include the prelude. MWE:

import Lean

unsafe def main : IO Unit := do
  let syn : Except _ Lean.Format ← Lean.withImportModules
    (imports := #[`Init])
    (opts := default)
    (trustLevel := 0)
    <| fun env => EIO.toIO' <|
    Lean.Core.CoreM.run'
      (ctx := {
        fileName := "Example.lean"
        fileMap := default
      })
      (s := {
        env
      })
      (do
        let opt ← Lean.liftCommandElabM (do
          let nat := Lean.mkIdent `Nat
          `(theorem hi (x : $nat) : 0 < x := sorry))
        Lean.PrettyPrinter.formatCommand opt
      )
  match syn with
  | .error exc =>
    IO.println (← exc.toMessageData.toString)
  | .ok syn =>
  IO.println (syn.pretty)

Without the Init import, it complains about the < syntax (which is declared in the prelude). With the Init import, it successfully #evals, but fails when I execute it via lake exe, with error:

uncaught exception: unknown package 'Init'

So I assume I need to configure the search path or something??

( @Mario Carneiro this is what I was asking about earlier )

[Mario Carneiro]

yes you need to configure the search path