Stream: Coq users

Topic: Counting number of certain branches executed in Ltac

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.

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

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.

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

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: Oct 13 2024 at 01:02 UTC