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.
45 lines
1 KiB
Text
45 lines
1 KiB
Text
/-!
|
|
# More helpful ranges of parser error messages on unexpected tokens
|
|
|
|
When the parser hits an unexpected token, it will now include all preceding
|
|
whitespace in the error message range as the expected token could be inserted
|
|
at any of these places to fix the error. -/
|
|
|
|
/-!
|
|
In the following example, we want the parser error to start right after
|
|
`exact` as the error belongs to this declaration, not the next one, and
|
|
otherwise would be too easy to overlook. -/
|
|
|
|
theorem lem1 : True := by
|
|
exact
|
|
|
|
theorem lem2 : True := ⟨⟩
|
|
|
|
/-!
|
|
Outside of tactics as well it is generally a better idea to place the error
|
|
right after the last correct token. -/
|
|
|
|
def f1
|
|
|
|
def f2 := 0
|
|
|
|
/-!
|
|
We do not currently special-case linebreaks in this; on a single line,
|
|
the shift is usually not very noticeable nor clearly worse than before. -/
|
|
|
|
def f3 := def f4 := 0
|
|
|
|
/-! Test other expected token errors as well -/
|
|
|
|
inductive
|
|
|
|
example := 0
|
|
|
|
-- merge of token errors
|
|
set_option pp.all
|
|
|
|
example := 0
|
|
|
|
/-! Do not shift other kinds of errors. -/
|
|
|
|
example := "a
|