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`