fix: enforce proper meta discipline for Verso docstring extensions (#13808)

This PR enforces that Verso docstring extensions should always be meta
at attribute application time, giving better error messages, and ensures
that the generated argument parser helper is also meta and has the same
visibility.

src/Lean/Elab/DocString.lean

@@ -604,7 +604,8 @@ private def genWrapper (declName : Name) (argType : Option Expr) (retType : Expr
     let parserTy ← inferType parser
     let name ← mkFreshUserName (declName ++ `getArgs)
     let name := declName ++ `getArgs
-    addAndCompile <| .defnDecl {
+    let isMeta := isMarkedMeta (← getEnv) declName
+    addAndCompile (markMeta := isMeta) <| .defnDecl {
       name
       levelParams := []
       type := parserTy
@@ -803,11 +804,20 @@ builtin_initialize registerBuiltinAttribute {
       throwError "{.ofConstName decl} is not defined"
 }
 
+/--
+In module mode, docstring extensions are invoked at elaboration time, so the underlying definition
+must be marked `meta`.
+-/
+private def checkDocExtMeta (decl : Name) (kind : String) : CoreM Unit := do
+  if (← getEnv).header.isModule && !isMarkedMeta (← getEnv) decl then
+    throwError m!"`{.ofConstName decl}` must be marked `meta` to be used as a docstring {kind}"
+
 builtin_initialize registerBuiltinAttribute {
   name := `doc_role
   descr := "docstring role expander"
   applicationTime := .afterCompilation
   add := fun decl stx kind => do
+    checkDocExtMeta decl "role"
     let roleName ←
       if let `(attr|doc_role $x) := stx then
         realizeGlobalConstNoOverloadWithInfo x
@@ -859,6 +869,7 @@ builtin_initialize registerBuiltinAttribute {
   descr := "docstring code block expander"
   applicationTime := .afterCompilation
   add := fun decl stx kind => do
+    checkDocExtMeta decl "code block"
     let blockName ←
       if let `(attr|doc_code_block $x) := stx then
         realizeGlobalConstNoOverloadWithInfo x
@@ -968,6 +979,7 @@ builtin_initialize registerBuiltinAttribute {
   descr := "docstring directive expander"
   applicationTime := .afterCompilation
   add := fun decl stx kind => do
+    checkDocExtMeta decl "directive"
     let directiveName ←
       if let `(attr|doc_directive $x) := stx then
         realizeGlobalConstNoOverloadWithInfo x
@@ -1021,6 +1033,7 @@ builtin_initialize registerBuiltinAttribute {
   descr := "docstring command expander"
   applicationTime := .afterCompilation
   add := fun decl stx kind => do
+    checkDocExtMeta decl "command"
     let commandName ←
       if let `(attr|doc_command $x) := stx then
         realizeGlobalConstNoOverloadWithInfo x

tests/elab/versoDocsModule.lean

@@ -0,0 +1,162 @@
+module
+
+public import Lean
+
+/-!
+This file tests that custom Verso docstring extensions work in `module`s. The `@[doc_role]`,
+`@[doc_code_block]`, `@[doc_directive]`, and `@[doc_command]` attributes should:
+
+1. Enforce that the underlying definition is `meta` (since it is used during elaboration).
+
+2. Work correctly. In particular, they should generate the `getArgs` wrapper as `meta`.
+-/
+
+set_option doc.verso true
+
+open Lean Doc Elab Term
+
+@[doc_role]
+meta def r (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+
+@[doc_code_block]
+meta def c (s : StrLit) : DocM (Block ElabInline ElabBlock) :=
+  pure (Block.code (s.getString.toList.reverse |> String.ofList))
+
+@[doc_directive]
+meta def d (s : TSyntaxArray `block) : DocM (Block ElabInline ElabBlock) := do
+  .concat <$> s.reverse.mapM elabBlock
+
+@[doc_command]
+meta def cmd (_ : Ident) : DocM (Block ElabInline ElabBlock) := do
+  return .empty
+
+/-- Uses the custom role: {r}`role here` -/
+def useRole := ()
+
+open Lean Elab Command in
+/-- info: Uses the custom role: -/
+#guard_msgs in
+#eval show CommandElabM Unit from do
+  IO.print (← findDocString? (← getEnv) ``useRole).get!
+
+/--
+Uses the custom code block:
+
+```c
+hello
+```
+-/
+def useCodeBlock := ()
+
+open Lean Elab Command in
+/--
+info: Uses the custom code block:
+
+```
+
+olleh
+```
+-/
+#guard_msgs in
+#eval show CommandElabM Unit from do
+  IO.print (← findDocString? (← getEnv) ``useCodeBlock).get!
+
+/--
+Uses the custom directive:
+
+:::d
+
+text
+
+:::
+-/
+def useDirective := ()
+
+open Lean Elab Command in
+/--
+info: Uses the custom directive:
+
+text
+-/
+#guard_msgs in
+#eval show CommandElabM Unit from do
+  IO.print (← findDocString? (← getEnv) ``useDirective).get!
+
+/--
+Uses the custom command:
+
+{cmd Foo}
+-/
+def useCommand := ()
+
+open Lean Elab Command in
+/-- info: Uses the custom command: -/
+#guard_msgs in
+#eval show CommandElabM Unit from do
+  IO.print (← findDocString? (← getEnv) ``useCommand).get!
+
+-- Each attribute should refuse to apply to a definition that is not `meta`, since the generated
+-- `.getArgs` wrapper is invoked at elaboration time.
+
+def notMetaRole (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+
+/-- error: `notMetaRole` must be marked `meta` to be used as a docstring role -/
+#guard_msgs in
+attribute [doc_role] notMetaRole
+
+def notMetaCodeBlock (s : StrLit) : DocM (Block ElabInline ElabBlock) :=
+  pure (Block.code s.getString)
+
+/-- error: `notMetaCodeBlock` must be marked `meta` to be used as a docstring code block -/
+#guard_msgs in
+attribute [doc_code_block] notMetaCodeBlock
+
+def notMetaDirective (s : TSyntaxArray `block) : DocM (Block ElabInline ElabBlock) := do
+  .concat <$> s.mapM elabBlock
+
+/-- error: `notMetaDirective` must be marked `meta` to be used as a docstring directive -/
+#guard_msgs in
+attribute [doc_directive] notMetaDirective
+
+def notMetaCommand (_ : Ident) : DocM (Block ElabInline ElabBlock) := do
+  return .empty
+
+/-- error: `notMetaCommand` must be marked `meta` to be used as a docstring command -/
+#guard_msgs in
+attribute [doc_command] notMetaCommand
+
+-- The generated `getArgs` wrapper should have the same public/private visibility as the
+-- definition it wraps. A private wrapper for a public def would mean the role couldn't be
+-- used from importing modules.
+
+@[doc_role]
+public meta def publicRole (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+
+@[doc_role]
+meta def internalRole (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+
+-- Same again, but applying the attribute as a separate command rather than inline:
+public meta def publicRole' (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+attribute [doc_role] publicRole'
+
+meta def internalRole' (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+attribute [doc_role] internalRole'
+
+/--
+info: publicRole.getArgs       visible publicly: true
+internalRole.getArgs    visible publicly: false
+publicRole'.getArgs     visible publicly: true
+internalRole'.getArgs   visible publicly: false
+-/
+#guard_msgs in
+#eval show Lean.Elab.Command.CommandElabM Unit from withExporting do
+  IO.println s!"publicRole.getArgs       visible publicly: {← hasConst ``publicRole.getArgs}"
+  IO.println s!"internalRole.getArgs    visible publicly: {← hasConst ``internalRole.getArgs}"
+  IO.println s!"publicRole'.getArgs     visible publicly: {← hasConst ``publicRole'.getArgs}"
+  IO.println s!"internalRole'.getArgs   visible publicly: {← hasConst ``internalRole'.getArgs}"