)]}'
{
  "commit": "09ce61cfd1ddfbb1d7a86325d5c934bbbc4c2868",
  "tree": "345ab662bea68db3036d070adedd4529e9aaa79c",
  "parents": [
    "4d0b7cf66c140dd83f8c8634293047335a385026"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jul 02 20:24:32 2024 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jul 02 20:39:33 2024 -0700"
  },
  "message": "feat: safe exponentiation\n\n- Adds configuration option `exponentiation.threshold`\n- An expression `b^n` where `b` and `n` are literals is not reduced by\n  `whnf`, `simp`, and `isDefEq` if `n \u003e exponentiation.threshold`.\n\nMotivation: prevents system from becoming irresponsive.\n\nTODO: improve support in the kernel. It is using a hard-coded limit\nfor now.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "7d23cd9d5ca2206b12008e9605ad535bf9c10780",
      "old_mode": 33188,
      "old_path": "src/Lean/CoreM.lean",
      "new_id": "75eae9b8ad644e92514f439bd4ba145accd580f9",
      "new_mode": 33188,
      "new_path": "src/Lean/CoreM.lean"
    },
    {
      "type": "modify",
      "old_id": "193c311b2711f573892c984d2ba80bd92804d28f",
      "old_mode": 33188,
      "old_path": "src/Lean/Message.lean",
      "new_id": "edbdb59b33af56ec36731d7e57c270e4bb02a22b",
      "new_mode": 33188,
      "new_path": "src/Lean/Message.lean"
    },
    {
      "type": "modify",
      "old_id": "a4940982227f36c4d4ae1a7a102c0ffb58002d39",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Offset.lean",
      "new_id": "b3afaf728a9be9526cd1a9c7ea41f2a722742f8f",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Offset.lean"
    },
    {
      "type": "modify",
      "old_id": "3939a4b49edd6334383a5f320d8c9e5713431ad0",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean",
      "new_id": "930ca1e4a605b4e961fec8d871f1e35fbca6795c",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean"
    },
    {
      "type": "modify",
      "old_id": "23c0d1b90b836868da3e88df8f6574b843989b55",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean",
      "new_id": "2a1a4163fbe0861754809496a3cf39633b517fcd",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean"
    },
    {
      "type": "modify",
      "old_id": "ebd379279b36b3eb4f94be5bd1467f37e239965d",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/WHNF.lean",
      "new_id": "f1c79159346f5f0206a776dd42845692e95be71d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/WHNF.lean"
    },
    {
      "type": "modify",
      "old_id": "9df7ef2f8aa3f2940bcd442f788ef65640fbce10",
      "old_mode": 33188,
      "old_path": "src/Lean/Util.lean",
      "new_id": "dbdfa955345e2adf175d5b3c3d1114a799be228a",
      "new_mode": 33188,
      "new_path": "src/Lean/Util.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "4a402e6e4fa9a32add325ec925584d4952a0d621",
      "new_mode": 33188,
      "new_path": "src/Lean/Util/SafeExponentiation.lean"
    },
    {
      "type": "modify",
      "old_id": "1dbb0819a98ef7b9256a593b6960d0bda1cee81e",
      "old_mode": 33188,
      "old_path": "src/kernel/type_checker.cpp",
      "new_id": "013c960f64c4ef9e738b293587582cd8ad48a4ba",
      "new_mode": 33188,
      "new_path": "src/kernel/type_checker.cpp"
    },
    {
      "type": "modify",
      "old_id": "e281c96474a125adf6fa856d3f36989fe7976f3c",
      "old_mode": 33188,
      "old_path": "src/kernel/type_checker.h",
      "new_id": "3ab2ce643b72d2e85984ddca20da833b5d446e70",
      "new_mode": 33188,
      "new_path": "src/kernel/type_checker.h"
    },
    {
      "type": "modify",
      "old_id": "cb91e6e53cb795f2c99ca1b841c563dd7e003520",
      "old_mode": 33188,
      "old_path": "tests/lean/run/lean_nat_gcd.lean",
      "new_id": "4cb2b4727895ff3cded56e402605977e4b09e932",
      "new_mode": 33188,
      "new_path": "tests/lean/run/lean_nat_gcd.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "ef27868f320511b0162fdf918e07f9c3ebdedf84",
      "new_mode": 33188,
      "new_path": "tests/lean/run/safeExp.lean"
    }
  ]
}