Unit-testing a MetaM computation

Stream: lean4

[Valentin Robert]

I have a function Expr → MetaM SomeResult that I would like to test on sample expressions, but I'd like to build these expressions using human-readable syntax.

I am struggling to find a way to run TacticM computations in #eval. While I have found a way to use functions to get something that type checks, it fails at run-time, seemingly because of the bogus MVarId I am creating, even though I think my code doesn't depend on the "goal".

Here is where I am:

-- The function I am trying to test.
def someFunction (_e : Expr) : MetaM String := return "placeholder for real function"

-- Here is the wrapper that generates an Expr. In practice, I will want this to be within some context, but even the context-free version eludes me at the moment.
def testSomeFunction : TacticM String := do
  let e ← elabTerm (← `(1 + (1 : Nat))) none
  someFunction e

-- And here is where I clumsily do my best to run the above TacticM... The crux is `Tactic.run` demands an `mvarId`, so I make a bogus one, but seemingly it's unhappy with it
#eval MetaM.run' (do
    let mvarId ← mkFreshMVarId
    Term.TermElabM.run' $ Tactic.run mvarId do
      let s ← testSomeFunction
      logInfo s
      return ()
  ) {} {}

The error is as follows:

unknown metavariable '?_uniq.19430'

How should I go about this?

[Robin Arnez]

mkFreshMVarId is the wrong function, you need to use docs#Lean.Meta.mkFreshExprMVar:

import Lean

open Lean Meta Elab Tactic

-- The function I am trying to test.
def someFunction (_e : Expr) : MetaM String := return "placeholder for real function"

-- Here is the wrapper that generates an Expr. In practice, I will want this to be within some context, but even the context-free version eludes me at the moment.
def testSomeFunction : TacticM String := do
  let e ← elabTerm (← `(1 + (1 : Nat))) none
  someFunction e

-- And here is where I clumsily do my best to run the above TacticM... The crux is `Tactic.run` demands an `mvarId`, so I make a bogus one, but seemingly it's unhappy with it
#eval MetaM.run' (do
    let mvarId ← mkFreshExprMVar none
    Term.TermElabM.run' $ Tactic.run mvarId.mvarId! do
      let s ← testSomeFunction
      logInfo s
      return ()
  ) {} {}

[Marcus Rossel]

@Valentin Robert Do you need the TacticM monad to be involved? Or do you want to test functions just in MetaM?

[Marcus Rossel]

Not sure if this might cause problems in certain cases, but this also produces the desired output:

#eval Term.TermElabM.run' do
  let s ← testSomeFunction { elaborator := .anonymous } |>.run' { goals := [] }
  logInfo s
  return ()

It's based on the implementation of Tactic.run.

[Valentin Robert]

Thanks, both answers helped!