From 5ce1f67261a3393bbe97e365b8ab595b8971fe70 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Mon, 17 Nov 2025 14:57:00 +0100
Subject: [PATCH] fix: module docstring header nesting in Verso format (#11215)

This PR fixes an issue where header nesting levels were properly tracked
between, but not within, moduledocs.
---
 src/Lean/Elab/DocString.lean         |  1 +
 tests/lean/run/versoDocMarkdown.lean |  3 ++
 tests/lean/run/versoDocNesting.lean  | 58 ++++++++++++++++++++++++++++
 3 files changed, 62 insertions(+)
 create mode 100644 tests/lean/run/versoDocNesting.lean

diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
index fba7da5239..4974d39b88 100644
--- a/src/Lean/Elab/DocString.lean
+++ b/src/Lean/Elab/DocString.lean
@@ -1491,6 +1491,7 @@ private def elabModSnippet'
           logErrorAt b m!"Incorrect header nesting: expected at most `{"#".pushn '#' maxLevel}` \
             but got `{"#".pushn '#' n}`"
         else
+          maxLevel := n + 1
           let title ←
             liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := b}) <|
               name.mapM elabInline
diff --git a/tests/lean/run/versoDocMarkdown.lean b/tests/lean/run/versoDocMarkdown.lean
index 9d7e5bcf42..893759e415 100644
--- a/tests/lean/run/versoDocMarkdown.lean
+++ b/tests/lean/run/versoDocMarkdown.lean
@@ -8,6 +8,9 @@ set_option doc.verso true
 This module tests the Markdown rendering of all the builtin Verso docstring operators.
 
 Each section begins with a command that will fail when a new, untested operator is added.
+
+## Helpers
+
 -/
 
 section
diff --git a/tests/lean/run/versoDocNesting.lean b/tests/lean/run/versoDocNesting.lean
new file mode 100644
index 0000000000..333cff9d23
--- /dev/null
+++ b/tests/lean/run/versoDocNesting.lean
@@ -0,0 +1,58 @@
+set_option doc.verso true
+
+/-!
+This test checks that header nesting rules are enforced within and across Verso module docs.
+
+First, within.
+
+# A
+## B
+### C
+-/
+
+
+/-- error: Incorrect header nesting: expected at most `###` but got `####` -/
+#guard_msgs in
+/-!
+# A
+## B
+#### C
+-/
+
+/-- error: Incorrect header nesting: expected at most `##` but got `###` -/
+#guard_msgs in
+/-!
+# A
+## B
+### C
+#### D
+# E
+### F
+-/
+
+/-!
+Now, check between blocks.
+
+# A
+## B
+-/
+
+/-!
+### C
+-/
+
+/-- error: Incorrect header nesting: expected at most `####` but got `#####` -/
+#guard_msgs in
+/-!
+##### D
+-/
+
+/-!
+# A
+-/
+
+/-- error: Incorrect header nesting: expected at most `##` but got `#####` -/
+#guard_msgs in
+/-!
+##### B
+-/