Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Trace to stdout


view this post on Zulip 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?

view this post on Zulip Simon Hudon (Sep 22 2020 at 16:09):

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

view this post on Zulip Logan Murphy (Sep 22 2020 at 16:30):

Oh great!

view this post on Zulip 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

view this post on Zulip Simon Hudon (Sep 22 2020 at 19:16):

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

view this post on Zulip 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)

view this post on Zulip Logan Murphy (Sep 22 2020 at 19:35):

oh, maybe I can just provide an argument to tactic_even

view this post on Zulip 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

view this post on Zulip 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