run_term

Stream: Is there code for X?

[Adam Topaz]

We have run_cmd for running commands in CommandElabM, and run_meta for running commands in MetaM. We also have run_tac for running a tactic in TacticM within a tactic block. Do we have anything similar for term elaborators? I want to be able to write def f : Nat := elab_term do ... and construct a term in TermElabM as an Expr explicitly.

[Adam Topaz]

FWIW, I came up with this:

import Lean

open Lean Elab Term in
elab "elab_term" seq:doSeq : term => do
  ← unsafe evalTerm (TermElabM Expr) (mkApp (mkConst ``TermElabM) (mkConst ``Expr)) (← `(do $seq))

def f : Nat := elab_term
  return .lit <| .natVal 2

#eval f

[Kim Morrison]

There is already run_elab. Sorry, different use case.

[Kyle Miller]

Can you remind me what run_cmd and run_meta do that #eval doesn't?

[Adam Topaz]

I don’t know. I always end up using #eval show MetaM Unit from do … etc.

[Kyle Miller]

Answering your question, I think it might be elab% (see docs#Lean.Elab.Command.elabElab)

[Kyle Miller]

(there's also mathlib's eval% for evaluating an expression and inserting the result, but that's not quite what you're asking)

[Adam Topaz]

Thats a command elab. Would that work for terms?

[Eric Wieser]

Kyle Miller said:

Can you remind me what run_cmd and run_meta do that #eval doesn't?

import Lean

run_cmd Lean.logInfo "works"
run_elab Lean.logInfo "also works"
run_meta Lean.logInfo "works again"


#eval show Lean.Elab.Command.CommandElabM _ from Lean.logInfo "works"
#eval show Lean.Elab.Term.TermElabM _ from  Lean.logInfo "works but smaller span"
#eval show Lean.Meta.MetaM _ from Lean.logInfo "does not work"

[Kyle Miller]

The fact logInfo doesn't propagate from MetaM is a bug, I have my eye on fixing it.

[Kyle Miller]

@Adam Topaz Sorry about that last suggestion. Here it is for real: docs#Lean.byElab

[Adam Topaz]

Thanks!

[Kyle Miller]

I knew I had seen it before, but I couldn't remember the syntax. I got too excited when elab% matched anything :upside_down:

It looks like there is also a full suite of run_cmd/run_elab/run_meta (I had thought these were in mathlib, not core)

[Eric Wieser]

Should these be mentioned in the docstring of their corresponding monad types?

[Adam Topaz]

I think that’s a good idea!

[Mario Carneiro]

Kyle Miller said:

It looks like there is also a full suite of run_cmd/run_elab/run_meta (I had thought these were in mathlib, not core)

That happens a lot :upside_down: I originally added these to mathlib but I think run_cmd was wanted upstream and the others went along for the ride