mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
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.
28 lines
1.5 KiB
Plaintext
28 lines
1.5 KiB
Plaintext
sanitychecks.lean:1:8-1:15: error: fail to show termination for
|
|
unsound
|
|
with errors
|
|
failed to infer structural recursion:
|
|
no parameters suitable for structural recursion
|
|
|
|
well-founded recursion cannot be used, `unsound` does not take any (non-fixed) arguments
|
|
sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
|
|
sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
|
|
sanitychecks.lean:10:0-10:23: error: failed to synthesize 'Inhabited' or 'Nonempty' instance for
|
|
False
|
|
|
|
If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
|
|
sanitychecks.lean:18:12-18:20: error: invalid use of `partial`, `Foo.unsound3` is not a function
|
|
False
|
|
sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition `Foo.unsound4`, could not prove that the type
|
|
∀ (x : Unit), False
|
|
is nonempty.
|
|
|
|
This process uses multiple strategies:
|
|
- It looks for a parameter that matches the return type.
|
|
- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
|
|
- It tries unfolding the return type.
|
|
|
|
If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
|
|
sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
|
|
sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
|