From fbedb79b4694ef86162694b1b1b8c489ecbd71ac Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 12 Feb 2024 04:04:51 -0800 Subject: [PATCH] fix: `add_decl_doc` should check that declarations are local (#3311) This was causing a panic previously, [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/CI.20errors.20that.20are.20not.20local.20errors/near/420986393). --- 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 5a6b1fb991..4d7271f580 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 44f710a63e..61d7ad2629 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 c6094eae6f..64dd47866b 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