)]}'
{
  "commit": "8ce42848b22925349104f038f91d2a620bd8e3b2",
  "tree": "324b06e3c2aa77b92b2b1ee5fb89df08100607fa",
  "parents": [
    "2c38bb3306997b999180b7bbd5e3cd8992437fe8"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sat May 16 16:21:46 2026 +1000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon May 18 13:55:26 2026 +0000"
  },
  "message": "feat: filter MePo candidates to theorems and order output by iteration\n\nThis PR refines MePo premise selection so that (1) candidates are restricted\nto theorems, matching the convention already used by `SineQuaNon` and\n`SymbolFrequency`, and (2) the result is ordered lexicographically by\n`(iteration, score)` rather than by score alone.\n\nBefore the theorem filter, `mepoSelector` returned functions, recursors, and\ncasts (e.g. `Int.add`, `Eq.ndrec`, `cast`, `proof_irrel`) alongside real\npremises. With it, those go away and the obvious lemmas — e.g. `Int.add_comm`\nfor `a + b \u003d b + a` — rank well above the remaining noise.\n\nThe `(iteration, score)` ordering preserves the iteration priority of the\noriginal Meng–Paulson MePo: an iter-1 premise scoring 0.6 always ranks above\nan iter-2 premise scoring 1.0, since later iterations score against a strictly\nlarger `relevant` set and a higher threshold, so their raw scores are not\ncomparable.\n\nThanks to Xavier Généreux for the report. Further tuning of the score function\nis tracked in https://github.com/leanprover/lean4/issues/13749.\n\nCo-Authored-By: Claude Opus 4.7 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "b719f59c5940b2a4a65864cd63c1fb1207a752d9",
      "old_mode": 33188,
      "old_path": "src/Lean/LibrarySuggestions/MePo.lean",
      "new_id": "27c499c29f11505d98843c8c398627dba2ce94dd",
      "new_mode": 33188,
      "new_path": "src/Lean/LibrarySuggestions/MePo.lean"
    },
    {
      "type": "modify",
      "old_id": "2e9b988e4342957314bfdc3763123f7fd709d42c",
      "old_mode": 33188,
      "old_path": "tests/elab/library_suggestions_mepo_order.lean",
      "new_id": "e83c1a0ef0ae8bdbb593987fe00a1f5ae69c7222",
      "new_mode": 33188,
      "new_path": "tests/elab/library_suggestions_mepo_order.lean"
    },
    {
      "type": "modify",
      "old_id": "bbb4d1c5fba2b2d509e4cd04f2526807b921ed81",
      "old_mode": 33188,
      "old_path": "tests/elab/library_suggestions_mepo_order.lean.out.expected",
      "new_id": "aa752520f4d74751025feb27a1ff0af4fdd667f8",
      "new_mode": 33188,
      "new_path": "tests/elab/library_suggestions_mepo_order.lean.out.expected"
    }
  ]
}