diff --git a/src/tests/VersoTests/BlockParseErrors.lean b/src/tests/VersoTests/BlockParseErrors.lean new file mode 100644 index 000000000..348238d92 --- /dev/null +++ b/src/tests/VersoTests/BlockParseErrors.lean @@ -0,0 +1,205 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Errata +import Verso + +/-! +These tests check where Verso's block parsers report parse errors and ensure that a `>` begins a +blockquote precisely when it's in a block-opening position (and not in the middle of text). + +When a block parser encounters an error after its opening marker, it fails at the error. Error +recovery must resume from this position, without rewinding. This is how Verso's top-level blocks +maintain the Lean command-parsing loop's invariant that each command's syntax, end position, and +parse errors depend on at most two more commands. + +Each case runs a block parser on a small input with `ParserFn.test!`. The output lists each error +with its byte offset, its line and column, and the rest of the input from there. Then it shows the +final syntax stack. A recovered error is listed at the position where recovery stopped. +-/ + +namespace Verso.BlockParseErrorsTest +open Verso.Parser +open Lean.Parser + +/-! # Error tests -/ + +/- +This case checks that a directive fails at an error in its contents. The directive's third paragraph +is the unfinished role `{hig`. The role's error is at the end of its line (6:4). The directive fails +at the end of input (8:0), because the unclosed role reads past the closing `:::`. +-/ +/-- +info: 2 failures: + @56 (⟨6, 4⟩): unexpected ' +'; expected positional argument, named argument, flag, or '}' (use '\{' for a literal '{') + "\n:::\n" + @61 (⟨8, 0⟩): unexpected end of input; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{' + "" + +Final stack: + (Lean.Doc.Syntax.directive + ":::" + `note + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"The weather was nice.\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"We went for a walk.\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.role + "{" + `hig + [] + + "[" + [(Lean.Doc.Syntax.footnote )] + "]")])]) +-/ +#test_msgs in +#eval (block {}).test! ":::note\nThe weather was nice.\n\nWe went for a walk.\n\n{hig\n:::\n" + +/- +This case checks that a code block fails at an error in its contents. The code block has no closing +fence, so it reads to the end of input and fails there (5:0). +-/ +/-- +info: Failure @47 (⟨5, 0⟩): unexpected end of input +Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [] + "\n" + (str + "\"The weather was nice.\\n\\nWe went for a walk.\\n\"") + ) +Remaining: "" +-/ +#test_msgs in +#eval (block {}).test! "```\nThe weather was nice.\n\nWe went for a walk.\n" + +/-! # Blockquote placement tests -/ + +/- +A blockquote with two paragraphs, followed by a paragraph, parses with no errors. +-/ +/-- +info: Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"The weather was nice.\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"We went for a walk.\""))] + "}")]) + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"We came home.\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")] +All input consumed. +-/ +#test_msgs in +#eval (document).test! "> The weather was nice.\n\n We went for a walk.\n\nWe came home.\n" + +/- +A `>` alone on its line is an empty blockquote. +-/ +/-- +info: Success! Final stack: + [(Lean.Doc.Syntax.blockquote ">" []) + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"We came home.\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")] +All input consumed. +-/ +#test_msgs in +#eval (document).test! ">\n\nWe came home.\n" + +/- +A `>` in the middle of a line is text, not a blockquote. +-/ +/-- +info: Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Also, 2 > 3.\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")] +All input consumed. +-/ +#test_msgs in +#eval (document).test! "Also, 2 > 3.\n" + +/- +A `>` that is indented less than a list item's contents ends the list and begins a blockquote. The +`>` is at column 0, and the item's contents are at column 2. +-/ +/-- +info: Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"The weather was nice.\""))] + "}")])] + "}") + (Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"We went for a walk.\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] +All input consumed. +-/ +#test_msgs in +#eval (document).test! "* The weather was nice.\n\n> We went for a walk.\n" + +/- +A `>` that is indented less than the required column is not a blockquote. Here blocks must start at +column 2, and the `>` is at column 0. The parser fails at 1:0 and consumes no input, because the +error comes before the opening marker. This lets an enclosing block end at that line. +-/ +/-- +info: Failure @0 (⟨1, 0⟩): unexpected block opener; expected %%% (at line beginning) or expected column at least 2 +Final stack: + (Lean.Doc.Syntax.metadata_block + + ) +Remaining: "> The weather was nice.\n" +-/ +#test_msgs in +#eval (block { minIndent := 2 }).test! "> The weather was nice.\n" diff --git a/src/tests/VersoTests/IncrementalParsing.lean b/src/tests/VersoTests/IncrementalParsing.lean new file mode 100644 index 000000000..8a1484b7c --- /dev/null +++ b/src/tests/VersoTests/IncrementalParsing.lean @@ -0,0 +1,387 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +import Errata +import Lean.Parser +import Verso.Parser +import Verso.SyntaxUtils + +/-! +These tests check that Verso's top-level block commands satisfy an _incremental parsing invariant_ +on documents with parse errors. When the invariant is not satisfied, the editor shows stale errors, +folds and symbols. + +The incremental parsing invariant says that the parse of a top-level block command doesn't depend on +any text that follows the end of the command after next. Lean's command loop relies on it. After an +edit, Lean reuses a command without parsing it again if the command after next ends before the first +changed byte. Verso parses each top-level block of a `#doc` document as one command. When a block +fails to parse, error recovery makes it a command anyway. For Verso, the takeaway is that a +recovered command must end at or after all the text that its parser read. + +Each test splits a document into commands as `versoBlockCommandFn` does, with Verso's error +recovery. Then it checks each command that has a command after next. At each line start after the +end of the command after next, it changes the text in each of the ways listed in `changes`. It +parses the command again from its start. The syntax, the end position and the errors must match the +first parse. + +The documents are small. Each has a parse error in one block, followed by more paragraphs. In most +of them, the error is the unfinished role `{hig`. The interactive test +`parse_errors_blockquote_in_directive.lean` checks one of these documents through the language +server. +-/ + +namespace Verso.IncrementalParsingTest + +open Lean Parser Verso.Parser Errata + +/-- +Parses one top-level block command at the current position. This is a copy of the recovery step of +`versoBlockCommandFn` in `Verso.Doc.Concrete`, which is private. It leaves out the update of the +trailing whitespace and the saved end position. When that recovery step changes, this copy must +change with it. +-/ +def cmdFn : ParserFn := fun c s => + let s := recoverBlockWith #[.missing] (block {}) c s + if s.hasError then s else ignoreFn (manyFn blankLine) c s + +/-- The result of parsing one command: its syntax, its end position and its errors. -/ +structure Parsed where + stx : String + endPos : Nat + errors : List (Nat × String) + failed : Bool +deriving BEq, Repr + +/-- Parses the command that starts at byte `pos` of `input`. -/ +def parseAt (input : String) (pos : Nat) : IO Parsed := do + let env ← mkEmptyEnvironment + let ictx := mkInputContext input "" + let pmctx : ParserModuleContext := { env, options := {} } + let s := cmdFn.run ictx pmctx (getTokenTable env) ((mkParserState input).setPos ⟨pos⟩) + let stx := if s.stxStack.size > 0 then toString s.stxStack.back else "" + let errors := s.allErrors.toList.map fun (p, _, e) => (p.byteIdx, toString e) + return { stx, endPos := s.pos.byteIdx, errors, failed := s.hasError } + +/-- Splits a document into top-level block commands, returning each start position and result. -/ +def commands (input : String) : IO (Array (Nat × Parsed)) := do + let env ← mkEmptyEnvironment + let ictx := mkInputContext input "" + let pmctx : ParserModuleContext := { env, options := {} } + let s := (ignoreFn (manyFn blankLine)).run ictx pmctx (getTokenTable env) (mkParserState input) + let mut pos := s.pos.byteIdx + let mut out := #[] + for _ in [0:input.utf8ByteSize] do + if pos ≥ input.utf8ByteSize then break + let r ← parseAt input pos + out := out.push (pos, r) + if r.failed || r.endPos ≤ pos then break + pos := r.endPos + return out + +/-- +The ways the text is changed after a cut point: it is cut off there, or text is added at the cut +point. The additions close or open inline markup and blocks, change indentation, and add lines. +-/ +def changes (input : String) (cut : Nat) : List String := + let pre := String.Pos.Raw.extract input 0 ⟨cut⟩ + let rest := String.Pos.Raw.extract input ⟨cut⟩ input.rawEndPos + [pre, pre ++ "]\n", pre ++ "[x]\n", pre ++ "}\n", pre ++ "x\n\ny\n", pre ++ "> q\n", + pre ++ "[" ++ rest, pre ++ "]" ++ rest, pre ++ "}" ++ rest, pre ++ "{" ++ rest, + pre ++ ":::\n" ++ rest, pre ++ "*" ++ rest, pre ++ "```\n" ++ rest, pre ++ " " ++ rest, + pre ++ "\n" ++ rest, pre ++ "x" ++ rest] + +/-- The byte positions where lines of `input` start. -/ +def lineStarts (input : String) : List Nat := Id.run do + let mut acc := 0 + let mut out := [] + for l in input.splitOn "\n" do + out := acc :: out + acc := acc + l.utf8ByteSize + 1 + return out.reverse.filter (· ≤ input.utf8ByteSize) + +/-- +Finds the commands whose parse changes when text after the end of the command after next changes. +Each result describes the command, the cut point and the changed text. +-/ +def violations (input : String) : IO (Array String) := do + let cmds ← commands input + let mut out := #[] + for h : j in [0:cmds.size] do + let some (_, after) := cmds[j + 2]? | continue + let (start, parsed) := cmds[j] + let mut found := false + for cut in lineStarts input do + if found then break + if cut < after.endPos then continue + for changed in changes input cut do + let parsed' ← parseAt changed start + if parsed' != parsed then + let suffix := String.Pos.Raw.extract changed ⟨cut⟩ changed.rawEndPos + out := out.push s!"command {j} at byte {start} ends at {parsed.endPos}, and the command \ + after next ends at {after.endPos}. Changing the text at byte {cut} to {repr suffix} \ + changes its parse to end at {parsed'.endPos} with errors at \ + {parsed'.errors.map (·.1)}, where it had errors at {parsed.errors.map (·.1)}." + found := true + break + return out + +/-- Asserts that `input` satisfies the incremental parsing invariant. -/ +def checkInvariant (input : String) : Test := do + let cmds ← commands input + assertTrue (cmds.size ≥ 3) "the document splits into at least three commands" + (detail? := some s!"{cmds.size} commands") + let found ← violations input + assertTrue found.isEmpty "a command's parse depends on text after the command after next" + (detail? := some ("\n".intercalate found.toList)) + +/-- +A blockquote whose fourth paragraph is the unfinished role `{hig`. This is the basic case. In prior +versions of the blockquote parser, this document broke the invariant. The blockquote failed at its +`>`, so its recovered command ended after its first paragraph. Its parser had read up to the error, +which is after the command after next. +-/ +def blockquote3 : String := +"> The weather was nice today. + + We went for a walk. + + The park was quiet. + + {hig + +Then we went home. + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. +" + +@[test] def blockquoteThreeParagraphs : Test := checkInvariant blockquote3 + +/-- +A blockquote with five paragraphs before the unfinished role. In prior versions of the blockquote +parser, this document broke the invariant. +-/ +def blockquote5 : String := +"> The weather was nice today. + + We went for a walk. + + The park was quiet. + + We sat on a bench. + + Then we went home. + + {hig + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. + +We went to the beach. +" + +@[test] def blockquoteFiveParagraphs : Test := checkInvariant blockquote5 + +/-- +A `:::note` directive whose first block is a blockquote with the unfinished role. In prior versions +of the blockquote parser, this document broke the invariant. Both the directive's command and the +command after it ended before the error. +-/ +def blockquoteInDirective : String := +":::note +> The weather was nice today. + + We went for a walk. + + The park was quiet. + + {hig +::: + +Then we went home. + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. +" + +@[test] def blockquoteInsideDirective : Test := checkInvariant blockquoteInDirective + +/-- +A blockquote that contains a code block whose closing fence is too short. The code block recovers +from its error, so the blockquote succeeds. This document satisfied the invariant in prior versions +of the blockquote parser too. +-/ +def codeInBlockquote : String := +"> The weather was nice today. + + We went for a walk. + + The park was quiet. + + ``` + Thanks + `` + +Then we went home. + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. +" + +@[test] def codeBlockInsideBlockquote : Test := checkInvariant codeInBlockquote + +/-- +A list item that contains a blockquote with the unfinished role. In prior versions of the +blockquote parser, this document broke the invariant. The list item ended at the blockquote. +-/ +def blockquoteInList : String := +"* The weather was nice today. + + > We went for a walk. + + The park was quiet. + + We sat on a bench. + + {hig + +Then we went home. + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. +" + +@[test] def blockquoteInsideListItem : Test := checkInvariant blockquoteInList + +/-- +A blockquote that contains a list whose item is the unfinished role. In prior versions of the +blockquote parser, this document broke the invariant. The blockquote failed at its `>`, before the +list. +-/ +def listInBlockquote : String := +"> The weather was nice today. + + We went for a walk. + + The park was quiet. + + * {hig + +Then we went home. + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. +" + +@[test] def listInsideBlockquote : Test := checkInvariant listInBlockquote + +/-- +A list item whose fourth paragraph is the unfinished role, with no blockquote. This document +satisfied the invariant in prior versions of the blockquote parser too, because a list fails at its +error. +-/ +def listItem : String := +"* The weather was nice today. + + We went for a walk. + + The park was quiet. + + {hig + +Then we went home. + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. +" + +@[test] def listItemWithError : Test := checkInvariant listItem + +/-- +A `:::note` directive whose fourth paragraph is the unfinished role, with no blockquote. This +document satisfied the invariant in prior versions of the blockquote parser too, because a directive +fails at its error. +-/ +def directive : String := +":::note +The weather was nice today. + +We went for a walk. + +The park was quiet. + +{hig +::: + +Then we went home. + +We had dinner. + +We went to bed. + +We slept well. + +The next day was sunny. +" + +@[test] def directiveWithError : Test := checkInvariant directive + +/-- +Three paragraphs and then a code block whose closing fence is too short. The code block recovers +from its error. This document satisfied the invariant in prior versions of the blockquote parser +too. The code block runs to the end of the text, so only the three paragraphs before it have a +command after next, and only they are checked. +-/ +def codeBlock : String := +"The weather was nice today. + +We went for a walk. + +The park was quiet. + +``` +Thanks +`` + +Then we went home. +" + +@[test] def codeBlockWithBrokenFence : Test := checkInvariant codeBlock diff --git a/src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean b/src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean new file mode 100644 index 000000000..4932daff0 --- /dev/null +++ b/src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean @@ -0,0 +1,80 @@ +import Verso + +/-! +This test checks, through the language server, that fixing a parse error in a blockquote inside a +directive clears the error and restores the document's folds and symbols. It matters when you change +a block parser or its error recovery. `VersoTests.IncrementalParsing` checks more documents of this +kind without the language server. `VersoTests.BlockParseErrors` checks where the errors are +reported. + +The document has a `:::note` directive whose first block is a blockquote. The edits replace the +blockquote's fourth paragraph, `Thanks`, with `{highlight}[Thanks]` in five steps. While the role is +unfinished, the blockquote and the directive have a parse error. The runner waits for the server +after each edit. After the last edit, it prints the diagnostics, the folding ranges and the document +symbols. + +The final text is valid, so the expected output is the same as for a fresh elaboration. It has no +diagnostics. It has folds for the document, the header, the directive and the blockquote. It has the +document symbol `Notes` with its header `Weekend`. A stale error, a missing fold or a missing symbol +would mean that Lean reused a command after text that its parse depends on had changed. Lean reuses +commands correctly when Verso's block commands maintain the incremental parsing invariant, which +`VersoTests.IncrementalParsing` defines. + +In prior versions of the blockquote parser, this test failed. On an error, the blockquote failed at +its `>`. Error recovery started there and stopped at the first blank line, before the error. The +output had stale errors (`expected closing ':::'`, `unexpected block opener` and the role error). +The folds for the document, the header, the directive and the blockquote were missing, and so was +the document symbol `Notes`. +-/ + +open Lean Verso Doc Elab + +/-- A genre with no extensions of its own. -/ +def TestGenre : Genre where + PartMetadata := Unit + Block := Empty + Inline := Empty + TraverseContext := Unit + TraverseState := Unit + +/-- Emphasizes its contents. -/ +@[role] +def highlight : RoleExpanderOf Unit + | (), contents => do + let contents ← contents.mapM elabInline + ``(Verso.Doc.Inline.emph #[$contents,*]) + +/-- Groups its blocks. -/ +@[directive] +def note : DirectiveExpanderOf Unit + | (), blocks => do + let blocks ← blocks.mapM elabBlock + ``(Verso.Doc.Block.concat #[$blocks,*]) + +#doc (TestGenre) "Notes" => + +# Weekend + +:::note +> The weather was nice today. + + We went for a walk. + + The park was quiet. + + Thanks + --⬑ delete: "Thanks" + --⬑ sync + --⬑ insert: "\x7bhig" + --⬑ sync + --⬑ insert: "hli" + --⬑ sync + --⬑ insert: "ght" + --⬑ sync + --⬑ insert: "\x7d\x5bTh" + --⬑ sync + --⬑ insert: "anks\x5d" + --⬑ collectDiagnostics + --⬑ textDocument/foldingRange + --⬑ textDocument/documentSymbol +::: diff --git a/src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean.expected.out b/src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean.expected.out new file mode 100644 index 000000000..88dc74b7d --- /dev/null +++ b/src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean.expected.out @@ -0,0 +1,56 @@ +{"version": 7, + "uri": + "file:///src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean", + "isIncremental": false, + "diagnostics": []} +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean"}, + "position": {"line": 64, "character": 2}} +[{"startLine": 53, "endLine": 79}, + {"startLine": 55, "endLine": 79}, + {"startLine": 58, "endLine": 78}, + {"startLine": 57, "endLine": 79}, + {"startLine": 2, "kind": "comment", "endLine": 27}, + {"startLine": 32, "kind": "region", "endLine": 37}, + {"startLine": 41, "kind": "region", "endLine": 44}, + {"startLine": 48, "kind": "region", "endLine": 51}, + {"startLine": 57, "kind": "region", "endLine": 79}] +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/parse_errors_blockquote_in_directive.lean"}, + "position": {"line": 64, "character": 2}} +[{"selectionRange": + {"start": {"line": 32, "character": 4}, "end": {"line": 32, "character": 13}}, + "range": + {"start": {"line": 31, "character": 0}, "end": {"line": 37, "character": 23}}, + "name": "TestGenre", + "kind": 6}, + {"selectionRange": + {"start": {"line": 41, "character": 4}, "end": {"line": 41, "character": 13}}, + "range": + {"start": {"line": 39, "character": 0}, "end": {"line": 44, "character": 44}}, + "name": "highlight", + "kind": 6}, + {"selectionRange": + {"start": {"line": 48, "character": 4}, "end": {"line": 48, "character": 8}}, + "range": + {"start": {"line": 46, "character": 0}, "end": {"line": 51, "character": 43}}, + "name": "note", + "kind": 6}, + {"selectionRange": + {"start": {"line": 53, "character": 17}, + "end": {"line": 53, "character": 24}}, + "range": + {"start": {"line": 53, "character": 0}, "end": {"line": 80, "character": 0}}, + "name": "Notes", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 55, "character": 0}, + "end": {"line": 55, "character": 9}}, + "range": + {"start": {"line": 55, "character": 0}, + "end": {"line": 80, "character": 0}}, + "name": "Weekend", + "kind": 15}]}] diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean index 24f76e81e..db1b46e50 100644 --- a/src/verso/Verso/Parser.lean +++ b/src/verso/Verso/Parser.lean @@ -785,8 +785,8 @@ mutual asStringFn (chFn ':' false) >> ignoreFn (lookaheadFn (chFn ' ')) partial def blockquote (ctxt : BlockCtxt) : ParserFn := - atomicFn <| nodeFn ``blockquote <| - takeWhileFn (· == ' ') >> guardMinColumn ctxt.minIndent >> chFn '>' >> + nodeFn ``blockquote <| + atomicFn (takeWhileFn (· == ' ') >> guardMinColumn ctxt.minIndent >> chFn '>') >> withCurrentColumn fun c => blocks { ctxt with minIndent := c } partial def unorderedList (ctxt : BlockCtxt) : ParserFn :=