advice for running MetaM code easily

Stream: lean4

[Scott Morrison]

Sometimes I want to run small fragments of code to test them out. Often I use something like:

#eval show MetaM _ from do
  let n := 7
  guard $ n > 5

which works great.

But how do I print stuff?

The shortest I've found so far is:

set_option trace.debug true

#eval show MetaM _ from do
  let n := 7
  guard $ n > 5
  trace[debug] "{9}"

Anything snappier? logInfo succeeds, but the messages don't seem to appear.

[Thomas Murrills]

It might be cool to have something like the following macro somewhere:

macro "trace!" s:interpolatedStr(term) : term =>
  `(addRawTrace (s! $s))

#eval show MetaM _ from do let a := 5; trace! "{a}" -- 5

[Thomas Murrills]

(addRawTrace (s! "{a}") is the extant, macroless version that I know of, but I'm not sure it counts as snappier!)

[Gabriel Ebner]

This would work after lean4#1967.

[Gabriel Ebner]

In the meantime, I usually declare an elaborator if I want to test code.

elab "foo" : command => liftTermElabM do
  let n := 7
  guard $ n > 5
  logInfo m!"{n}"
foo

[Mario Carneiro]

the defined-on-the-spot elaborator use case is mostly covered by run_cmd / run_tac / run_elab, although it does require an import

[Thomas Murrills]

(btw, here's a better version of trace! patterned more closely after trace[...] for when you just don't feel like setting an option:)

macro "trace!" s:interpolatedStr(term) : doElem => do
  let msg ← if s.raw.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
  `(doElem| Lean.addRawTrace $msg)

#eval show MetaM _ from do -- 7
  let n := 7
  guard $ n > 5
  trace! "{n}"