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

@@ -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

tests/pkg/structure_docstrings/StructureDocstrings.lean

@@ -0,0 +1,2 @@
+import StructureDocstrings.A
+import StructureDocstrings.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

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

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

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"]

tests/pkg/structure_docstrings/lean-toolchain

@@ -0,0 +1 @@
+lean4-2

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