From ee82c3834b73628ec2aa740e58e6cff72a02beac Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 12 Feb 2024 05:16:17 -0500
Subject: [PATCH] fix: `add_decl_doc` should check that declarations are local

---
 src/Lean/Elab/BuiltinCommand.lean   | 2 ++
 tests/lean/docStr.lean              | 3 +++
 tests/lean/docStr.lean.expected.out | 1 +
 3 files changed, 6 insertions(+)

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 5a6b1fb991d6..4d7271f58092 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -722,6 +722,8 @@ opaque elabEval : CommandElab
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
     let declName ← resolveGlobalConstNoOverloadWithInfo id
+    unless ((← getEnv).getModuleIdxFor? declName).isNone do
+      throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`
diff --git a/tests/lean/docStr.lean b/tests/lean/docStr.lean
index 44f710a63eda..61d7ad2629b0 100644
--- a/tests/lean/docStr.lean
+++ b/tests/lean/docStr.lean
@@ -102,3 +102,6 @@ def printRangesTest : MetaM Unit := do
   printRanges `g.foo
 
 #eval printRangesTest
+
+/-- no dice -/
+add_decl_doc Nat.add
diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out
index c6094eae6f50..64dd47866ba5 100644
--- a/tests/lean/docStr.lean.expected.out
+++ b/tests/lean/docStr.lean.expected.out
@@ -189,3 +189,4 @@ g.foo :=
                         charUtf16 := 44,
                         endPos := { line := 42, column := 47 },
                         endCharUtf16 := 47 } }
+docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module