)]}'
{
  "commit": "771a3e668f6f0892c5bfd91f78e4dac03c5be801",
  "tree": "cf814ad6b768bd380c9f1e00c9aed0e94fb51831",
  "parents": [
    "e3a5369bd7705e732d571319a7d3513ba9a70a63"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Oct 20 17:13:32 2025 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Oct 20 17:15:27 2025 -0700"
  },
  "message": "feat: improve `done` tactic in `grind` interactive mode\n\nThis PR improves the `done` tactic in `grind` interactive mode. It now\ndisplays the `grind` state diagnostics for all unsolved subgoals.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "2885f6a1d420f9f503304a438389bfa7d1962927",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Basic.lean",
      "new_id": "60d4d270883d73caf9b3220651bbd153527c64ec",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "b1aabd06fc8540249d63822495ee0185379d0265",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_interactive.lean",
      "new_id": "6fc110ba5a597c51b790cb31561348a250e70347",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_interactive.lean"
    }
  ]
}