ban omega?

Stream: general

[Floris van Doorn]

Should we ban docs#tactic.interactive.omega in mathlib to make porting to Lean 4 easier? If we ban omega, we can port mathlib more easily to Lean 4 (we don't need to port omega before porting the library). We could still write omega in Lean 4 after the initial port.
Related PR: #7646

[Julian Berman]

This is a basic question I'm sure but what makes omega particularly ban-desirable over other finishing tactics? Its implementation is particularly non-trivial?

[Scott Morrison]

It's implementation is complicated, and was done by someone who hasn't been active in mathlib since they contributed it, and we've treated it as a black box ever since.