From 385efbbaa786ea48815d8ba44319c9b73b617c5e Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 18 May 2026 05:37:49 +1000
Subject: [PATCH] fix: drop stale `.reverse` in MePo premise selector (#13747)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes the MePo premise selector returning its lowest-scoring
premises instead of its best ones.

Since https://github.com/leanprover/lean4/pull/10917 `mepo` returns
suggestions in score-descending order, but `mepoSelector` still applied
a `.reverse` that predated that change. The `.reverse` flipped the order
to score-ascending, so the subsequent `.take config.maxSuggestions` kept
the `maxSuggestions` worst premises.

Thanks to Xavier Généreux for the report.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 src/Lean/LibrarySuggestions/MePo.lean         |  3 +--
 .../elab/library_suggestions_mepo_order.lean  | 25 +++++++++++++++++++
 ...y_suggestions_mepo_order.lean.out.expected |  1 +
 3 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 tests/elab/library_suggestions_mepo_order.lean
 create mode 100644 tests/elab/library_suggestions_mepo_order.lean.out.expected

diff --git a/src/Lean/LibrarySuggestions/MePo.lean b/src/Lean/LibrarySuggestions/MePo.lean
index b095a091aa..b719f59c59 100644
--- a/src/Lean/LibrarySuggestions/MePo.lean
+++ b/src/Lean/LibrarySuggestions/MePo.lean
@@ -78,6 +78,5 @@ public def mepoSelector (useRarity : Bool) (p : Float := 0.6) (c : Float := 2.4)
     pure <| unweightedScore
   let accept := fun ci => return !isDeniedPremise env ci.name
   let suggestions ← mepo constants score accept config.maxSuggestions p c
-  let suggestions := suggestions
-    |>.reverse  -- we favor constants that appear at the end of `env.constants`
+  -- `mepo` already returns suggestions in score-descending order.
   return suggestions.take config.maxSuggestions
diff --git a/tests/elab/library_suggestions_mepo_order.lean b/tests/elab/library_suggestions_mepo_order.lean
new file mode 100644
index 0000000000..2e9b988e43
--- /dev/null
+++ b/tests/elab/library_suggestions_mepo_order.lean
@@ -0,0 +1,25 @@
+import Lean.LibrarySuggestions.MePo
+
+/-!
+Regression test: the MePo premise selector must return suggestions in
+score-descending order.
+
+A stale `.reverse` in `mepoSelector` (left over from before the selector was
+made score-sorting) flipped the order to score-ascending, so `.take` returned
+the lowest-scoring premises instead of the best ones.
+-/
+
+open Lean Lean.Elab.Tactic Lean.LibrarySuggestions
+
+example (a b : Int) : a + b = b + a := by
+  run_tac do
+    let sel : Selector := mepoSelector (useRarity := false)
+    let s ← sel (← getMainGoal) {}
+    let mut prev? : Option Float := none
+    for x in s do
+      if let some prev := prev? then
+        unless prev ≥ x.score do
+          throwError "MePo suggestions are not score-descending: \
+            score {prev} precedes score {x.score}"
+      prev? := some x.score
+  sorry
diff --git a/tests/elab/library_suggestions_mepo_order.lean.out.expected b/tests/elab/library_suggestions_mepo_order.lean.out.expected
new file mode 100644
index 0000000000..bbb4d1c5fb
--- /dev/null
+++ b/tests/elab/library_suggestions_mepo_order.lean.out.expected
@@ -0,0 +1 @@
+library_suggestions_mepo_order.lean:14:0-14:7: warning: declaration uses `sorry`