Performance of simp vs simp only

Stream: general

[Moritz Doll]

What is the difference in performance between simp and simp only [..]? I would guess that the later is way faster and I wonder why simp is allowed in mathlib at all.

[Kevin Buzzard]

Sometimes simp is really fast so there's no point changing

[Alex J. Best]

simp is also more robust when used as a finishing tactic. If a lemma is renamed or a namespace not opened somewhere else in the file a simp only call might need fixing, but a plain simp won't. Its debatable whether the extra compile time is worth it in all cases, but mathlib does place emphasis on trying to make proofs robust where it can.