error message of `register_label_attr`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

register_label_attr has the following behavior.

import Lean.LabelAttribute

register_label_attr rom

/-- error: unknown attribute [rom] -/
#guard_msgs in @[rom]
def womp : 2 + 2 = 4 := by rfl

Expected behavior: The possible solution is displayed in the error message. An error message appears saying, “Since it is not possible to register and use labels in the same file, please consider separating the files." (this message is a example)

Actual behavior: It simply displays “unknown attribute” and does not show possible solutions.

Versions

• Lean v4.7.0

Additional Information

see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20register_labell_attr.20not.20working

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal example with import Lean.LabelAttribute and register_label_attr rom to reproduce the diagnostic. Trace the implementation of register_label_attr and the unknown-attribute error, then make the failure explain that labels cannot be registered and used in the same file. Done means the example reports a useful suggested solution instead of only “unknown attribute”.