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.
30 lines
805 B
Text
30 lines
805 B
Text
/-!
|
|
# Test for improved error message when `initialize` fails due to missing `Nonempty` instance
|
|
|
|
See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/initialize.20structure.20with.20IO.2ERef/near/564920245
|
|
-/
|
|
|
|
structure Foo where
|
|
ref : IO.Ref Nat
|
|
|
|
def mkFoo : IO Foo := do
|
|
let ref ← IO.mkRef 0
|
|
return { ref }
|
|
|
|
/-- error: failed to synthesize 'Inhabited' or 'Nonempty' instance for
|
|
Foo
|
|
|
|
If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it. -/
|
|
#guard_msgs in
|
|
initialize _foo : Foo ← mkFoo
|
|
|
|
-- The fix: adding `deriving Nonempty` makes it work
|
|
structure Bar where
|
|
ref : IO.Ref Nat
|
|
deriving Nonempty
|
|
|
|
def mkBar : IO Bar := do
|
|
let ref ← IO.mkRef 0
|
|
return { ref }
|
|
|
|
initialize _bar : Bar ← mkBar
|