leanprover/lean4

error message of `register_label_attr`

Opened this issue · 1 comments

Seasawher commented

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.

semorrison commented

If someone would like to make a PR improving the error message that would be great.