Run `MetaM` in `IO`

Stream: lean4

[Tomas Skrivan]

How do I run a : MetaM Unit inside of IO Unit. I can do #eval a in a file.

My expectation is that I need to do something like a.run {} {} ... <path to lean project/file>.

Here is mwe

import Lean
import Qq
open Lean Qq

def foo : MetaM Unit := do
  let cls := q(Field ℝ)
  let inst ← Meta.synthInstance cls
  IO.println s!"instance of {← Meta.ppExpr cls} is {← Meta.ppExpr inst}"

def main : IO Unit := do
  let ctx : Core.Context := sorry
  let state : IO.Ref Core.State := sorry
  let _ ← (foo.run {} {} ctx state).toIO (fun _ => .userError "ups")

How do I properly initialize Core.Context and Core.State? For example, I want to get whole mathlib which is installed in ~/Documents/mathlib directory.

[Adam Topaz]

a.run will reduce it to CoreM, which you can then run with one of the variants of withImport.

[Tomas Skrivan]

Thanks! But the only usable function I found is in mathlib CoreM.withImportModules

import Lean
import Qq
import Mathlib

open Lean Qq

def foo : MetaM Unit := do
  let cls := q(Field ℝ)
  let inst ← Meta.synthInstance cls
  IO.println s!"instance of {← Meta.ppExpr cls} is {← Meta.ppExpr inst}"

def bar : CoreM Unit := do
  let _ ← foo.run {} {}

def main : IO Unit := do
  CoreM.withImportModules #[`Mathlib] bar

#eval main

[Tomas Skrivan]

Ohh but this does not work when I compile it and run. I guess setting up the searchPath argument somehow.

I have tried this

def main : IO Unit := do
  CoreM.withImportModules #[`Mathlib] bar
    (searchPath:= .some ["/home/tskrivan/doodle/lean/math/.lake/build",
                         "/home/tskrivan/doodle/lean/math/",
                         "/home/tskrivan/doodle/lean/math/.lake/packages/mathlib",
                         "/home/tskrivan/doodle/lean/math/.lake/packages/mathlib/.lake/build"])

but I'm getting this error

uncaught exception: object file '/home/tskrivan/doodle/lean/math/.lake/packages/mathlib/Mathlib.olean' of module Mathlib does not exist

[Eric Wieser]

You might want compile_time_search_path%

[Tomas Skrivan]

Progress! Now I'm getting

uncaught exception: Could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore').
For declarations from `Init` or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

[Tomas Skrivan]

Well this is fixable exactly with supportInterpreter := true as the error message suggests.