## Stream: metaprogramming / tactics

### Topic: Trace to stdout

#### Logan Murphy (Sep 22 2020 at 15:43):

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 (Sep 22 2020 at 16:09):

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

Oh great!

#### Logan Murphy (Sep 22 2020 at 19:14):

@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 (Sep 22 2020 at 19:16):

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

#### Logan Murphy (Sep 22 2020 at 19:33):

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 (Sep 22 2020 at 19:35):

oh, maybe I can just provide an argument to tactic_even

#### Simon Hudon (Sep 22 2020 at 19:48):

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 (Sep 22 2020 at 19:50):

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!

Last updated: May 09 2021 at 21:10 UTC