)]}'
{
  "commit": "a1413b8fa130bb06e75e3ff346880ce6a1b7f268",
  "tree": "3a3a62ef6797813d01dbc66f810fc033376d5e09",
  "parents": [
    "76245b39d128da11c495bc8a42506808ad87b78a"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leonardo@microsoft.com",
    "time": "Sun Jul 03 21:49:45 2022 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leonardo@microsoft.com",
    "time": "Sun Jul 03 21:52:01 2022 -0700"
  },
  "message": "feat: cache failures at `isDefEq`\n\nWe can compile Lean with these changes, but 3 tests are still broken.\nThis cache is used to address a performance issue reported at\n  https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout.20with.20structures/near/288180087\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "ae222e63505365650e46a55ac3506720e8272d24",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/App.lean",
      "new_id": "65535684b3e250d90f07ff9451dc076ef841c895",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/App.lean"
    },
    {
      "type": "modify",
      "old_id": "70afe8586707fb81d712430f5d89062f3ab0d039",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/BuiltinTerm.lean",
      "new_id": "77901fa46962e2516713ba6a5764362c5ed0d5bb",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/BuiltinTerm.lean"
    },
    {
      "type": "modify",
      "old_id": "06d71e02f5d1acc04c6ab570bf3b43263420c0ca",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Match.lean",
      "new_id": "549906a15949d8689f0c3420825680be7a93a2e4",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Match.lean"
    },
    {
      "type": "modify",
      "old_id": "eee16a58418e15f0b83f6cd857408925a42989d2",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/MutualDef.lean",
      "new_id": "7f07b62197e2e4786b59646ecc8b02b7b9465f7c",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/MutualDef.lean"
    },
    {
      "type": "modify",
      "old_id": "4e0855fda89b7f847a8df92706a77b3c9cfd1fc9",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Term.lean",
      "new_id": "47d83db169720a05139f1dd015d498bb2ab431c3",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Term.lean"
    },
    {
      "type": "modify",
      "old_id": "24cb189be17fe2b6c4077a64676b286a836324c8",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Basic.lean",
      "new_id": "2dd67ccc4c2f974527509fa21c0ff3e633873fdf",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "3bc337321719319cf0c9cf2c4092c45b10b0906f",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/CollectMVars.lean",
      "new_id": "8d681dbb68bc5412945b98083ce00225c7beee0f",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/CollectMVars.lean"
    },
    {
      "type": "modify",
      "old_id": "e938946ed21fca2067b5eaea0a166e8fbeecd973",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/DecLevel.lean",
      "new_id": "a3e36db58dc778368895699c763f124cd9b935a7",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/DecLevel.lean"
    },
    {
      "type": "modify",
      "old_id": "0cdb2d2f8c3aa5adb3e512d130a4ccabf598d2bf",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/ExprDefEq.lean",
      "new_id": "24be82cb2038b6536cc4bd0b396f96e122ab52d1",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/ExprDefEq.lean"
    },
    {
      "type": "modify",
      "old_id": "bd2867828a0d0496a0718bd51958b814f9c3571a",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/GeneralizeVars.lean",
      "new_id": "c6dba7af09e6ca2a2899a46bc3754f1cb9ff4ecc",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/GeneralizeVars.lean"
    },
    {
      "type": "modify",
      "old_id": "004ff02b0f73772c79204f9bf299d1449d9c56d3",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/PPGoal.lean",
      "new_id": "5651036fdc710e581967f0c2c595f5083a23e2e3",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/PPGoal.lean"
    },
    {
      "type": "modify",
      "old_id": "c70fb8c5ce84e59ec93c5a2050de45ea84c434cf",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Cases.lean",
      "new_id": "ca312ffd9547325614dec5caabad49ddaf583e9b",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Cases.lean"
    },
    {
      "type": "modify",
      "old_id": "cc9b4a81d311e651de0269232ec458d00ddced53",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Clear.lean",
      "new_id": "4c93c12e49f5b13fae4153583a8d5349cb24e116",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Clear.lean"
    },
    {
      "type": "modify",
      "old_id": "e9421941a32c009ac752a35d37ceeee57cca42a9",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Induction.lean",
      "new_id": "2315e62d63422dbcb114caf3ec228b1e10727764",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Induction.lean"
    },
    {
      "type": "modify",
      "old_id": "944a070f32b1c6239d64578622435d54014c6bd3",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Revert.lean",
      "new_id": "7dacfea3d75966198e5208d5f0ae92730c4b4efb",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Revert.lean"
    },
    {
      "type": "modify",
      "old_id": "3358c13b82194db0460192e65b78ccc6fc080b48",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Subst.lean",
      "new_id": "5b8106bcd473c502e42e93e8da28d1a0c5893d04",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Subst.lean"
    },
    {
      "type": "modify",
      "old_id": "2546d86f42687b5ad4dfdd35c4d089dda51b1ba0",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/WHNF.lean",
      "new_id": "8dd7b25d9532d6209811e4e50852ff55926206fd",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/WHNF.lean"
    },
    {
      "type": "modify",
      "old_id": "ceafb60ddc3b47607547a3c48594a09e07c4a3ac",
      "old_mode": 33188,
      "old_path": "src/Lean/MetavarContext.lean",
      "new_id": "29648aacebe51326784cec710ac0659246e38d9b",
      "new_mode": 33188,
      "new_path": "src/Lean/MetavarContext.lean"
    },
    {
      "type": "modify",
      "old_id": "ecb25bc0167369cb41f1f4f45ed0f549861eb301",
      "old_mode": 33188,
      "old_path": "src/Lean/Server/Rpc/Deriving.lean",
      "new_id": "0906a1969c057e2c49e2a307bf901e934678e240",
      "new_mode": 33188,
      "new_path": "src/Lean/Server/Rpc/Deriving.lean"
    },
    {
      "type": "modify",
      "old_id": "203d26b9ce2af0b65f2b14e6da5c35c9fde244a5",
      "old_mode": 33188,
      "old_path": "src/Lean/Util/OccursCheck.lean",
      "new_id": "e48c0a6e60e46320d164c1c9595896051fd5e14a",
      "new_mode": 33188,
      "new_path": "src/Lean/Util/OccursCheck.lean"
    }
  ]
}