From 64fbc77fca4205db3a3f196417a32e63d0a3de3c Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 29 Sep 2026 12:08:35 +0000
Subject: [PATCH 1/4] test: add additional tests for document part structure
 (#1009)

Previously, specific document elaboration structures were not
well-exercised by the test suite.

As I work on nested incrementality, this is the kind of thing that could
go very wrong. This PR adds tests that check various aspects of nesting
structures.

No-Changelog: this is an internal testing change, not a user-visible
one.
---
 src/tests/VersoTests/DocStructure.lean        | 384 ++++++++++++++++++
 src/tests/VersoTests/DocStructure/Genre.lean  |  75 ++++
 .../VersoTests/DocStructure/Included.lean     |  23 ++
 .../VersoTests/DocStructure/Includes.lean     |  41 ++
 .../VersoTests/DocStructure/Metadata.lean     |  50 +++
 .../VersoTests/DocStructure/Nesting.lean      |  63 +++
 .../DocStructure/Term/Includes.lean           |  41 ++
 .../DocStructure/Term/Metadata.lean           |  50 +++
 .../VersoTests/DocStructure/Term/Nesting.lean |  63 +++
 .../VersoTests/VersoManual/Markdown.lean      |  17 +
 .../doc-structure/expected/includes.txt       |  49 +++
 .../doc-structure/expected/metadata.txt       |  18 +
 .../doc-structure/expected/nesting.txt        |  39 ++
 .../test-cases/symbols_verso_nesting.lean     |  59 +++
 .../symbols_verso_nesting.lean.expected.out   | 149 +++++++
 15 files changed, 1121 insertions(+)
 create mode 100644 src/tests/VersoTests/DocStructure.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Genre.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Included.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Includes.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Metadata.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Nesting.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Term/Includes.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Term/Metadata.lean
 create mode 100644 src/tests/VersoTests/DocStructure/Term/Nesting.lean
 create mode 100644 src/tests/integration/doc-structure/expected/includes.txt
 create mode 100644 src/tests/integration/doc-structure/expected/metadata.txt
 create mode 100644 src/tests/integration/doc-structure/expected/nesting.txt
 create mode 100644 src/tests/interactive/test-cases/symbols_verso_nesting.lean
 create mode 100644 src/tests/interactive/test-cases/symbols_verso_nesting.lean.expected.out

diff --git a/src/tests/VersoTests/DocStructure.lean b/src/tests/VersoTests/DocStructure.lean
new file mode 100644
index 000000000..835365d88
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure.lean
@@ -0,0 +1,384 @@
+/-
+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 VersoTests.DocStructure.Genre
+import VersoTests.DocStructure.Included
+import VersoTests.DocStructure.Nesting
+import VersoTests.DocStructure.Metadata
+import VersoTests.DocStructure.Includes
+import VersoTests.DocStructure.Term.Nesting
+import VersoTests.DocStructure.Term.Metadata
+import VersoTests.DocStructure.Term.Includes
+
+set_option doc.verso true
+
+/-!
+Tests of the parts that document elaboration produces.
+
+The sample documents in {lit}`VersoTests.DocStructure` are elaborated three ways: block by block by
+the {lit}`#doc` command, and all at once by {lit}`#docs` and by the {lit}`#doc` term. All three
+must produce the same parts. The tests compare them with golden files.
+-/
+
+open Verso.Doc
+open Errata
+
+namespace Verso.Tests.DocStructure.Docs
+
+/- The document of `VersoTests.DocStructure.Nesting`, elaborated all at once by `#docs`. -/
+#docs (StructuralTesting) nesting "Nesting" :=
+:::::::
+
+Text before any header.
+
+A second paragraph before any header.
+
+# One
+
+Text in one.
+
+## One A
+
+Text in one A.
+
+### One A i
+
+Text in one A i.
+
+#### One A i x
+
+Text in one A i x.
+
+## One B
+
+Text in one B.
+
+### One B i
+
+# Two
+
+## Two A
+
+### Two A i
+
+Text in two A i.
+
+# Three
+
+Text in three.
+
+* a list
+* in three
+
+## Three A
+
+## Three B
+
+## Three C
+
+Text in three C.
+:::::::
+
+/- The document of `VersoTests.DocStructure.Metadata`, elaborated all at once by `#docs`. -/
+#docs (StructuralTesting) metadata "Metadata" :=
+:::::::
+%%%
+tag := "root"
+number := 1
+%%%
+
+Text in the root, with a [link][example] and a footnote.[^note]
+
+[example]: https://example.com
+
+# First
+%%%
+tag := "first"
+%%%
+
+Text in first.
+
+[^note]: The footnote text.
+
+## First Nested
+%%%
+number := 2
+%%%
+
+# Second
+
+Text in second, which has no metadata.
+
+[other]: https://example.org
+
+## Second Nested
+%%%
+tag := "second nested"
+number := 3
+%%%
+
+Text in second nested, with [another link][other].
+:::::::
+
+/- The document of `VersoTests.DocStructure.Includes`, elaborated all at once by `#docs`. -/
+#docs (StructuralTesting) includes "Includes" :=
+:::::::
+
+Text before the first include.
+
+{include VersoTests.DocStructure.Included}
+
+# Section
+
+Text in section.
+
+## Nested
+
+Text in nested.
+
+{include 2 VersoTests.DocStructure.Included}
+
+{include 1 VersoTests.DocStructure.Included}
+
+# After
+
+Text after the includes.
+
+## After Nested
+
+{include VersoTests.DocStructure.Included}
+
+{include 3 VersoTests.DocStructure.Included}
+:::::::
+
+end Verso.Tests.DocStructure.Docs
+
+namespace Verso.Tests.DocStructure
+
+/-- The directory that holds the golden files and the test output. -/
+def baseDir : System.FilePath := "src/tests/integration/doc-structure"
+
+/--
+Renders each document's parts to {lit}`output/<dir>/<name>.txt`, then compares the output with the
+golden files in {lit}`expected`.
+-/
+def checkStructure (dir : String) (docs : List (String × Part StructuralTesting)) : Test := do
+  let output := baseDir / "output" / dir
+  if ← output.pathExists then IO.FS.removeDirAll output
+  IO.FS.createDirAll output
+  for (name, part) in docs do
+    IO.FS.writeFile (output / s!"{name}.txt") (renderPart part)
+  goldenDir (baseDir / "expected") output
+
+/-- The documents elaborated block by block by the {lit}`#doc` command match the golden files. -/
+@[test]
+def docCommand : Test :=
+  checkStructure "doc-command" [
+    ("nesting", %doc VersoTests.DocStructure.Nesting),
+    ("metadata", %doc VersoTests.DocStructure.Metadata),
+    ("includes", %doc VersoTests.DocStructure.Includes)
+  ]
+
+/-- The documents elaborated all at once by {lit}`#docs` match the golden files. -/
+@[test]
+def docsCommand : Test :=
+  checkStructure "docs-command" [
+    ("nesting", Docs.nesting.toPart),
+    ("metadata", Docs.metadata.toPart),
+    ("includes", Docs.includes.toPart)
+  ]
+
+/-- The documents elaborated all at once by the {lit}`#doc` term match the golden files. -/
+@[test]
+def docTerm : Test :=
+  checkStructure "doc-term" [
+    ("nesting", Term.nesting.toPart),
+    ("metadata", Term.metadata.toPart),
+    ("includes", Term.includes.toPart)
+  ]
+
+end Verso.Tests.DocStructure
+
+namespace Verso.Tests.DocStructure.Errors
+
+/- Errors for badly structured parts. -/
+
+/--
+error: Wrong header nesting - got ### but expected at most ##
+-/
+#test_msgs in
+#docs (StructuralTesting) wrongNesting "Wrong Nesting" :=
+:::::::
+# One
+
+### Too Deep
+
+Text.
+:::::::
+
+/--
+error: Wrong header nesting - got ### but expected at most ##
+-/
+#test_msgs in
+#docs (StructuralTesting) wrongNestingAfterClose "Wrong Nesting After Closing Several Parts" :=
+:::::::
+# A
+
+## B
+
+### C
+
+# D
+
+### E
+:::::::
+
+/--
+error: Wrong header nesting - got ## but expected at most #
+-/
+#test_msgs in
+#docs (StructuralTesting) wrongNestingAtRoot "Wrong Nesting at the Root" :=
+:::::::
+## Too Deep
+:::::::
+
+/--
+error: Metadata blocks must precede both content and subsections
+-/
+#test_msgs in
+#docs (StructuralTesting) metadataAfterContent "Metadata After Content" :=
+:::::::
+Text.
+
+%%%
+tag := "late"
+%%%
+:::::::
+
+/--
+error: Metadata blocks must precede both content and subsections
+-/
+#test_msgs in
+#docs (StructuralTesting) metadataAfterContentInSection "Metadata After Content in a Section" :=
+:::::::
+# Section
+
+Text.
+
+%%%
+tag := "late"
+%%%
+:::::::
+
+/--
+error: Metadata blocks must precede both content and subsections
+-/
+#test_msgs in
+#docs (StructuralTesting) metadataAfterSubPart "Metadata After a Sub-Part" :=
+:::::::
+# Section
+
+{include VersoTests.DocStructure.Included}
+
+%%%
+tag := "late"
+%%%
+:::::::
+
+/--
+error: Metadata already provided for this section
+-/
+#test_msgs in
+#docs (StructuralTesting) duplicateMetadata "Duplicate Metadata" :=
+:::::::
+%%%
+tag := "first"
+%%%
+
+%%%
+tag := "second"
+%%%
+:::::::
+
+/--
+error: Metadata already provided for this section
+-/
+#test_msgs in
+#docs (StructuralTesting) duplicateMetadataInSection "Duplicate Metadata in a Section" :=
+:::::::
+# Section
+%%%
+tag := "first"
+%%%
+
+%%%
+tag := "second"
+%%%
+:::::::
+
+/--
+error: Block content found in a context where a header was expected.
+
+
+Note: A document part (section/chapter/etc) consists of a header, followed by zero or more blocks, followed by zero or more sub-parts. This block occurs after a sub-part (namely `VersoTests.DocStructure.Included`), but outside of the sub-parts.
+-/
+#test_msgs in
+#docs (StructuralTesting) contentAfterInclude "Content After an Include" :=
+:::::::
+Text.
+
+{include VersoTests.DocStructure.Included}
+
+More text.
+:::::::
+
+/--
+error: Block content found in a context where a header was expected.
+
+
+Note: A document part (section/chapter/etc) consists of a header, followed by zero or more blocks, followed by zero or more sub-parts. This block occurs after a sub-part (namely `VersoTests.DocStructure.Included`), but outside of the sub-parts.
+-/
+#test_msgs in
+#docs (StructuralTesting) contentAfterIncludeInSection "Content After an Include in a Section" :=
+:::::::
+# Section
+
+{include 2 VersoTests.DocStructure.Included}
+
+* A list
+:::::::
+
+open Lean Lean.Elab Lean.Doc.Syntax Verso.Doc.Elab PartElabM in
+/--
+Adds a finished part with the title {lit}`Built Part` as a sub-part of the root part. It is an
+example of a part command that builds a whole part.
+-/
+@[part_command Lean.Doc.Syntax.command]
+meta def builtPart : PartCommand
+  | stx@`(block|command{builtPart $args*}) => do
+    unless args.isEmpty do throwErrorAt stx "Expected no arguments"
+    let endPos := stx.getTailPos?.getD 0
+    closePartsUntil 1 (stx.getPos?.getD 0)
+    addPart <| .mk stx stx #[] "Built Part" none #[] #[] endPos
+  | _ => throwUnsupportedSyntax
+
+/--
+error: Block content found in a context where a header was expected.
+
+
+Note: A document part (section/chapter/etc) consists of a header, followed by zero or more blocks, followed by zero or more sub-parts. This block occurs after a sub-part (namely “Built Part”), but outside of the sub-parts.
+-/
+#test_msgs in
+#docs (StructuralTesting) contentAfterBuiltPart "Content After a Built Part" :=
+:::::::
+# Section
+
+{builtPart}
+
+Text.
+:::::::
+
+end Verso.Tests.DocStructure.Errors
diff --git a/src/tests/VersoTests/DocStructure/Genre.lean b/src/tests/VersoTests/DocStructure/Genre.lean
new file mode 100644
index 000000000..25a1ec436
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Genre.lean
@@ -0,0 +1,75 @@
+/-
+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
+public import Verso
+
+set_option doc.verso true
+
+/-!
+A minimal genre for the document structure tests, and a text rendering of a document's parts.
+-/
+
+namespace Verso.Tests.DocStructure
+
+open Verso.Doc
+
+/-- The part metadata of the test genre. -/
+public structure StructuralTesting.Metadata where
+  tag : String := ""
+  number : Nat := 0
+deriving Repr
+
+/-- A genre whose only feature is its part metadata. -/
+@[expose]
+public def StructuralTesting : Genre where
+  PartMetadata := StructuralTesting.Metadata
+  Block := Empty
+  Inline := Empty
+  TraverseContext := Unit
+  TraverseState := Unit
+
+public instance : Repr (Genre.PartMetadata StructuralTesting) :=
+  inferInstanceAs (Repr StructuralTesting.Metadata)
+
+/-- A plain-text summary of some inline content. -/
+partial def inlineSummary : Inline StructuralTesting → String
+  | .text s | .code s | .math _ s => s
+  | .linebreak _ => " "
+  | .emph xs | .bold xs | .concat xs => String.join (xs.map inlineSummary).toList
+  | .link xs url => s!"[{String.join (xs.map inlineSummary).toList}]({url})"
+  | .footnote name _ => s!"[^{name}]"
+  | .image alt url => s!"![{alt}]({url})"
+  | .other e _ => nomatch e
+
+/-- A one-line summary of a block. -/
+def blockSummary : Block StructuralTesting → String
+  | .para xs => s!"para: {(String.join (xs.map inlineSummary).toList).trimAscii}"
+  | .code s => s!"code: {s.trimAscii}"
+  | .ul items => s!"ul: {items.size} items"
+  | .ol _ items => s!"ol: {items.size} items"
+  | .dl items => s!"dl: {items.size} items"
+  | .blockquote items => s!"blockquote: {items.size} blocks"
+  | .concat items => s!"concat: {items.size} blocks"
+  | .other e _ => nomatch e
+
+/--
+Renders a part as indented text: its title, metadata, blocks and sub-parts. Included documents
+appear as the parts they contain.
+-/
+public partial def renderPart (part : Part StructuralTesting) (depth : Nat := 0) : String :=
+  let indent := "".pushn ' ' (2 * depth)
+  let header := s!"{indent}part {part.titleString.quote}\n"
+  let metadata :=
+    match part.metadata with
+    | some m => s!"{indent}  metadata: {reprStr m}\n"
+    | none => ""
+  let blocks :=
+    s!"{indent}  blocks: {part.content.size}\n" ++
+    String.join (part.content.map (s!"{indent}  - {blockSummary ·}\n")).toList
+  let subParts := String.join (part.subParts.map (renderPart · (depth + 1))).toList
+  header ++ metadata ++ blocks ++ subParts
+
+end Verso.Tests.DocStructure
diff --git a/src/tests/VersoTests/DocStructure/Included.lean b/src/tests/VersoTests/DocStructure/Included.lean
new file mode 100644
index 000000000..9b0304880
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Included.lean
@@ -0,0 +1,23 @@
+/-
+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 VersoTests.DocStructure.Genre
+
+open Verso.Tests.DocStructure
+
+/-!
+A document that the other document structure samples include.
+-/
+
+#doc (StructuralTesting) "Included Document" =>
+%%%
+tag := "included"
+%%%
+
+Text of the included document.
+
+# Included Section
+
+Text of the included section.
diff --git a/src/tests/VersoTests/DocStructure/Includes.lean b/src/tests/VersoTests/DocStructure/Includes.lean
new file mode 100644
index 000000000..705b172cc
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Includes.lean
@@ -0,0 +1,41 @@
+/-
+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 VersoTests.DocStructure.Genre
+import VersoTests.DocStructure.Included
+
+open Verso.Tests.DocStructure
+
+/-!
+Included documents, with and without an explicit header level.
+-/
+
+#doc (StructuralTesting) "Includes" =>
+
+Text before the first include.
+
+{include VersoTests.DocStructure.Included}
+
+# Section
+
+Text in section.
+
+## Nested
+
+Text in nested.
+
+{include 2 VersoTests.DocStructure.Included}
+
+{include 1 VersoTests.DocStructure.Included}
+
+# After
+
+Text after the includes.
+
+## After Nested
+
+{include VersoTests.DocStructure.Included}
+
+{include 3 VersoTests.DocStructure.Included}
diff --git a/src/tests/VersoTests/DocStructure/Metadata.lean b/src/tests/VersoTests/DocStructure/Metadata.lean
new file mode 100644
index 000000000..668c9b7bd
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Metadata.lean
@@ -0,0 +1,50 @@
+/-
+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 VersoTests.DocStructure.Genre
+
+open Verso.Tests.DocStructure
+
+/-!
+Metadata on the root part and on sub-parts, with link and footnote definitions between headers.
+-/
+
+#doc (StructuralTesting) "Metadata" =>
+%%%
+tag := "root"
+number := 1
+%%%
+
+Text in the root, with a [link][example] and a footnote.[^note]
+
+[example]: https://example.com
+
+# First
+%%%
+tag := "first"
+%%%
+
+Text in first.
+
+[^note]: The footnote text.
+
+## First Nested
+%%%
+number := 2
+%%%
+
+# Second
+
+Text in second, which has no metadata.
+
+[other]: https://example.org
+
+## Second Nested
+%%%
+tag := "second nested"
+number := 3
+%%%
+
+Text in second nested, with [another link][other].
diff --git a/src/tests/VersoTests/DocStructure/Nesting.lean b/src/tests/VersoTests/DocStructure/Nesting.lean
new file mode 100644
index 000000000..7cc1109ce
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Nesting.lean
@@ -0,0 +1,63 @@
+/-
+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 VersoTests.DocStructure.Genre
+
+open Verso.Tests.DocStructure
+
+/-!
+Nested headers, headers that return to shallower levels, and sibling parts.
+-/
+
+#doc (StructuralTesting) "Nesting" =>
+
+Text before any header.
+
+A second paragraph before any header.
+
+# One
+
+Text in one.
+
+## One A
+
+Text in one A.
+
+### One A i
+
+Text in one A i.
+
+#### One A i x
+
+Text in one A i x.
+
+## One B
+
+Text in one B.
+
+### One B i
+
+# Two
+
+## Two A
+
+### Two A i
+
+Text in two A i.
+
+# Three
+
+Text in three.
+
+* a list
+* in three
+
+## Three A
+
+## Three B
+
+## Three C
+
+Text in three C.
diff --git a/src/tests/VersoTests/DocStructure/Term/Includes.lean b/src/tests/VersoTests/DocStructure/Term/Includes.lean
new file mode 100644
index 000000000..ac03c12d2
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Term/Includes.lean
@@ -0,0 +1,41 @@
+/-
+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 VersoTests.DocStructure.Genre
+import VersoTests.DocStructure.Included
+
+open Verso.Doc Verso.Tests.DocStructure
+
+/-!
+The document of `VersoTests.DocStructure.Includes`, elaborated all at once by the `#doc` term.
+-/
+
+def Verso.Tests.DocStructure.Term.includes : VersoDoc StructuralTesting := #doc (StructuralTesting) "Includes" =>
+
+Text before the first include.
+
+{include VersoTests.DocStructure.Included}
+
+# Section
+
+Text in section.
+
+## Nested
+
+Text in nested.
+
+{include 2 VersoTests.DocStructure.Included}
+
+{include 1 VersoTests.DocStructure.Included}
+
+# After
+
+Text after the includes.
+
+## After Nested
+
+{include VersoTests.DocStructure.Included}
+
+{include 3 VersoTests.DocStructure.Included}
diff --git a/src/tests/VersoTests/DocStructure/Term/Metadata.lean b/src/tests/VersoTests/DocStructure/Term/Metadata.lean
new file mode 100644
index 000000000..9a28a0d07
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Term/Metadata.lean
@@ -0,0 +1,50 @@
+/-
+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 VersoTests.DocStructure.Genre
+
+open Verso.Doc Verso.Tests.DocStructure
+
+/-!
+The document of `VersoTests.DocStructure.Metadata`, elaborated all at once by the `#doc` term.
+-/
+
+def Verso.Tests.DocStructure.Term.metadata : VersoDoc StructuralTesting := #doc (StructuralTesting) "Metadata" =>
+%%%
+tag := "root"
+number := 1
+%%%
+
+Text in the root, with a [link][example] and a footnote.[^note]
+
+[example]: https://example.com
+
+# First
+%%%
+tag := "first"
+%%%
+
+Text in first.
+
+[^note]: The footnote text.
+
+## First Nested
+%%%
+number := 2
+%%%
+
+# Second
+
+Text in second, which has no metadata.
+
+[other]: https://example.org
+
+## Second Nested
+%%%
+tag := "second nested"
+number := 3
+%%%
+
+Text in second nested, with [another link][other].
diff --git a/src/tests/VersoTests/DocStructure/Term/Nesting.lean b/src/tests/VersoTests/DocStructure/Term/Nesting.lean
new file mode 100644
index 000000000..a4b226ac8
--- /dev/null
+++ b/src/tests/VersoTests/DocStructure/Term/Nesting.lean
@@ -0,0 +1,63 @@
+/-
+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 VersoTests.DocStructure.Genre
+
+open Verso.Doc Verso.Tests.DocStructure
+
+/-!
+The document of `VersoTests.DocStructure.Nesting`, elaborated all at once by the `#doc` term.
+-/
+
+def Verso.Tests.DocStructure.Term.nesting : VersoDoc StructuralTesting := #doc (StructuralTesting) "Nesting" =>
+
+Text before any header.
+
+A second paragraph before any header.
+
+# One
+
+Text in one.
+
+## One A
+
+Text in one A.
+
+### One A i
+
+Text in one A i.
+
+#### One A i x
+
+Text in one A i x.
+
+## One B
+
+Text in one B.
+
+### One B i
+
+# Two
+
+## Two A
+
+### Two A i
+
+Text in two A i.
+
+# Three
+
+Text in three.
+
+* a list
+* in three
+
+## Three A
+
+## Three B
+
+## Three C
+
+Text in three C.
diff --git a/src/tests/VersoTests/VersoManual/Markdown.lean b/src/tests/VersoTests/VersoManual/Markdown.lean
index e93137656..413607533 100644
--- a/src/tests/VersoTests/VersoManual/Markdown.lean
+++ b/src/tests/VersoTests/VersoManual/Markdown.lean
@@ -76,6 +76,23 @@ def markdownPartRangesValid (input : String) : Elab.TermElabM Bool := do
     let (_, _, part) ← addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default
     return part.partContext.priorParts.all partRangesValid
 
+open PartElabM in
+/--
+Adds a Markdown header while `currentHeaderLevels` lists one Markdown section. The root part is the
+only part under construction, so closing that section fails.
+-/
+def closeMarkdownSectionAtRoot : Elab.TermElabM Unit := do
+  let some parsed := MD4Lean.parse "# Header"
+    | throwError m!"Couldn't parse markdown"
+  let addParts : PartElabM Unit := do
+    for block in parsed.blocks do
+      discard <| addPartFromMarkdown block (currentHeaderLevels := [1])
+  discard <| addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default
+
+/-- error: Failed to close verso part corresponding to markdown section: no parts left -/
+#test_msgs in
+#eval closeMarkdownSectionAtRoot
+
 /-- info: true -/
 #test_msgs in
 #eval markdownPartRangesValid r#"
diff --git a/src/tests/integration/doc-structure/expected/includes.txt b/src/tests/integration/doc-structure/expected/includes.txt
new file mode 100644
index 000000000..cce8f48c4
--- /dev/null
+++ b/src/tests/integration/doc-structure/expected/includes.txt
@@ -0,0 +1,49 @@
+part "Includes"
+  blocks: 1
+  - para: Text before the first include.
+  part "Included Document"
+    metadata: { tag := "included", number := 0 }
+    blocks: 1
+    - para: Text of the included document.
+    part "Included Section"
+      blocks: 1
+      - para: Text of the included section.
+  part "Section"
+    blocks: 1
+    - para: Text in section.
+    part "Nested"
+      blocks: 1
+      - para: Text in nested.
+    part "Included Document"
+      metadata: { tag := "included", number := 0 }
+      blocks: 1
+      - para: Text of the included document.
+      part "Included Section"
+        blocks: 1
+        - para: Text of the included section.
+  part "Included Document"
+    metadata: { tag := "included", number := 0 }
+    blocks: 1
+    - para: Text of the included document.
+    part "Included Section"
+      blocks: 1
+      - para: Text of the included section.
+  part "After"
+    blocks: 1
+    - para: Text after the includes.
+    part "After Nested"
+      blocks: 0
+      part "Included Document"
+        metadata: { tag := "included", number := 0 }
+        blocks: 1
+        - para: Text of the included document.
+        part "Included Section"
+          blocks: 1
+          - para: Text of the included section.
+      part "Included Document"
+        metadata: { tag := "included", number := 0 }
+        blocks: 1
+        - para: Text of the included document.
+        part "Included Section"
+          blocks: 1
+          - para: Text of the included section.
diff --git a/src/tests/integration/doc-structure/expected/metadata.txt b/src/tests/integration/doc-structure/expected/metadata.txt
new file mode 100644
index 000000000..3e1d7999f
--- /dev/null
+++ b/src/tests/integration/doc-structure/expected/metadata.txt
@@ -0,0 +1,18 @@
+part "Metadata"
+  metadata: { tag := "root", number := 1 }
+  blocks: 1
+  - para: Text in the root, with a [link](https://example.com) and a footnote.[^note]
+  part "First"
+    metadata: { tag := "first", number := 0 }
+    blocks: 1
+    - para: Text in first.
+    part "First Nested"
+      metadata: { tag := "", number := 2 }
+      blocks: 0
+  part "Second"
+    blocks: 1
+    - para: Text in second, which has no metadata.
+    part "Second Nested"
+      metadata: { tag := "second nested", number := 3 }
+      blocks: 1
+      - para: Text in second nested, with [another link](https://example.org).
diff --git a/src/tests/integration/doc-structure/expected/nesting.txt b/src/tests/integration/doc-structure/expected/nesting.txt
new file mode 100644
index 000000000..5dae1540b
--- /dev/null
+++ b/src/tests/integration/doc-structure/expected/nesting.txt
@@ -0,0 +1,39 @@
+part "Nesting"
+  blocks: 2
+  - para: Text before any header.
+  - para: A second paragraph before any header.
+  part "One"
+    blocks: 1
+    - para: Text in one.
+    part "One A"
+      blocks: 1
+      - para: Text in one A.
+      part "One A i"
+        blocks: 1
+        - para: Text in one A i.
+        part "One A i x"
+          blocks: 1
+          - para: Text in one A i x.
+    part "One B"
+      blocks: 1
+      - para: Text in one B.
+      part "One B i"
+        blocks: 0
+  part "Two"
+    blocks: 0
+    part "Two A"
+      blocks: 0
+      part "Two A i"
+        blocks: 1
+        - para: Text in two A i.
+  part "Three"
+    blocks: 2
+    - para: Text in three.
+    - ul: 2 items
+    part "Three A"
+      blocks: 0
+    part "Three B"
+      blocks: 0
+    part "Three C"
+      blocks: 1
+      - para: Text in three C.
diff --git a/src/tests/interactive/test-cases/symbols_verso_nesting.lean b/src/tests/interactive/test-cases/symbols_verso_nesting.lean
new file mode 100644
index 000000000..15081734a
--- /dev/null
+++ b/src/tests/interactive/test-cases/symbols_verso_nesting.lean
@@ -0,0 +1,59 @@
+import VersoTests.DocStructure.Genre
+import VersoTests.DocStructure.Included
+
+open Verso.Tests.DocStructure
+
+-- Document symbols and folding ranges for deep nesting, headers that return to shallower levels,
+-- included documents and metadata. Synchronize first so that the whole document is elaborated.
+-- The `--^` requests come before the document. After it, they would be paragraph text in its last
+-- part, and they would change what the test measures.
+--^ sync
+--^ textDocument/documentSymbol
+--^ textDocument/foldingRange
+
+#doc (StructuralTesting) "Nesting Symbols" =>
+%%%
+tag := "root"
+%%%
+
+Text before any header.
+
+# One
+%%%
+tag := "one"
+%%%
+
+Text in one.
+
+## One A
+
+### One A i
+
+#### One A i x
+
+Text in one A i x.
+
+{include 3 VersoTests.DocStructure.Included}
+
+## One B
+
+{include 2 VersoTests.DocStructure.Included}
+
+# Two
+%%%
+number := 2
+%%%
+
+{include VersoTests.DocStructure.Included}
+
+# Three
+
+## Three A
+
+### Three A i
+
+Text in three A i.
+
+# Four
+
+Text at the end of the document.
diff --git a/src/tests/interactive/test-cases/symbols_verso_nesting.lean.expected.out b/src/tests/interactive/test-cases/symbols_verso_nesting.lean.expected.out
new file mode 100644
index 000000000..af64ff5fa
--- /dev/null
+++ b/src/tests/interactive/test-cases/symbols_verso_nesting.lean.expected.out
@@ -0,0 +1,149 @@
+{"textDocument":
+ {"uri": "file:///src/tests/interactive/test-cases/symbols_verso_nesting.lean"},
+ "position": {"line": 8, "character": 2}}
+[{"selectionRange":
+  {"start": {"line": 13, "character": 25},
+   "end": {"line": 13, "character": 42}},
+  "range":
+  {"start": {"line": 13, "character": 0}, "end": {"line": 59, "character": 0}},
+  "name": "Nesting Symbols",
+  "kind": 15,
+  "children":
+  [{"selectionRange":
+    {"start": {"line": 20, "character": 0},
+     "end": {"line": 20, "character": 5}},
+    "range":
+    {"start": {"line": 20, "character": 0},
+     "end": {"line": 41, "character": 0}},
+    "name": "One",
+    "kind": 15,
+    "children":
+    [{"selectionRange":
+      {"start": {"line": 27, "character": 0},
+       "end": {"line": 27, "character": 8}},
+      "range":
+      {"start": {"line": 27, "character": 0},
+       "end": {"line": 37, "character": 0}},
+      "name": "One A",
+      "kind": 15,
+      "children":
+      [{"selectionRange":
+        {"start": {"line": 29, "character": 0},
+         "end": {"line": 29, "character": 11}},
+        "range":
+        {"start": {"line": 29, "character": 0},
+         "end": {"line": 35, "character": 0}},
+        "name": "One A i",
+        "kind": 15,
+        "children":
+        [{"selectionRange":
+          {"start": {"line": 31, "character": 0},
+           "end": {"line": 31, "character": 14}},
+          "range":
+          {"start": {"line": 31, "character": 0},
+           "end": {"line": 35, "character": 0}},
+          "name": "One A i x",
+          "kind": 15}]},
+       {"selectionRange":
+        {"start": {"line": 35, "character": 11},
+         "end": {"line": 35, "character": 43}},
+        "range":
+        {"start": {"line": 35, "character": 11},
+         "end": {"line": 35, "character": 43}},
+        "name": "VersoTests.DocStructure.Included",
+        "kind": 7,
+        "detail":
+        "Included from VersoTests.DocStructure.Included.«the canonical document object name»"}]},
+     {"selectionRange":
+      {"start": {"line": 37, "character": 0},
+       "end": {"line": 37, "character": 8}},
+      "range":
+      {"start": {"line": 37, "character": 0},
+       "end": {"line": 39, "character": 0}},
+      "name": "One B",
+      "kind": 15},
+     {"selectionRange":
+      {"start": {"line": 39, "character": 11},
+       "end": {"line": 39, "character": 43}},
+      "range":
+      {"start": {"line": 39, "character": 11},
+       "end": {"line": 39, "character": 43}},
+      "name": "VersoTests.DocStructure.Included",
+      "kind": 7,
+      "detail":
+      "Included from VersoTests.DocStructure.Included.«the canonical document object name»"}]},
+   {"selectionRange":
+    {"start": {"line": 41, "character": 0},
+     "end": {"line": 41, "character": 5}},
+    "range":
+    {"start": {"line": 41, "character": 0},
+     "end": {"line": 48, "character": 0}},
+    "name": "Two",
+    "kind": 15,
+    "children":
+    [{"selectionRange":
+      {"start": {"line": 46, "character": 9},
+       "end": {"line": 46, "character": 41}},
+      "range":
+      {"start": {"line": 46, "character": 9},
+       "end": {"line": 46, "character": 41}},
+      "name": "VersoTests.DocStructure.Included",
+      "kind": 7,
+      "detail":
+      "Included from VersoTests.DocStructure.Included.«the canonical document object name»"}]},
+   {"selectionRange":
+    {"start": {"line": 48, "character": 0},
+     "end": {"line": 48, "character": 7}},
+    "range":
+    {"start": {"line": 48, "character": 0},
+     "end": {"line": 56, "character": 0}},
+    "name": "Three",
+    "kind": 15,
+    "children":
+    [{"selectionRange":
+      {"start": {"line": 50, "character": 0},
+       "end": {"line": 50, "character": 10}},
+      "range":
+      {"start": {"line": 50, "character": 0},
+       "end": {"line": 56, "character": 0}},
+      "name": "Three A",
+      "kind": 15,
+      "children":
+      [{"selectionRange":
+        {"start": {"line": 52, "character": 0},
+         "end": {"line": 52, "character": 13}},
+        "range":
+        {"start": {"line": 52, "character": 0},
+         "end": {"line": 56, "character": 0}},
+        "name": "Three A i",
+        "kind": 15}]}]},
+   {"selectionRange":
+    {"start": {"line": 56, "character": 0},
+     "end": {"line": 56, "character": 6}},
+    "range":
+    {"start": {"line": 56, "character": 0},
+     "end": {"line": 59, "character": 0}},
+    "name": "Four",
+    "kind": 15}]}]
+{"textDocument":
+ {"uri": "file:///src/tests/interactive/test-cases/symbols_verso_nesting.lean"},
+ "position": {"line": 8, "character": 2}}
+[{"startLine": 13, "endLine": 58},
+ {"startLine": 20, "endLine": 40},
+ {"startLine": 27, "endLine": 36},
+ {"startLine": 29, "endLine": 34},
+ {"startLine": 31, "endLine": 34},
+ {"startLine": 37, "endLine": 38},
+ {"startLine": 41, "endLine": 47},
+ {"startLine": 48, "endLine": 55},
+ {"startLine": 50, "endLine": 55},
+ {"startLine": 52, "endLine": 55},
+ {"startLine": 56, "endLine": 58},
+ {"startLine": 14, "endLine": 16},
+ {"startLine": 21, "endLine": 23},
+ {"startLine": 42, "endLine": 44},
+ {"startLine": 0, "kind": "imports", "endLine": 3},
+ {"startLine": 14, "kind": "region", "endLine": 16},
+ {"startLine": 21, "kind": "region", "endLine": 23},
+ {"startLine": 42, "kind": "region", "endLine": 44},
+ {"startLine": 58, "kind": "region", "endLine": 59}]

From e7496ac20c7444618c68e24e6d0bfc138664f956 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 29 Sep 2026 16:40:42 +0200
Subject: [PATCH 2/4] test: match builtPart on the part command's view

On nightly-testing, part commands receive a block view instead of
syntax, so the builtPart test command matches on `.command v`.
---
 src/tests/VersoTests/DocStructure.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/tests/VersoTests/DocStructure.lean b/src/tests/VersoTests/DocStructure.lean
index 835365d88..f13627917 100644
--- a/src/tests/VersoTests/DocStructure.lean
+++ b/src/tests/VersoTests/DocStructure.lean
@@ -351,15 +351,17 @@ Note: A document part (section/chapter/etc) consists of a header, followed by ze
 * A list
 :::::::
 
-open Lean Lean.Elab Lean.Doc.Syntax Verso.Doc.Elab PartElabM in
+open Lean Lean.Elab Verso.Doc.Elab PartElabM in
 /--
 Adds a finished part with the title {lit}`Built Part` as a sub-part of the root part. It is an
 example of a part command that builds a whole part.
 -/
-@[part_command Lean.Doc.Syntax.command]
+@[part_command Lean.Doc.Parser.Block.command]
 meta def builtPart : PartCommand
-  | stx@`(block|command{builtPart $args*}) => do
-    unless args.isEmpty do throwErrorAt stx "Expected no arguments"
+  | .command v => do
+    unless v.name.getId == `builtPart do throwUnsupportedSyntax
+    let stx ← getRef
+    unless v.args.isEmpty do throwErrorAt stx "Expected no arguments"
     let endPos := stx.getTailPos?.getD 0
     closePartsUntil 1 (stx.getPos?.getD 0)
     addPart <| .mk stx stx #[] "Built Part" none #[] #[] endPos

From c5b5e366572d1c7d386420acd5e09eab4d5b7d17 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 30 Sep 2026 09:13:06 +0200
Subject: [PATCH 3/4] fix: dep versions

---
 .../literate-config/lake-manifest.json        | 143 ++++++++++--------
 .../literate-multi-root/lake-manifest.json    | 143 ++++++++++--------
 2 files changed, 158 insertions(+), 128 deletions(-)

diff --git a/test-projects/literate-config/lake-manifest.json b/test-projects/literate-config/lake-manifest.json
index 6c61161cf..8ba776da0 100644
--- a/test-projects/literate-config/lake-manifest.json
+++ b/test-projects/literate-config/lake-manifest.json
@@ -1,64 +1,79 @@
-{"version": "1.3.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"type": "path",
-   "scope": "",
-   "name": "verso",
-   "manifestFile": "lake-manifest.json",
-   "inherited": false,
-   "dir": "../..",
-   "copy": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/illuminate",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f",
-   "name": "illuminate",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/plausible",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "b7fb2b866d25bd937a2069931f9733197521cb27",
-   "name": "plausible",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/subverso",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c",
-   "name": "subverso",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"}],
- "name": "«literate-config-test»",
- "lakeDir": ".lake",
- "fixedToolchain": false}
+{
+  "version": "1.3.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "type": "path",
+      "scope": "",
+      "name": "verso",
+      "manifestFile": "lake-manifest.json",
+      "inherited": false,
+      "dir": "../..",
+      "copy": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/illuminate",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f",
+      "name": "illuminate",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "b7fb2b866d25bd937a2069931f9733197521cb27",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/acmepjz/md4lean",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
+      "name": "MD4Lean",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover/subverso",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c",
+      "name": "subverso",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    }
+  ],
+  "name": "«literate-config-test»",
+  "lakeDir": ".lake",
+  "fixedToolchain": false
+}
diff --git a/test-projects/literate-multi-root/lake-manifest.json b/test-projects/literate-multi-root/lake-manifest.json
index 8da095fdb..ed2bbf005 100644
--- a/test-projects/literate-multi-root/lake-manifest.json
+++ b/test-projects/literate-multi-root/lake-manifest.json
@@ -1,64 +1,79 @@
-{"version": "1.3.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"type": "path",
-   "scope": "",
-   "name": "verso",
-   "manifestFile": "lake-manifest.json",
-   "inherited": false,
-   "dir": "../..",
-   "copy": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/illuminate",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f",
-   "name": "illuminate",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/plausible",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "b7fb2b866d25bd937a2069931f9733197521cb27",
-   "name": "plausible",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/subverso",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c",
-   "name": "subverso",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"}],
- "name": "«literate-multi-root-test»",
- "lakeDir": ".lake",
- "fixedToolchain": false}
+{
+  "version": "1.3.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "type": "path",
+      "scope": "",
+      "name": "verso",
+      "manifestFile": "lake-manifest.json",
+      "inherited": false,
+      "dir": "../..",
+      "copy": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/illuminate",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f",
+      "name": "illuminate",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "b7fb2b866d25bd937a2069931f9733197521cb27",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/acmepjz/md4lean",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
+      "name": "MD4Lean",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover/subverso",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c",
+      "name": "subverso",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    }
+  ],
+  "name": "«literate-multi-root-test»",
+  "lakeDir": ".lake",
+  "fixedToolchain": false
+}

From b8260c1941945504c485747c126228f1b8a76b38 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Wed, 30 Sep 2026 07:15:30 +0000
Subject: [PATCH 4/4] ci: sync test-project lean-toolchains

---
 test-projects/errata-widget/lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-projects/errata-widget/lean-toolchain b/test-projects/errata-widget/lean-toolchain
index 788a4d267..f39649bac 100644
--- a/test-projects/errata-widget/lean-toolchain
+++ b/test-projects/errata-widget/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-09-27
+leanprover/lean4:nightly-2026-09-29