)]}'
{
  "commit": "40b4acced91c2f9a022acd3044935cfa346c3c25",
  "tree": "920e109c7841ce6d80cc44226a13c3d45cb9de75",
  "parents": [
    "712a0e42e09378ebc9a2b63b371f223eec289ebd"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 01:31:58 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 01:31:58 2026 +0000"
  },
  "message": "perf: bound expression comparisons in the type inference cache\n\nThis PR fixes quadratic elaboration behavior for large string-literal equalities by limiting structural expression comparisons in the type inference cache.\n",
  "tree_diff": [
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "88195e1803ce6f56acabe521ce1d74f2c0a741c4",
      "new_mode": 33188,
      "new_path": "src/Lean/Data/BudgetedCache.lean"
    },
    {
      "type": "modify",
      "old_id": "41889e2ff853265fa01e785420455d1874e9275e",
      "old_mode": 33188,
      "old_path": "src/Lean/Expr.lean",
      "new_id": "86f4a1e0436e629e314cbd18aa7be504d3ca2bc2",
      "new_mode": 33188,
      "new_path": "src/Lean/Expr.lean"
    },
    {
      "type": "modify",
      "old_id": "c1e88217a7ee2f6bc6973bf3e83a6c20aab75923",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Basic.lean",
      "new_id": "9462930d005b1011fd5c4370729e71d31392d9c0",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "0d06228576675f2cdcead38906751d73f2c712b0",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/InferType.lean",
      "new_id": "dea89dd7d4dea4a11831bdd037902c73beb88748",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/InferType.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "e624c79bf49525626421989da22cec485e7ae68c",
      "new_mode": 33188,
      "new_path": "tests/compile/budgetedCache.lean"
    },
    {
      "type": "modify",
      "old_id": "7856b326c460cebbaf7f590c207c6e99d60fc3b7",
      "old_mode": 33188,
      "old_path": "tests/compile/exprBudgetedEq.lean",
      "new_id": "d0c0cca62e7e3d8500f4fab9d5232b41cf5d723b",
      "new_mode": 33188,
      "new_path": "tests/compile/exprBudgetedEq.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "fa90febaaa6da4b928be52b6868fcee6e306f0da",
      "new_mode": 33188,
      "new_path": "tests/elab/budgetedMetaCache.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "24e02c46406bc7204e59289d549d487a38893b93",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/inferTypeCache.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "3787ae87f82feebee03ee060e7b926528725fcd8",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/matcherInferTypeCache.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "1ce0a6d96d7444edc560454547a4299611603fc6",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/stringLiteralDefEq.lean"
    }
  ]
}
