Trace to stdout

Stream: metaprogramming / tactics

[Logan Murphy]

Sorry if this is a noobish question. Let's say that i have something like the following in the file even.lean

import system.io
open  io

inductive even : ℕ → Prop
| zero : even 0
| add_two : ∀ n, even n → even (n+2)

meta def tactic_even : tactic unit :=
do
  tactic.repeat
  ((tactic.trace "Inductive step"; tactic.applyc ``even.add_two)
  <|>
  (tactic.trace "Base Case"; tactic.applyc ``even.zero))

def six_is_even : even 6 := by tactic_even

The trace of six_is_even is

Inductive step
Inductive step
Inductive step
Inductive step
Base Case

Is there a way I can write a function def main : io unit such that invoking lean --run even.lean would print the above trace to std output?

[Simon Hudon]

Yes you can call it using io.run_tactic in your main function

[Logan Murphy]

Oh great!

[Logan Murphy]

@Simon Hudon can you give any example of how to use it? I can't seem to figure how it works from the code itself

[Simon Hudon]

Have you tried def main : io unit := io.run_tactic tactic_even

[Logan Murphy]

Yes, but invoking

meta def main : io unit :=
do
   io.run_tactic tactic_even

prints

Inductive step
Base Case

which I'm assuming just means it traces out everything in the tactic. I'm wondering how I would use it in conjunction with a particular goal, so if I use tactic_even to show that, say, 4 is even, it would print 2 isntances of Inductive step and one instance of Base Case

(although the above version of tactic_even I provided actually prints an extra line)

[Logan Murphy]

oh, maybe I can just provide an argument to tactic_even

[Simon Hudon]

If you call lean even.lean you'll already see the printout with regards to your specific proof. Why do you need it to be called from main?

Regardless, you can do that with:

meta def main : io unit :=
do
   io.run_tactic $ do `[have : even 6], tactic_even

[Logan Murphy]

What I actually want to do is get some information from stdin in main and then show the trace of a proof about that information.

Thanks for the help!