From c7652413db4673ae400a6f7e08617f592a9dd0e7 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 10 Nov 2025 12:05:01 +1100
Subject: [PATCH] feat: link docstrings for diamond inheritance (#11122)

This PR fixes a problem for structures with diamond inheritance: rather
than copying doc-strings (which are not available unless `.server.olean`
is loaded), we link to them. Adds tests.
---
 src/Lean/Elab/Structure.lean                      |  5 +++--
 .../structure_docstrings/StructureDocstrings.lean |  2 ++
 .../StructureDocstrings/A.lean                    |  9 +++++++++
 .../StructureDocstrings/B.lean                    |  7 +++++++
 .../StructureDocstrings/C.lean                    | 15 +++++++++++++++
 tests/pkg/structure_docstrings/lakefile.toml      | 13 +++++++++++++
 tests/pkg/structure_docstrings/lean-toolchain     |  1 +
 tests/pkg/structure_docstrings/test.sh            |  5 +++++
 8 files changed, 55 insertions(+), 2 deletions(-)
 create mode 100644 tests/pkg/structure_docstrings/StructureDocstrings.lean
 create mode 100644 tests/pkg/structure_docstrings/StructureDocstrings/A.lean
 create mode 100644 tests/pkg/structure_docstrings/StructureDocstrings/B.lean
 create mode 100644 tests/pkg/structure_docstrings/StructureDocstrings/C.lean
 create mode 100644 tests/pkg/structure_docstrings/lakefile.toml
 create mode 100644 tests/pkg/structure_docstrings/lean-toolchain
 create mode 100755 tests/pkg/structure_docstrings/test.sh

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index bf89634050..4bd011bf40 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -10,6 +10,7 @@ public import Lean.Meta.Structure
 public import Lean.Elab.MutualInductive
 import Lean.Linter.Basic
 import Lean.DocString
+import Lean.DocString.Extension
 
 public section
 
@@ -661,8 +662,8 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis
     let mut declName := view.declName ++ fieldName
     if inSubobject?.isNone then
       declName ← applyVisibility (← toModifiers fieldInfo) declName
-      -- No need to validate links because this docstring was already added to the environment previously
-      addDocStringCore' declName (← findDocString? (← getEnv) fieldInfo.projFn)
+      -- Create a link to the parent field's docstring
+      addInheritedDocString declName fieldInfo.projFn
       addDeclarationRangesFromSyntax declName (← getRef)
     checkNotAlreadyDeclared declName
     withLocalDecl fieldName fieldInfo.binderInfo (← reduceFieldProjs fieldType) fun fieldFVar => do
diff --git a/tests/pkg/structure_docstrings/StructureDocstrings.lean b/tests/pkg/structure_docstrings/StructureDocstrings.lean
new file mode 100644
index 0000000000..6680f482eb
--- /dev/null
+++ b/tests/pkg/structure_docstrings/StructureDocstrings.lean
@@ -0,0 +1,2 @@
+import StructureDocstrings.A
+import StructureDocstrings.B
diff --git a/tests/pkg/structure_docstrings/StructureDocstrings/A.lean b/tests/pkg/structure_docstrings/StructureDocstrings/A.lean
new file mode 100644
index 0000000000..9deb4c357b
--- /dev/null
+++ b/tests/pkg/structure_docstrings/StructureDocstrings/A.lean
@@ -0,0 +1,9 @@
+module
+
+public section
+
+class Monoid (M : Type) extends Mul M where
+
+class DivInvMonoid (G : Type) extends Mul G where
+  /-- The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
+  protected zpow : Int → G → G
diff --git a/tests/pkg/structure_docstrings/StructureDocstrings/B.lean b/tests/pkg/structure_docstrings/StructureDocstrings/B.lean
new file mode 100644
index 0000000000..e345be9851
--- /dev/null
+++ b/tests/pkg/structure_docstrings/StructureDocstrings/B.lean
@@ -0,0 +1,7 @@
+module
+
+public import StructureDocstrings.A
+
+public section
+
+class GroupWithZero (G : Type) extends Monoid G, DivInvMonoid G where
diff --git a/tests/pkg/structure_docstrings/StructureDocstrings/C.lean b/tests/pkg/structure_docstrings/StructureDocstrings/C.lean
new file mode 100644
index 0000000000..deee50d349
--- /dev/null
+++ b/tests/pkg/structure_docstrings/StructureDocstrings/C.lean
@@ -0,0 +1,15 @@
+module
+
+import Lean.DocString
+import Lean.Meta.Basic
+public import StructureDocstrings.B
+
+public section
+
+/-- info: The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
+#guard_msgs in
+open Lean in
+run_meta do
+  let env ← getEnv
+  let some r ← Lean.findDocString? env `GroupWithZero.zpow | failure
+  logInfo r
diff --git a/tests/pkg/structure_docstrings/lakefile.toml b/tests/pkg/structure_docstrings/lakefile.toml
new file mode 100644
index 0000000000..4c0b776af5
--- /dev/null
+++ b/tests/pkg/structure_docstrings/lakefile.toml
@@ -0,0 +1,13 @@
+name = "structure_docstrings"
+defaultTargets = ["StructureDocstrings", "StructureDocstringsTest"]
+
+[[lean_lib]]
+name = "StructureDocstrings"
+leanOptions = { experimental.module = true }
+roots = ["StructureDocstrings.A", "StructureDocstrings.B"]
+
+[[lean_lib]]
+name = "StructureDocstringsTest"
+# Elab.inServer to allow docstring tests to access .server level data
+leanOptions = { experimental.module = true, Elab.inServer = true }
+roots = ["StructureDocstrings.C"]
diff --git a/tests/pkg/structure_docstrings/lean-toolchain b/tests/pkg/structure_docstrings/lean-toolchain
new file mode 100644
index 0000000000..acba940092
--- /dev/null
+++ b/tests/pkg/structure_docstrings/lean-toolchain
@@ -0,0 +1 @@
+lean4-2
diff --git a/tests/pkg/structure_docstrings/test.sh b/tests/pkg/structure_docstrings/test.sh
new file mode 100755
index 0000000000..11ed62fb84
--- /dev/null
+++ b/tests/pkg/structure_docstrings/test.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+set -e
+
+rm -rf .lake/build
+LEAN_ABORT_ON_PANIC=1 lake build