Comment by daxfohl

I guess it makes sense: the tactics are defined in the lean repo (but not in the kernel of that repo), while mathlib has its own repo. But any changes to tactic code triggers a test to verify that mathlib still works against it. Which implies there's a reasonable set of checks and balances that don't allow tactic changes to break anything too badly if you follow mathlib's idioms, though it can still happen.