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.
you can put
idtac "HELLO" in the branch and count how many times it gets printed
@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.
do you need to do the measurement interactively? otherwise you can do something like
coqc bla.v | grep HELLO | wc
@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 01 2023 at 19:01 UTC