From bc60b1c19da2260e872e0d34926acf9c1014e557 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 12 Nov 2025 11:58:47 +1100
Subject: [PATCH] fix: don't suggest deprecated theorems (#11146)

This PR fixes a bug in #11125. Added a test this time ...

<!-- CURSOR_SUMMARY -->
---

> [!NOTE]
> Exclude deprecated declarations from library suggestions and add a
test verifying they are filtered out.
>
> - **Library Suggestions**:
> - Update `isDeniedPremise` in `src/Lean/LibrarySuggestions/Basic.lean`
to treat `Lean.Linter.isDeprecated` as denied (`true`), filtering
deprecated constants from suggestions.
> - **Tests**:
> - Add `tests/lean/run/library_suggestions_deprecated.lean` to verify
deprecated theorems (e.g., `deprecatedTheorem`) are not suggested by
`currentFile`, while non-deprecated ones are.
>
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
ef7e546dbcca1893d68b07ed79e592ff97f2ceb4. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->
---
 src/Lean/LibrarySuggestions/Basic.lean        |  2 +-
 .../run/library_suggestions_deprecated.lean   | 26 +++++++++++++++++++
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/library_suggestions_deprecated.lean

diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
index 6080e520d5..0b900ff669 100644
--- a/src/Lean/LibrarySuggestions/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -300,7 +300,7 @@ def isDeniedPremise (env : Environment) (name : Name) : Bool := Id.run do
   if name == ``sorryAx then return true
   if name.isInternalDetail then return true
   if Lean.Meta.isInstanceCore env name then return true
-  if Lean.Linter.isDeprecated env name then return false
+  if Lean.Linter.isDeprecated env name then return true
   if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
   if let some moduleIdx := env.getModuleIdxFor? name then
     let moduleName := env.header.moduleNames[moduleIdx.toNat]!
diff --git a/tests/lean/run/library_suggestions_deprecated.lean b/tests/lean/run/library_suggestions_deprecated.lean
new file mode 100644
index 0000000000..7b1caa6fa0
--- /dev/null
+++ b/tests/lean/run/library_suggestions_deprecated.lean
@@ -0,0 +1,26 @@
+import Lean.LibrarySuggestions.Basic
+
+-- Define a normal theorem that should appear in suggestions
+theorem normalTheorem : True := trivial
+
+-- Define a deprecated theorem that should be filtered out by isDeniedPremise
+@[deprecated "Use normalTheorem instead" (since := "1970-01-01")]
+theorem deprecatedTheorem : True := trivial
+
+-- Another normal theorem to verify filtering is selective
+theorem anotherNormalTheorem : 1 + 1 = 2 := rfl
+
+-- Test the currentFile selector which uses isDeniedPremise to filter
+set_library_suggestions Lean.LibrarySuggestions.currentFile
+
+-- This test verifies that deprecated theorems are filtered out by isDeniedPremise
+-- Expected: deprecatedTheorem should NOT appear in suggestions
+/--
+info: Library suggestions:
+  anotherNormalTheorem
+  normalTheorem
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial