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.
210 lines
4.1 KiB
Lean4
210 lines
4.1 KiB
Lean4
import Lean
|
|
|
|
set_option doc.verso true
|
|
|
|
/-!
|
|
This test ensures that syntax errors in Verso docs are appropriately reported.
|
|
-/
|
|
|
|
-- Syntax error in module docstring should report actual error location
|
|
/--
|
|
@ +2:40...*
|
|
error: unexpected '`'; expected positional argument, named argument, flag, or '}' (use '\{' for a literal '{')
|
|
---
|
|
@ +3:0...*
|
|
error: unexpected end of input; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
Here is text with an unclosed role {name`Nat
|
|
-/
|
|
|
|
-- Syntax error with specific position (not at end of docstring)
|
|
/--
|
|
@ +2:27...*
|
|
error: '*'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
Some mismatched *formatting_
|
|
|
|
A b c d e f.
|
|
|
|
```
|
|
-/
|
|
|
|
-- Syntax error in a normal docstring
|
|
/--
|
|
@ +2:27...*
|
|
error: '*'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/--
|
|
Some mismatched *formatting_
|
|
|
|
A b c d e f.
|
|
-/
|
|
def x := 5
|
|
|
|
-- Issue #12063: bare curly brace should suggest escaping
|
|
/--
|
|
@ +2:8...*
|
|
error: unexpected '='; expected positional argument, named argument, flag, or '}' (use '\{' for a literal '{')
|
|
---
|
|
@ +3:0...*
|
|
error: unexpected end of input; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
{module =checked}
|
|
-/
|
|
|
|
|
|
/--
|
|
@ +2:7...*
|
|
error: unexpected '='; expected positional argument, named argument, flag, or newline
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
```foo =thing
|
|
```
|
|
-/
|
|
|
|
/--
|
|
@ +2:5...*
|
|
error: unexpected '='; expected positional argument, named argument, flag, or '}' (use '\{' for a literal '{')
|
|
---
|
|
@ +3:0...*
|
|
error: unexpected end of input; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
{foo =thing}[]
|
|
-/
|
|
|
|
/--
|
|
@ +2:7...*
|
|
error: unexpected '='; expected positional argument, named argument, flag, or newline
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
:::foo =thing
|
|
:::
|
|
-/
|
|
|
|
|
|
-- Issue #12063: link target should suggest escaping
|
|
/--
|
|
@ +2:24...*
|
|
error: expected link target '(url)' or '[ref]' (use '\[' for a literal '[')
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
[`rigid` --> `flexible`]
|
|
-/
|
|
|
|
-- Escaped special characters should parse without errors
|
|
/-!
|
|
Use \{ and \} for literal braces.
|
|
Use \[ and \] for literal brackets.
|
|
Use \* and \_ for literal asterisks and underscores.
|
|
-/
|
|
|
|
|
|
/--
|
|
@ +2:25...*
|
|
error: expected URL
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
[`rigid` --> `flexible`](
|
|
-/
|
|
|
|
/--
|
|
@ +2:26...*
|
|
error: expected URL
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
[`rigid` --> `flexible`]()
|
|
-/
|
|
|
|
/--
|
|
@ +2:32...*
|
|
error: expected ')'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
[`rigid` --> `flexible`](http://
|
|
-/
|
|
|
|
|
|
/--
|
|
@ +2:25...*
|
|
error: expected reference name
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
[`rigid` --> `flexible`][
|
|
-/
|
|
|
|
/--
|
|
@ +2:26...*
|
|
error: expected reference name
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
[`rigid` --> `flexible`][]
|
|
-/
|
|
|
|
/--
|
|
@ +2:28...*
|
|
error: expected ']'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
[`rigid` --> `flexible`][xyz
|
|
-/
|
|
|
|
-- Unmatched closing bracket in docstring (issue #12118)
|
|
/--
|
|
@ +2:0...*
|
|
error: unexpected '}' (use '\}' to escape); expected '![', '$$', '$', '*', '[', '[^', '_', '`', '{', block opener (at line start: '#', '>', ':', '*', '-', '+', '1.', '```', '%%%', '{..}'), newline or text
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/--
|
|
}
|
|
-/
|
|
def z := 0
|
|
|
|
-- Unmatched closing bracket in module docstring
|
|
/--
|
|
@ +2:0...*
|
|
error: unexpected '}' (use '\}' to escape); expected '![', '$$', '$', '*', '[', '[^', '_', '`', '{', block opener (at line start: '#', '>', ':', '*', '-', '+', '1.', '```', '%%%', '{..}'), newline or text
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
}
|
|
-/
|
|
|
|
-- Unmatched closing square bracket in docstring
|
|
/--
|
|
@ +2:0...*
|
|
error: unexpected ']' (use '\]' to escape); expected '![', '$$', '$', '*', '[', '[^', '_', '`', '{', block opener (at line start: '#', '>', ':', '*', '-', '+', '1.', '```', '%%%', '{..}'), newline or text
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/--
|
|
]
|
|
-/
|
|
def w := 0
|
|
|
|
-- Unmatched closing square bracket in module docstring
|
|
/--
|
|
@ +2:0...*
|
|
error: unexpected ']' (use '\]' to escape); expected '![', '$$', '$', '*', '[', '[^', '_', '`', '{', block opener (at line start: '#', '>', ':', '*', '-', '+', '1.', '```', '%%%', '{..}'), newline or text
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
]
|
|
-/
|