Expression which can #eval cannot be parsed

Stream: lean4

[Leni Aniva]

I have this expression

-- Gives 10
#eval let x := 5; x + x

However if I run this through

Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := input)
    (fileName := "<stdin>")

then I get the error <stdin>:1:8: expected term. The same thing happens with let x := 5\n x + x. How can I make this expression go through parsing?

[Sebastian Ullrich]

Do you have an #mwe?

[Leni Aniva]

Sebastian Ullrich said:

Do you have an #mwe?

Yes. (this has some extra stuff since even if the syntax passes parsing it has to parse elaboration too

import Lean

open Lean

def str_to_name (s: String): Name :=
  (s.splitOn ".").foldl Name.str Name.anonymous

def subroutine : Elab.TermElabM Unit := do
  let input := "let x : = 5\n x + x"
  let stx := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := input)
    (fileName := "<stdin>")
  match stx with
  | .error str => IO.println str
  | .ok stx =>
    let expr ← Elab.Term.elabTerm (stx := stx) (expectedType? := .none)
    let expr ← instantiateMVars expr
    let str := toString <| (← Meta.ppExpr expr)
    IO.println str

def main : IO Unit := do
  let env: Environment ← importModules
    (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
    (opts := {})
    (trustLevel := 1)
  let coreM := Meta.MetaM.run' <| Elab.Term.TermElabM.run' subroutine
  let coreContext: Lean.Core.Context := {
    currNamespace := str_to_name "Roundtrip",
    openDecls := [],     -- No 'open' directives needed
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0], lines := #[1] }
  }
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
    IO.println s!"{← exception.toMessageData.toString}"
  | .ok a            =>
    IO.println "Finished"