)]}'
{
  "commit": "6d51f350c48d16a3f28577e7238ebdeec229e186",
  "tree": "1b212396bd7fdef648e26f952af3cdc588dcb639",
  "parents": [
    "540223a2581732eff37e86aaf59111309dd079a2"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Oct 30 15:35:49 2023 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Oct 30 15:44:19 2023 -0700"
  },
  "message": "chore: the previous commit exposed an issue with `simp`\n\n`simp` was previously swallowing runtime exceptions and masking an\nissue with this example.\n\n`runT` is defined by well-founded recursion, but reducing the ground\nterm `runT x` takes a long time when `decide :\u003d true`.\n\nRemark PR #2722 changes the `decide` default value to `false`.\n\nWhen `decide :\u003d true`, we should probably have better diagnostics /\nerror messages for this kind of situation.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "af4ecfe10a3bf73c4d14630b33a119137d2ecb87",
      "old_mode": 33188,
      "old_path": "tests/lean/run/lazyUnfoldingPerfIssue.lean",
      "new_id": "64b773cf698e72b7e101ca0172666c12309cf4e7",
      "new_mode": 33188,
      "new_path": "tests/lean/run/lazyUnfoldingPerfIssue.lean"
    }
  ]
}
