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.
111 lines
3.0 KiB
Plaintext
111 lines
3.0 KiB
Plaintext
Inferred termination measure:
|
|
termination_by n - i
|
|
Inferred termination measure:
|
|
termination_by xs.size - i
|
|
Inferred termination measure:
|
|
termination_by xs.size - i
|
|
Inferred termination measure:
|
|
termination_by (xs.size - i, ys.size - j)
|
|
Inferred termination measure:
|
|
termination_by (xs.size - i, i - j)
|
|
Inferred termination measure:
|
|
termination_by (xs.size - i, i)
|
|
guessLexDiff.lean:84:4-84:11: error: fail to show termination for
|
|
failure
|
|
with errors
|
|
failed to infer structural recursion:
|
|
Not considering parameter xs of failure:
|
|
it is unchanged in the recursive calls
|
|
Cannot use parameter i:
|
|
failed to eliminate recursive application
|
|
_root_.failure xs i
|
|
|
|
|
|
Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
i #1 #2 i + 1 0 - i #3 i + i
|
|
1) 85:26-38 = = = = = = =
|
|
2) 85:58-76 ? < _ _ _ _ _
|
|
3) 85:26-38 = = = = = = =
|
|
4) 88:26-42 _ < _ _ _ _ _
|
|
5) 88:26-42 ? ≤ ≤ ? ≤ ≤ ?
|
|
6) 88:26-42 _ < _ _ _ _ _
|
|
7) 88:26-42 _ < _ _ _ _ _
|
|
8) 88:26-42 _ < _ _ _ _ _
|
|
9) 97:8-20 _ < _ _ _ _ _
|
|
|
|
#1: xs.size - i
|
|
#2: xs.size - (i + 1)
|
|
#3: 42 - i
|
|
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
guessLexDiff.lean:102:4-102:18: error: fail to show termination for
|
|
mutual_failure
|
|
mutual_failure2
|
|
with errors
|
|
failed to infer structural recursion:
|
|
Not considering parameter xs of mutual_failure:
|
|
it is unchanged in the recursive calls
|
|
Not considering parameter xs of mutual_failure2:
|
|
it is unchanged in the recursive calls
|
|
Cannot use parameters i of mutual_failure and i of mutual_failure2:
|
|
failed to eliminate recursive application
|
|
mutual_failure2 xs i
|
|
|
|
|
|
Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
Call from mutual_failure to mutual_failure2 at 104:4-24:
|
|
i #1 #2 i + 1
|
|
i = ? ? <
|
|
#3 ? = ? ?
|
|
Call from mutual_failure to mutual_failure2 at 104:52-78:
|
|
i #1 #2 i + 1
|
|
i ? _ _ =
|
|
#3 _ < _ _
|
|
Call from mutual_failure to mutual_failure2 at 104:4-24:
|
|
i #1 #2 i + 1
|
|
i _ _ _ <
|
|
#3 _ = _ _
|
|
Call from mutual_failure to mutual_failure2 at 111:4-28:
|
|
i #1 #2 i + 1
|
|
i _ _ _ =
|
|
#3 _ < _ _
|
|
Call from mutual_failure to mutual_failure2 at 117:8-28:
|
|
i #1 #2 i + 1
|
|
i _ _ _ <
|
|
#3 _ ? _ _
|
|
Call from mutual_failure2 to mutual_failure at 123:4-23:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 ? _
|
|
Call from mutual_failure2 to mutual_failure at 123:50-75:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 _ _
|
|
Call from mutual_failure2 to mutual_failure at 127:4-27:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 _ _
|
|
Call from mutual_failure2 to mutual_failure at 133:8-27:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 _ _
|
|
|
|
|
|
#1: xs.size - i
|
|
#2: xs.size - (i + 1)
|
|
#3: xs.size - i
|
|
|
|
Please use `termination_by` to specify a decreasing measure.
|