Verso docstring appears to ignore header on 0th line

[Vierkantor]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When a Verso module or declaration docstring has a #-header on the same line as the opening bracket, this seems to be ignored for header nesting purposes:

set_option doc.verso true

/-! # Level 1 doc

## Level 2 doc
-/ -- error on previous line:
-- error: Incorrect header nesting: expected at most `#` but got `##`

/-- # Level 1 doc

## Level 2 doc
-/ -- error on previous line:
-- error: Expected a header no deeper than `#`
def foo := 1

Context

Mathlib commonly uses /-! ## Section -/ module docstrings to separate declarations from each other in the doc-gen output, so having one-line headers would be very useful.

Steps to Reproduce

1. Write a Verso module or declaration doc.
2. Open a heading on the same line as the /-! or the /--.
3. Open a lower-level heading on a line below.

Expected behavior: The lower-level heading is nested below the first heading.

Actual behavior: An error, as if the first heading is not recognized.

Versions

Lean 4.27.0-rc1 (Mathlib, MacOS / Darwin Kernel Version 23.6.0 / arm64), Lean 4.28.0-nightly-2026-01-19 (Lean4web nightly)

Additional Information

n/a.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.