08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
43 lines
1.2 KiB
Text
43 lines
1.2 KiB
Text
import Lean
|
|
/-!
|
|
# Attribute Errors
|
|
|
|
Tests errors generated by the core attribute infrastructure. Does *not* test errors generated by
|
|
attributes' individual preprocessing (e.g., `[reducible]`).
|
|
-/
|
|
|
|
/-- error: Unknown attribute `[nonexistent_attribute]` -/
|
|
#guard_msgs in
|
|
@[nonexistent_attribute] def x := 32
|
|
|
|
/--
|
|
error: Cannot add attribute `[unused_variables_ignore_fn]`: Declaration `notAnIgnoreFn` has type
|
|
Bool
|
|
but `[unused_variables_ignore_fn]` can only be added to declarations of type
|
|
Lean.Linter.IgnoreFunction
|
|
-/
|
|
#guard_msgs in
|
|
@[unused_variables_ignore_fn] def notAnIgnoreFn := true
|
|
|
|
/--
|
|
error: Cannot add attribute `[expose]`: This attribute can only be added when declaring a `def`
|
|
-/
|
|
#guard_msgs in
|
|
@[expose] theorem t : True := trivial
|
|
|
|
def foo := ()
|
|
/--
|
|
error: Cannot add attribute `[expose]`: This attribute can only be added when declaring a `def`
|
|
-/
|
|
#guard_msgs in
|
|
attribute [expose] foo
|
|
|
|
/-- error: Attribute `[expose]` cannot be erased -/
|
|
#guard_msgs in
|
|
attribute [-expose] Nat.add
|
|
|
|
/--
|
|
error: Cannot add attribute `[missing_docs_handler]` to declaration `Nat.succ` because it is in an imported module
|
|
-/
|
|
#guard_msgs in
|
|
attribute [missing_docs_handler] Nat.succ
|