Stream: Coq users

Topic: Counting number of certain branches executed in Ltac


view this post on Zulip YoungJu Song (Oct 30 2022 at 13:15):

Hi all,
I have an Ltac tactic, and I would like to count how many times a certain branch of such a tactic is executed during the whole proof. (The tactics is used multiple times during the proof)
Since Ltac is statetless, I don't see an easy way to get this. Maybe Ltac2 might help? (but not sure if I can mix Ltac1 and Ltac2) Maybe there is some OCaml plugin for this? Any advice would be appreciated.

view this post on Zulip Gaëtan Gilbert (Oct 30 2022 at 13:17):

you can put idtac "HELLO" in the branch and count how many times it gets printed

view this post on Zulip YoungJu Song (Oct 30 2022 at 13:22):

@Gaëtan Gilbert Thanks for the input, Gaetan! I agree that would work in many cases, but in my case the tactic is used a lot of time during the proof, and it wouldn't be feasible for me to manually collect the idtac outputs each time I execute the tactic.

view this post on Zulip Gaëtan Gilbert (Oct 30 2022 at 13:33):

do you need to do the measurement interactively? otherwise you can do something like coqc bla.v | grep HELLO | wc

view this post on Zulip YoungJu Song (Oct 30 2022 at 13:37):

@Gaëtan Gilbert No, I don't need to do it interactively. I didn't realize that idtac also prints in stdout. That I think could work. Thanks for the advice!!


Last updated: Mar 28 2024 at 17:01 UTC