)]}'
{
  "commit": "3f81d317b02e8791f92c344d0a450bfc30a71955",
  "tree": "c3fb653063f825bc5c61c3a59d35b86a64e065fb",
  "parents": [
    "64219ac91e2930d3950637317c7dc4f7b45568d1"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jul 22 16:10:08 2025 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jul 22 18:30:05 2025 -0700"
  },
  "message": "fix: improve `evalInt?`\n\nThis PR improves the `evalInt?` function, which is used to evaluate\nconfiguration parameters from the `ToInt` type class.\nThis PR also adds a new `evalNat?` function for handling the `IsCharP`\ntype class, and introduces a configuration option:\n```\ngrind (exp :\u003d \u003cnum\u003e)\n```\nThis option controls the maximum exponent size considered during\nexpression evaluation. Previously, `evalInt?` used `whnf`,\nwhich could run out of stack space when reducing terms such as `2^1024`.\n\ncloses #9427\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "812032509469c3269877a8925ba192208f0b1bca",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Tactics.lean",
      "new_id": "506583021bf68044388da86387b2dce36f3bc46a",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Tactics.lean"
    },
    {
      "type": "modify",
      "old_id": "2f663d55224056ea6731715c8a90028f769cbb02",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean",
      "new_id": "57bbcca9cee27e18339f3bad5eb358dd6debf135",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "d1f01f3f538d20fd6cb2dbc4ada5438ad1d6f013",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean"
    },
    {
      "type": "modify",
      "old_id": "e6761a72785e019d7c88429c61e0ad7633cbcfe2",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Insts.lean",
      "new_id": "aaacc95af5e21e2a2043c94d7b228be185647e95",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Insts.lean"
    },
    {
      "type": "modify",
      "old_id": "5d19556379dcc07b057b0d4e901e9fe26baa8c6f",
      "old_mode": 33188,
      "old_path": "src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean",
      "new_id": "41a7f4454931edd2fcaf8972afb96f964667c2e9",
      "new_mode": 33188,
      "new_path": "src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean"
    },
    {
      "type": "modify",
      "old_id": "79a0e58eddae8d9204ad48029c570bc7c84302ad",
      "old_mode": 33188,
      "old_path": "stage0/src/stdlib_flags.h",
      "new_id": "9fe80e1247d51130693fe3481b26c0d4c7b7a075",
      "new_mode": 33188,
      "new_path": "stage0/src/stdlib_flags.h"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "0c7daa561cb5e9757348767d4c31b1df0b2b22a8",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_9427.lean"
    }
  ]
}