From 1ce05b2a179eac8a902995c0caddc609c0169c49 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 31 Oct 2025 15:48:53 +1100
Subject: [PATCH] feat: library suggestion engine for local theorems (#11030)

This PR adds a library suggestion engine for local theorems. To be
useful, I still need to write more combinators to re-rank and combine
suggestions from multiple engines.

This is stacked on top of #11029.
---
 src/Lean/LibrarySuggestions/Basic.lean        | 16 ++++++++
 tests/lean/run/library_suggestions_local.lean | 39 +++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 tests/lean/run/library_suggestions_local.lean

diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
index c6dcc493fa..f711c54775 100644
--- a/src/Lean/LibrarySuggestions/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -286,6 +286,22 @@ def random (gen : StdGen := ⟨37, 59⟩) : Selector := fun _ cfg => do
       suggestions := suggestions.push { name := name, score := 1.0 / consts.size.toFloat }
   return suggestions
 
+/-- A library suggestion engine that returns locally defined theorems (those in the current file). -/
+def currentFile : Selector := fun _ cfg => do
+  let env ← getEnv
+  let max := cfg.maxSuggestions
+  -- Use map₂ from the staged map, which contains locally defined constants
+  let mut suggestions := #[]
+  for (name, ci) in env.constants.map₂.toList do
+    if suggestions.size >= max then
+      break
+    if isDeniedPremise env name then
+      continue
+    match ci with
+    | .thmInfo _ => suggestions := suggestions.push { name := name, score := 1.0 }
+    | _ => continue
+  return suggestions
+
 builtin_initialize librarySuggestionsExt : EnvExtension (Option Selector) ←
   registerEnvExtension (pure none)
 
diff --git a/tests/lean/run/library_suggestions_local.lean b/tests/lean/run/library_suggestions_local.lean
new file mode 100644
index 0000000000..bbe6a6fe76
--- /dev/null
+++ b/tests/lean/run/library_suggestions_local.lean
@@ -0,0 +1,39 @@
+import Lean.LibrarySuggestions.Basic
+
+-- Define some initial local constants
+def myLocalDef : Nat := 42
+
+theorem myLocalTheorem : myLocalDef = 42 := rfl
+
+-- Add a theorem in the Lean namespace (should be filtered by isDeniedPremise)
+namespace Lean
+theorem shouldBeFiltered : True := trivial
+end Lean
+
+-- Test the currentFile selector (should only show theorems, not definitions)
+set_library_suggestions Lean.LibrarySuggestions.currentFile
+
+-- First test: should show only myLocalTheorem
+-- (not myLocalDef since it's a def, not Lean.shouldBeFiltered since it's in Lean namespace)
+/--
+info: Library suggestions: [myLocalTheorem]
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial
+
+-- Add more local constants (mix of theorems and definitions)
+theorem anotherTheorem : True := trivial
+
+def myFunction (x : Nat) : Nat := x + 1
+
+-- Second test: should show only the two theorems (not myFunction)
+/--
+info: Library suggestions: [anotherTheorem, myLocalTheorem]
+-/
+#guard_msgs in
+example : False → True := by
+  suggestions
+  intro h
+  trivial