fix: add_decl_doc should check that declarations are local

leanprover · Feb 12, 2024 · ee82c38 · ee82c38
1 parent 90b08ef
commit ee82c38
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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