From 45df6fcd376e7e66bf179b16e2d6f182a60d3b93 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 15 Oct 2025 11:32:11 +0200 Subject: [PATCH] fix: hovers and docstrings for (co)inductive types (#10738) This PR fixes a regression introduced by #10307, where hovering the name of an inductive type or constructor in its own declaration didn't show the docstring. In the process, a bug in docstring handling for coinductive types was discovered and also fixed. Tests are added to prevent the regression from repeating in the future. --- src/Lean/Elab/MutualInductive.lean | 13 ++- tests/lean/interactive/hover.lean | 40 ++++++++ .../lean/interactive/hover.lean.expected.out | 99 +++++++++++++++++++ 3 files changed, 145 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 819ef56e72..f2ea0b2390 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -1123,7 +1123,6 @@ Term.withoutSavingRecAppSyntax do private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := withElaboratedHeaders vars elabs fun vars elabs rs scopeLevelNames => do let res ← mkInductiveDeclCore addAndFinalizeInductiveDecl vars elabs rs scopeLevelNames - addTermInfoViews <| elabs.map (·.view) return res private def mkAuxConstructions (declNames : Array Name) : TermElabM Unit := do @@ -1147,10 +1146,6 @@ def updateViewWithFunctorName (view : InductiveView) : InductiveView := let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (addFunctorPostfix ctor.declName.getPrefix)}) {view with declName := addFunctorPostfix view.declName, ctors := newCtors} -def updateViewRemovingFunctorName (view : InductiveView) : InductiveView := - let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (removeFunctorPostfix ctor.declName.getPrefix)}) - {view with declName := addFunctorPostfix view.declName, ctors := newCtors} - private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := do let view0 := elabs[0]!.view let ref := view0.ref @@ -1275,9 +1270,11 @@ private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res unless (views.any (·.isCoinductive)) do Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation + -- Term info is added here so that docstrings are maximally available in the environment for hovers + runTermElabM fun _ => Term.withDeclName view0.declName <| withRef ref <| addTermInfoViews views + private def elabInductiveViewsPostprocessingCoinductive (views : Array InductiveView) : CommandElabM Unit := do - let views := views.map updateViewRemovingFunctorName let view0 := views[0]! let ref := view0.ref @@ -1299,6 +1296,9 @@ private def elabInductiveViewsPostprocessingCoinductive (views : Array Inductive unless (views.any (·.isCoinductive)) do Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation + -- Term info is added here so that docstrings are maximally available in the environment for hovers + runTermElabM fun _ => Term.withDeclName view0.declName <| withRef ref <| addTermInfoViews views + def InductiveViewToCoinductiveElab (e : InductiveElabStep1) : CoinductiveElabData where declId := e.view.declId declName := e.view.declName @@ -1321,7 +1321,6 @@ def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Uni elabFlatInductiveViews vars flatElabs discard <| flatElabs.mapM fun e => MetaM.run' do mkSumOfProducts e.view.declName elabCoinductive (flatElabs.map InductiveViewToCoinductiveElab) - addTermInfoViews <| elabs.map (·.view) elabInductiveViewsPostprocessingCoinductive (elabs.map (·.view)) else let res ← runTermElabM fun vars => do diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index 393b13c0a0..86e38a7440 100644 --- a/tests/lean/interactive/hover.lean +++ b/tests/lean/interactive/hover.lean @@ -306,3 +306,43 @@ since it needs the environment with the generated `_eval.match_1` matcher. -/ #eval (default : Nat) matches .succ .. --^ textDocument/hover + +/-- +These are docs +-/ +structure S where + --^ textDocument/hover + /-- So are these -/ + mk :: +--^ textDocument/hover + /-- And these -/ + x : Nat +--^ textDocument/hover + +#check { x := 5 : S } + --^ textDocument/hover + --^ textDocument/hover + +/-- Docs -/ +inductive S' where + --^ textDocument/hover + /-- More docs -/ + | mk (x : Nat) + --^ textDocument/hover + +#check (.mk 5 : S') + --^ textDocument/hover + --^ textDocument/hover + +/-- An infinite sequence -/ +coinductive InfSeq (r : α → α → Prop) : α → Prop where + --^ textDocument/hover + /-- Take a step -/ + | step : r a b → InfSeq r b → InfSeq r a + --^ textDocument/hover + +#check InfSeq + --^ textDocument/hover + +#check InfSeq.step + --^ textDocument/hover diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index f4b9ca9fef..c53cb754c7 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -657,3 +657,102 @@ {"start": {"line": 306, "character": 6}, "end": {"line": 306, "character": 38}}, "contents": {"value": "```lean\nBool\n```", "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 312, "character": 10}} +{"range": + {"start": {"line": 312, "character": 10}, + "end": {"line": 312, "character": 11}}, + "contents": + {"value": "```lean\nS : Type\n```\n***\nThese are docs\n", "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 315, "character": 2}} +{"range": + {"start": {"line": 315, "character": 2}, "end": {"line": 315, "character": 4}}, + "contents": + {"value": "```lean\nS.mk (x : ℕ) : S\n```\n***\nSo are these ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 318, "character": 2}} +{"range": + {"start": {"line": 318, "character": 2}, "end": {"line": 318, "character": 3}}, + "contents": + {"value": "```lean\nS.x (self : S) : ℕ\n```\n***\nAnd these ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 321, "character": 9}} +{"range": + {"start": {"line": 321, "character": 9}, + "end": {"line": 321, "character": 10}}, + "contents": + {"value": "```lean\nx : ℕ\n```\n***\nAnd these ", "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 321, "character": 18}} +{"range": + {"start": {"line": 321, "character": 18}, + "end": {"line": 321, "character": 19}}, + "contents": + {"value": "```lean\nS : Type\n```\n***\nThese are docs\n", "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 326, "character": 10}} +{"range": + {"start": {"line": 326, "character": 10}, + "end": {"line": 326, "character": 12}}, + "contents": + {"value": "```lean\nS' : Type\n```\n***\nDocs ", "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 329, "character": 4}} +{"range": + {"start": {"line": 329, "character": 4}, "end": {"line": 329, "character": 6}}, + "contents": + {"value": "```lean\nS'.mk (x : ℕ) : S'\n```\n***\nMore docs ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 332, "character": 9}} +{"range": + {"start": {"line": 332, "character": 8}, + "end": {"line": 332, "character": 11}}, + "contents": + {"value": "```lean\nS'.mk (x : ℕ) : S'\n```\n***\nMore docs ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 332, "character": 16}} +{"range": + {"start": {"line": 332, "character": 16}, + "end": {"line": 332, "character": 18}}, + "contents": + {"value": "```lean\nS' : Type\n```\n***\nDocs ", "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 337, "character": 12}} +{"range": + {"start": {"line": 337, "character": 12}, + "end": {"line": 337, "character": 18}}, + "contents": + {"value": + "```lean\nInfSeq.{u_1} {α : Sort u_1} (r : α → α → Prop) : α → Prop\n```\n***\nAn infinite sequence ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 340, "character": 7}} +{"range": + {"start": {"line": 340, "character": 4}, "end": {"line": 340, "character": 8}}, + "contents": + {"value": + "```lean\nInfSeq.step.{u_1} {α : Sort u_1} (r : α → α → Prop) {a b : α} : r a b → InfSeq r b → InfSeq r a\n```\n***\nTake a step ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 343, "character": 7}} +{"range": + {"start": {"line": 343, "character": 7}, + "end": {"line": 343, "character": 13}}, + "contents": + {"value": + "```lean\nInfSeq.{u_1} {α : Sort u_1} (r : α → α → Prop) : α → Prop\n```\n***\nAn infinite sequence ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///hover.lean"}, + "position": {"line": 346, "character": 7}} +{"range": + {"start": {"line": 346, "character": 7}, + "end": {"line": 346, "character": 18}}, + "contents": + {"value": + "```lean\nInfSeq.step.{u_1} {α : Sort u_1} (r : α → α → Prop) {a b : α} : r a b → InfSeq r b → InfSeq r a\n```\n***\nTake a step ", + "kind": "markdown"}}