Trouble parsing Lean code from string

Stream: lean4

[Tomas Skrivan]

How do I correctly parse and elaborate Lean code from String?

The parsing of def run (x y z : Int) : List Int := [x,y,z] fails with:

<code>:1:38: expected ']'

It looks like I'm not correctly initializing some state as the syntax for List literals does not work. Parsing def run (x y z : Int) : List Int := List.cons x (List.cons y (List.cons z List.nil)) succeeds.

So the question is, how do I properly run CommandElabM from IO?

mwe

import Lean
open Lean Meta Elab Term Command

def main : IO Unit := do

  let code := "def run (x y z : Int) : List Int := [x, y, z]"

  initSearchPath (← findSysroot)
  let env ← Lean.importModules #[{ module := `Lean }] {}
  let ctx : Command.Context := {
    fileName := "",
    fileMap := .ofString code,
    snap? := none,
    cancelTk? := none
  }
  let stateRef : IO.Ref Command.State ← IO.mkRef (mkState env)

  let runCommandElabM := fun {α} [Inhabited α] (x : CommandElabM α) => do
    match ← (x ctx stateRef).toIO' with
    | .ok _ =>
      return ()
    | .error e =>
      IO.println "elaboration failed"
      IO.println (← e.toMessageData.toString)
      return ()

  runCommandElabM do
    match Parser.runParserCategory env `command code "<code>" with
    | .error e =>
      IO.println "parsing failed"
      IO.println e
      return 1
    | .ok stx =>
      Command.elabCommand stx
      let info ← getConstInfo `run
      liftTermElabM <|
      show MetaM _ from do
      IO.println s!"run : {← ppExpr info.type}"
      pure ()
      return 0

#eval main

[Tomas Skrivan]

Also how do I parse and elaborate a whole file? with imports and multiple commands?

[Kenny Lau]

why are you in the IO monad?

[Tomas Skrivan]

yes I'm in IO

[Kenny Lau]

i said why

[Kenny Lau]

import Lean
open Lean Meta Elab Term Command

def test : CommandElabM Nat := do
  let code := "def run (x y z : Int) : List Int := [x, y, z]"
  match Parser.runParserCategory (← getEnv) `command code "<code>" with
  | .error e =>
    IO.println "parsing failed"
    IO.println e
    return 1
  | .ok stx =>
    Command.elabCommand stx
    let info ← getConstInfo `run
    liftTermElabM <|
    show MetaM _ from do
    IO.println s!"run : {← ppExpr info.type}"
    pure ()
    return 0

#eval test

[Kenny Lau]

i just changed your monad to CommandElabM and it works fine

[Tomas Skrivan]

Ohh sorry ... I want to compile small snippets of Lean code to another language. So I want to create an executable compiler from the command line.

[Tomas Skrivan]

Kenny Lau said:

i just changed your monad to CommandElabM and it works fine

I really need to run in IO as I want to create an executable.

[Kenny Lau]

@Tomas Skrivan

import Lean
open Lean Meta Elab Term Command

def test : CommandElabM Nat := do
  let code := "def run (x y z : Int) : List Int := [x, y, z]"
  match Parser.runParserCategory (← getEnv) `command code "<code>" with
  | .error e =>
    IO.println "parsing failed"
    IO.println e
    return 1
  | .ok stx =>
    Command.elabCommand stx
    let info ← getConstInfo `run
    liftTermElabM <|
    show MetaM _ from do
    IO.println s!"run : {← ppExpr info.type}"
    pure ()
    return 0

def main : IO Unit := do
  let env ← Lean.importModules #[{ module := `Lean }] {}
  let (result, _) ← Lean.Core.CoreM.toIO (liftCommandElabM test)
    { fileName := "<input>"
      fileMap := default }
    { env := env }
  IO.println result

#eval test

[Kenny Lau]

have you seen the monad map? there's no need to reinvent the wheel

[Tomas Skrivan]

It still does not work, you have to change #eval main

[Kenny Lau]

oops, forgot that

[Kenny Lau]

that's interesting that calling test works and calling main fails, lol

[Tomas Skrivan]

main is definitely missing initSearchPath (← findSysroot). When you compile it into a binary, without that line you get

uncaught exception: unknown module prefix 'Lean'

No directory 'Lean' or file 'Lean.olean' in the search path entries:

