MetaM String -> IO String

Stream: lean4

[Quinn]

hi! we're (@Alok Singh ) having trouble transforming MetaM to IO

import Lean

open Lean Elab Command Term Meta Parser

def parseString (s : String) : MetaM Syntax := do
  -- Parse the string into a `Syntax` object
  let env ← getEnv
  let parserResult := Parser.runParserCategory env `module s
  -- only works on the happy path.
  return parserResult.toOption.get!

def readFile (path : String) : IO String := do
  let heading := s!"-- {path}\n"
  let contents ← IO.FS.readFile path
  pure s!"{heading}{contents}"

def main : IO Unit := do
  let contents ← readFile "Prooffusion/Fixture.lean"
  -- let (stx, s, ms) ← parseString contents |>.toIO
  IO.println contents

This is giving us

type mismatch
  fun ctxCore sCore => (parseString contents).toIO ctxCore sCore
has type
  Lean.Core.Context → Lean.Core.State → IO (Lean.Syntax × Lean.Core.State × Lean.Meta.State) : Type
but is expected to have type
  IO ?m.495 : Type

What's a cheap way to construct Core.Context and Core.State elements correctly?

[Eric Wieser]

What do you want env to contain? The environment in the loaded module?

[Quinn]

I think it should contain that, yeah. right now the IO is just for sanity check printing

[Quinn]

so it doesn't even have to contain anything, really, at first

[Adam Topaz]

There are various examples around that show how to do this

[Adam Topaz]

One way is to first convert to CoreM then use one of the variants of withImports

[Adam Topaz]

Here's an example to illustrate:

import Mathlib

open Lean

def foo (m : MetaM α) : IO α := CoreM.withImportModules #[`Mathlib] <| m.run'

#eval foo <| show MetaM Unit from do
  let env ← getEnv
  println! env.constants.toList.length

[Quinn]

cool! this works as written when mathlib is imported, still figuring out how to make it work in a mathlib-free project

[Quinn]

unknown constant 'Lean.Core.CoreM.withImportModules'

[Quinn]

oh dropping CoreM with open Lean Meta solved namespace issue

[Adam Topaz]

CoreM.withImportModules is a relatively thin wrapper around a function from core IIRC. You could therefore probably roll your own version by looking at the code

[Damiano Testa]

For minimizing imports, try adding set_option linter.minImports true right after import Mathlib and see what it says.

With meta-code it may not perform too well, but it may still be useful.