From bc9cc05082ed8317395fcfed3e03d783b3f43713 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 14 Nov 2025 12:31:30 +1100
Subject: [PATCH] feat: include current file in default premise selector
 (#11168)

This PR changes the default library suggestions (e.g. for `grind
+suggestions` or `simp_all? +suggestions) to include the theorems from
the current file in addition to the output of Sine Qua Non.
---
 src/Lean/LibrarySuggestions/Default.lean           | 12 +++++++-----
 tests/lean/run/library_suggestions_persistent.lean |  6 +++++-
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/Lean/LibrarySuggestions/Default.lean b/src/Lean/LibrarySuggestions/Default.lean
index e9a192cfb1..976155419d 100644
--- a/src/Lean/LibrarySuggestions/Default.lean
+++ b/src/Lean/LibrarySuggestions/Default.lean
@@ -11,15 +11,17 @@ import all Lean.LibrarySuggestions.SineQuaNon
 /-!
 # Default library suggestions engine
 
-This module sets the default library suggestions engine to Sine Qua Non.
+This module sets the default library suggestions engine to "Sine Qua Non",
+along with the theorems from the current file.
+.
 Any module that imports this (directly or transitively) will have library suggestions enabled.
 -/
 
 namespace Lean.LibrarySuggestions
 
-open Lean LibrarySuggestions SineQuaNon
-
--- Set the default library suggestions engine to Sine Qua Non
-set_library_suggestions Lean.LibrarySuggestions.sineQuaNonSelector
+-- Set the default library suggestions engine to
+-- a combination of "Sine Qua Non" and the theorems from the current file.
+-- For now we just intersperse the results, but in future we should re-rank them.
+set_library_suggestions open Lean.LibrarySuggestions in sineQuaNonSelector.intersperse currentFile
 
 end Lean.LibrarySuggestions
diff --git a/tests/lean/run/library_suggestions_persistent.lean b/tests/lean/run/library_suggestions_persistent.lean
index 602a05ffb0..767cc1863e 100644
--- a/tests/lean/run/library_suggestions_persistent.lean
+++ b/tests/lean/run/library_suggestions_persistent.lean
@@ -13,7 +13,11 @@ already be set from importing Lean.LibrarySuggestions (which imports Default).
 -/
 
 /--
-info: ✓ Selector found in imported state: `Lean.LibrarySuggestions.sineQuaNonSelector
+info: ✓ Selector found in imported state: (Term.open
+ "open"
+ (Command.openSimple [`Lean.LibrarySuggestions])
+ "in"
+ (Term.app `sineQuaNonSelector.intersperse [`currentFile]))
 ---
 info:   ✓ Successfully retrieved selector using getSelector!
 -/