Skip to content

doc: improve error message for unknown attributes #14213

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
0rca wants to merge 1 commit into
base: master
Choose a base branch
from
+5 −5
Open

doc: improve error message for unknown attributes #14213

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/Lean/Elab/Attributes.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,9 +59,9 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
else match attr.getKind with
| .str _ s => pure <| Name.mkSimple s
| _ => throwErrorAt attr "Unknown attribute"
let .ok _impl := getAttributeImpl (← getEnv) attrName
| throwError "Unknown attribute `[{attrName}]`"
if let .ok impl := getAttributeImpl (← getEnv) attrName then
match getAttributeImpl (← getEnv) attrName with
| .error _ => throwError "Unknown attribute `[{attrName}]`. Note, that attributes are impossible to use in the same file they are declared in: consider extracting the declaration into a separate file."
| .ok impl =>
if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then -- skip `builtin_initialize` attributes
-- Reject attribute uses where the implementation's module has been loaded for IR only as
-- this would make it `inServer`-dependent and confused shake as well (#13599).
Expand Down
2 changes: 1 addition & 1 deletion tests/elab/attributeErrors.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Tests errors generated by the core attribute infrastructure. Does *not* test err
attributes' individual preprocessing (e.g., `[reducible]`).
-/

/-- error: Unknown attribute `[nonexistent_attribute]` -/
/-- error: Unknown attribute `[nonexistent_attribute]`. Note, that attributes are impossible to use in the same file they are declared in: consider extracting the declaration into a separate file. -/
#guard_msgs in
@[nonexistent_attribute] def x := 32

Expand Down
2 changes: 1 addition & 1 deletion tests/elab_fail/nonfatalattrs.lean.out.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
nonfatalattrs.lean:6:2-6:19: error: Unknown attribute `[attrUnimplementedattr]`
nonfatalattrs.lean:6:2-6:19: error: Unknown attribute `[attrUnimplementedattr]`. Note, that attributes are impossible to use in the same file they are declared in: consider extracting the declaration into a separate file.
foo : Nat
nonfatalattrs.lean:11:12-11:17: error: invalid 'class', declaration 'bar.bar' must be inductive datatype, structure, or constant
bar : Nat
Loading