Choose fastest tactic

Stream: new members

[Martin Dvořák]

How do I choose the fastest tactic when hint shows me the following output?

the following tactics solve the goal:
----
Try this: omega
Try this: nlinarith
Try this: linarith
Try this: ring
Try this: finish

[Patrick Massot]

omega and finish should be slow. nlinarith strictly contains linarith

[Patrick Massot]

ring and linarith are probably comparable

[Martin Dvořák]

Can I see it from the output? Is it ordered with respect to the number of steps each tactic had to execute? Or how can I display this information?

[Patrick Massot]

You can't.

[Martin Dvořák]

Not even by editing the code? If I want to benchmark before choosing...

[Yaël Dillies]

You can always look at the times with the profiler. set_option profiler true.

[Martin Dvořák]

Can I display its result for a specific line of code? I'm looking at the output and I'm feeling dumb.