[Tomas Skrivan]

#eval can run IO, MetaM, CommandElabM, ... in the current context of the file, that is why #eval test works and #eval main does not. In main you do not have any Lean context and you have to initialize it yourself.

[Kenny Lau]

but it understood the rest of the declaration up until the ], or at least that's what the error message says

[Tomas Skrivan]

Yeah I really do not understand what is going on. The parser seems to be quite confused.

[Kenny Lau]

moreover (after i added Init to the import list) the import lists are actually the same

[Kenny Lau]

maybe the parser is running in a separate file that is not the file which imported init and lean?

[Kenny Lau]

import Lean
open Lean Meta Elab Term Command

def test : CommandElabM Nat := do
  let code := "def run (x y z : Int) : Nat := 3"
  let env ← getEnv
  -- IO.println s!"{env.allImportedModuleNames }"
  match Parser.runParserCategory env `command code "<code>" with
  | .error e =>
    IO.println "parsing failed"
    IO.println e
    return 1
  | .ok stx =>
    Command.elabCommand stx
    let info ← getConstInfo `run
    liftTermElabM <|
    show MetaM _ from do
    IO.println s!"run : {← ppExpr info.type}"
    pure ()
    return 0

def main : IO Unit := do
  let env ← Lean.importModules #[{ module := `Init.Prelude }] {}
  let (result, _) ← Lean.Core.CoreM.toIO (liftCommandElabM test)
    { fileName := "<input>"
      fileMap := default }
    { env := env }
  IO.println result

#eval test
#eval main

[Kenny Lau]

yeah i imported Init.Prelude but it doesn't know about OfNat 3 but it knew about Int and Nat

[Kenny Lau]

so the parser didn't import prelude at all

[Kenny Lau]

wait no it didn't know about Int as well, it assumed Int is a name (and used auto implicit)

[Tomas Skrivan]

Ok here is a simplified code, all the monad stuff is red herring.

import Lean

open Lean

def main : IO Unit := do
  initSearchPath (← findSysroot)
  let env ← Lean.importModules #[{ module := `Init }, { module := `Lean }, { module := `Init.Notation }, { module := `Init.Prelude }] {}
  let code := "def run (x y z : Int) : List Int := [x,y,z]"
  match Parser.runParserCategory env `command code "<code>" with
  | .error e =>
    IO.println "parsing failed"
    IO.println e
  | .ok stx =>
    IO.println "parsed string"
    IO.println stx.prettyPrint

[Tomas Skrivan]

but it still does not work

[Kenny Lau]

import Lean
open Lean Meta Elab Term Command

def test : CommandElabM Nat := do
  let code := "def run (x y z : Int) : List Int := [x,y,z]"
  let env ← getEnv
  match Parser.runParserCategory env `command code "<code>" with
  | .error e =>
    IO.println "parsing failed"
    IO.println e
    return 1
  | .ok stx =>
    Command.elabCommand stx
    let info ← getConstInfo `run
    liftTermElabM <|
    show MetaM _ from do
    IO.println s!"run : {← ppExpr info.type}"
    pure ()
    return 0

def main : IO Unit := do
  let env ← Lean.importModules #[{ module := `Init }] {} (loadExts := true)
  let (result, _) ← Lean.Core.CoreM.toIO (liftCommandElabM test)
    { fileName := "<input>"
      fileMap := default }
    { env := env }
  IO.println result

#eval test
#eval main

[Kenny Lau]

@Tomas Skrivan it turns out that when you make the environment you need to set loadExts to true, which is quite stupid

[Tomas Skrivan]

Nice find!

[Tomas Skrivan]

The docs says that you should run enableInitializersExecution before

[Tomas Skrivan]

Ok here is minimal working example:

import Lean

open Lean

unsafe def main : IO Unit := do
  initSearchPath (← findSysroot)
  enableInitializersExecution
  let env ← Lean.importModules #[{ module := `Lean }] {} (loadExts := true)
  let code := "def run (x y z : Int) : List Int := [x,y,z]"
  match Parser.runParserCategory env `command code "<code>" with
  | .error e =>
    IO.println "parsing failed"
    IO.println e
  | .ok stx =>
    IO.println "parsed string"
    IO.println stx.prettyPrint

To build an executable you also have to set supportInterpreter = true in lakefile