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