)]}'
{
  "commit": "7d948b2763e1677d5d9a5d752d993176e99212fc",
  "tree": "a64b0a366d6f570401182221db8d9e29c41d469a",
  "parents": [
    "b390ed1414d22d8111e7e30f455ad9e525b28e1c"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Jan 02 15:35:08 2025 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Jan 02 15:40:50 2025 -0800"
  },
  "message": "feat: add user-defined fallback procedure for the `grind` tactic\n\nThis PR introduces support for user-defined fallback code in the\n`grind` tactic. The fallback code can be utilized to inspect the state\nof failing `grind` subgoals and/or invoke user-defined\nautomation. Users can now write `grind on_failure \u003ccode\u003e`, where\n`\u003ccode\u003e` should have the type `GoalM Unit`. See the modified tests in\nthis PR for examples.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "bdc6bea97107ac1f46902e58b349b94a6b2a1e6b",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Tactics.lean",
      "new_id": "1554e8b0a4667f537310a6b059849b1166e8c130",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Tactics.lean"
    },
    {
      "type": "modify",
      "old_id": "774c6c055185924441916483df254fb631a1e8b2",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind.lean",
      "new_id": "b9a62e4baed7163b4960a6e6699273364deffe28",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind.lean"
    },
    {
      "type": "modify",
      "old_id": "da2f202c8fd4b9149d6f763c58c61dd31dacc788",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Main.lean",
      "new_id": "77a7b4ffa7bf1aefd6f359baa05ff71e1ef8e233",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Main.lean"
    },
    {
      "type": "modify",
      "old_id": "0a3329915afd33c4896d99036e98f460c35a4297",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "5ac73e6c4dff7a5a23e88274db117a40ee8e40f4",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "modify",
      "old_id": "ddbadb62f5e9fa8d228f09c346d52f0831587180",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_canon_insts.lean",
      "new_id": "c38feabfc8fa020df0b3259d38c4595396075dd2",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_canon_insts.lean"
    },
    {
      "type": "modify",
      "old_id": "ec956e8f61c02e9ccd67d93b220eb40adc399bd2",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_canon_types.lean",
      "new_id": "08a1e17276a760a2135ec5b00bd6daa627e6c22a",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_canon_types.lean"
    },
    {
      "type": "modify",
      "old_id": "f981018a26a312cfebf7b0796e771423962bed3a",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_congr.lean",
      "new_id": "1589785ef00f75187dbd5de1f6be3cff78577cbf",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_congr.lean"
    },
    {
      "type": "modify",
      "old_id": "5f9825eadab2e18d101441d655848c78debedd85",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_many_eqs.lean",
      "new_id": "25c254917c1b972459bc23fc4761c2cc1a49d298",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_many_eqs.lean"
    },
    {
      "type": "modify",
      "old_id": "bee9020b60e57d748e5bf24b9887aaa0be23272c",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_nested_proofs.lean",
      "new_id": "04b32f7fe7420713cd286e6adfe807007f5c3157",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_nested_proofs.lean"
    },
    {
      "type": "modify",
      "old_id": "aa29284c8fa3f7af096bf91c6ba88aa79783718c",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_norm_levels.lean",
      "new_id": "354b56319dd219c7e1e2564f38272216f27e4e89",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_norm_levels.lean"
    },
    {
      "type": "modify",
      "old_id": "66cc3add7adfd313ac8db9027303947ab9d33fdd",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_propagate_connectives.lean",
      "new_id": "e4f4a020dc688e16734c2c0a14f1e692445fc2a9",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_propagate_connectives.lean"
    }
  ]
}