feat: allow Verso syntax for module docs to be controlled separately (#12329)

This PR adds the option `doc.verso.module`. If set, it controls whether
module docstrings use Verso syntax. If not set, it defaults to the value
of the `doc.verso` option.

Closes #12070.

src/Lean/DocString/Extension.lean

@@ -69,6 +69,11 @@ register_builtin_option doc.verso : Bool := {
   descr := "whether to use Verso syntax in docstrings"
 }
 
+register_builtin_option doc.verso.module : Bool := {
+  defValue := false,
+  descr := "whether to use Verso syntax in module docstrings (falls back to `doc.verso` if not set)"
+}
+
 private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
 builtin_initialize docStringExt : MapDeclarationExtension String ←
   mkMapDeclarationExtension

src/Lean/DocString/Parser.lean

@@ -1214,6 +1214,35 @@ Parenthesizer for `ifVerso`—parenthesizes according to the underlying parenthe
 @[combinator_parenthesizer ifVerso, expose]
 public def ifVerso.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p1 <|> p2
 
+/--
+Parses as `ifVerso` if module docs should use Verso syntax, or as `ifNotVerso` otherwise.
+Checks `doc.verso.module` if explicitly set, otherwise falls back to `doc.verso`.
+-/
+public def ifVersoModuleDocsFn (ifVerso ifNotVerso : ParserFn) : ParserFn := fun c s =>
+  let useVerso :=
+    if c.options.contains `doc.verso.module then
+      c.options.getBool `doc.verso.module
+    else
+      c.options.getBool `doc.verso
+  if useVerso then ifVerso c s
+  else ifNotVerso c s
+
+@[inherit_doc ifVersoModuleDocsFn]
+public def ifVersoModuleDocs (ifVerso ifNotVerso : Parser) : Parser where
+  fn := ifVersoModuleDocsFn ifVerso.fn ifNotVerso.fn
+
+/--
+Formatter for `ifVersoModuleDocs`—formats according to the underlying formatters.
+-/
+@[combinator_formatter ifVersoModuleDocs, expose]
+public def ifVersoModuleDocs.formatter (f1 f2 : Formatter) : Formatter := f1 <|> f2
+
+/--
+Parenthesizer for `ifVersoModuleDocs`—parenthesizes according to the underlying parenthesizers.
+-/
+@[combinator_parenthesizer ifVersoModuleDocs, expose]
+public def ifVersoModuleDocs.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p1 <|> p2
+
 /--
 Disables the option `doc.verso` while running a parser.
 -/

src/Lean/Parser/Command.lean

@@ -56,7 +56,7 @@ multiple times in the same file.
 -/
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
-  "/-!" >> Doc.Parser.ifVerso versoCommentBody commentBody >> ppLine
+  "/-!" >> Doc.Parser.ifVersoModuleDocs versoCommentBody commentBody >> ppLine
 
 
 def namedPrio := leading_parser

tests/lean/run/versoDocModuleDeclOnly.lean

@@ -0,0 +1,45 @@
+/-
+Tests that `doc.verso.module false` disables Verso for module docs
+while `doc.verso true` keeps declaration docs as Verso.
+-/
+import Lean
+
+-- Module docs use Markdown, declaration docs use Verso
+set_option doc.verso true
+set_option doc.verso.module false
+
+/-!
+This is a plain Markdown module doc with `code` and **bold**.
+
+Verso syntax is {here}**visible**.
+-/
+
+open Lean Elab Term in
+/--
+info: Markdown:
+This is a plain Markdown module doc with `code` and **bold**.
+
+Verso syntax is {here}**visible**.
+
+Verso:
+-/
+#guard_msgs in
+#eval show TermElabM Unit from do
+  IO.println "Markdown:"
+  for modDoc in (Lean.getMainModuleDoc (← getEnv)).toArray do
+    IO.println modDoc.doc
+  IO.println "Verso:"
+  for modDoc in (Lean.getMainVersoModuleDocs (← getEnv)).snippets do
+    IO.println <| repr modDoc
+
+/--
+{name}`versoDecl`
+-/
+def versoDecl := "hello"
+
+-- This would show the Verso syntax if it were interpreted as Markdown
+open Lean Elab Term in
+/-- info: `versoDecl` -/
+#guard_msgs in
+#eval show TermElabM Unit from do
+  (← findDocString? (← getEnv) ``versoDecl).forM (IO.println ·)

tests/lean/run/versoDocModuleFallback.lean

@@ -0,0 +1,55 @@
+/-
+Tests that when `doc.verso.module` is not explicitly set,
+module docs fall back to the value of `doc.verso`.
+-/
+import Lean
+
+-- Only set doc.verso, do not set doc.verso.module
+set_option doc.verso true
+
+/-!
+Module docs should parse as Verso here (fallback from {option}`doc.verso`).
+
+*Bold* and _italic_ and [link](example.com)
+-/
+
+open Lean Elab Term in
+/--
+info: Markdown:
+Verso:
+{ text := #[Lean.Doc.Block.para
+              #[Lean.Doc.Inline.text "Module docs should parse as Verso here (fallback from ",
+                Lean.Doc.Inline.other
+                  { name := `Lean.Doc.Data.Option val := Dynamic.mk `Lean.Doc.Data.Option _ }
+                  #[Lean.Doc.Inline.code "doc.verso"],
+                Lean.Doc.Inline.text ")."],
+            Lean.Doc.Block.para
+              #[Lean.Doc.Inline.bold #[Lean.Doc.Inline.text "Bold"], Lean.Doc.Inline.text " and ",
+                Lean.Doc.Inline.emph #[Lean.Doc.Inline.text "italic"], Lean.Doc.Inline.text " and ",
+                Lean.Doc.Inline.link #[Lean.Doc.Inline.text "link"] "example.com", Lean.Doc.Inline.linebreak "\n"]],
+  sections := #[],
+  declarationRange := { pos := { line := 10, column := 0 },
+                        charUtf16 := 0,
+                        endPos := { line := 14, column := 2 },
+                        endCharUtf16 := 2 } }
+-/
+#guard_msgs in
+#eval show TermElabM Unit from do
+  IO.println "Markdown:"
+  for modDoc in (Lean.getMainModuleDoc (← getEnv)).toArray do
+    IO.println modDoc.doc
+  IO.println "Verso:"
+  for modDoc in (Lean.getMainVersoModuleDocs (← getEnv)).snippets do
+    IO.println <| repr modDoc
+
+
+/--
+{name}`fallbackDecl`
+-/
+def fallbackDecl := "hello"
+
+open Lean Elab Command Term in
+/-- info: `fallbackDecl` -/
+#guard_msgs in
+#eval show TermElabM Unit from do
+  (← findDocString? (← getEnv) ``fallbackDecl).forM (IO.println ·)

tests/lean/run/versoDocModuleVersoOnly.lean

@@ -0,0 +1,49 @@
+/-
+Tests that `doc.verso.module` can independently enable Verso syntax for module docs
+while keeping declaration docs as Markdown.
+-/
+import Lean
+
+-- Module docs use Verso, declaration docs use Markdown
+set_option doc.verso.module true
+set_option doc.verso false
+
+/-!
+Module docs should parse as Verso here.
+
+*Bold* and _italic_ and [link](example.com)
+-/
+
+open Lean Elab Term in
+/--
+info: Markdown:
+Verso:
+{ text := #[Lean.Doc.Block.para #[Lean.Doc.Inline.text "Module docs should parse as Verso here."],
+            Lean.Doc.Block.para
+              #[Lean.Doc.Inline.bold #[Lean.Doc.Inline.text "Bold"], Lean.Doc.Inline.text " and ",
+                Lean.Doc.Inline.emph #[Lean.Doc.Inline.text "italic"], Lean.Doc.Inline.text " and ",
+                Lean.Doc.Inline.link #[Lean.Doc.Inline.text "link"] "example.com", Lean.Doc.Inline.linebreak "\n"]],
+  sections := #[],
+  declarationRange := { pos := { line := 11, column := 0 },
+                        charUtf16 := 0,
+                        endPos := { line := 15, column := 2 },
+                        endCharUtf16 := 2 } }
+-/
+#guard_msgs in
+#eval show TermElabM Unit from do
+  IO.println "Markdown:"
+  for modDoc in (Lean.getMainModuleDoc (← getEnv)).toArray do
+    IO.println modDoc.doc
+  IO.println "Verso:"
+  for modDoc in (Lean.getMainVersoModuleDocs (← getEnv)).snippets do
+    IO.println <| repr modDoc
+
+
+/-- This is a plain Markdown docstring with {nonVerso}`code` and **bold**. -/
+def plainMarkdown := "hello"
+
+open Lean Elab Command Term in
+/-- info: "This is a plain Markdown docstring with {nonVerso}`code` and **bold**. " -/
+#guard_msgs in
+#eval show TermElabM Unit from do
+  (← findDocString? (← getEnv) ``plainMarkdown).forM (IO.println ·.quote)