)]}'
{
  "commit": "71402d1f362138dac8fb99943d15c7685d82d554",
  "tree": "f7b257c9cfda6838996b59c55ce63356fd66dd6d",
  "parents": [
    "cfb13b16890276eeb916998436f2760bca032e31"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Jul 14 20:21:58 2025 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Jul 14 20:34:32 2025 -0700"
  },
  "message": "fix: performance issue when elaborating match-expressions with many literals\n\nThis PR fixes a performance issue that occurs when generating equation\nlemmas for functions that use match-expressions containing several\nliterals. This issue was exposed by #9322 and arises from a combination of factors:\n\n1. Literal values are compiled into a chain of dependent if-then-else expressions.\n2. Dependent if-then-else expressions are significantly more expensive to simplify than regular ones.\n3. The `split` tactic selects a target, splits it, and then invokes `simp` on the resulting subgoals. Moreover, `simp` traverses the entire goal bottom-up and does not stop after reaching the target.\n\nThis PR addresses the issue by introducing a custom simproc that\navoids recursively simplifying nested if-then-else expressions. It\ndoes **not** alter the user-facing behavior of the `split` tactic\nbecause such a change would be highly disruptive. Instead, the PR adds\na new flag, `backward.split` to control the behavior of the\nuser-facing `split` tactic. It is currently set to `true`, i.e., the\nold behavior is still the default one. In a future PR, we should set\nthis flag to `false` by default and begin repairing all affected\nproofs.\n\ncloses #9322\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "7cdd965c696e76c561abbd31f8a93c326b7c7e97",
      "old_mode": 33188,
      "old_path": "src/Init/SimpLemmas.lean",
      "new_id": "5d510b25288631ae8f6826ff275e4ef1a941c1b4",
      "new_mode": 33188,
      "new_path": "src/Init/SimpLemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "f35384f1c1401606a0ec257cb2c43cdac36a78bb",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/PreDefinition/Eqns.lean",
      "new_id": "c979b442a1fdb923299d87b62e4c1e13f0c7314e",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/PreDefinition/Eqns.lean"
    },
    {
      "type": "modify",
      "old_id": "31ba9a5a3b7fac6fc30e04a5f5c828008f5fbf83",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/PreDefinition/Structural/Eqns.lean",
      "new_id": "cc421866ffd5343961fb1d8e16d1ebceb208ae85",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/PreDefinition/Structural/Eqns.lean"
    },
    {
      "type": "modify",
      "old_id": "58ae0838d2333fad43643fcf75db810cd56e1aff",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/PreDefinition/WF/Unfold.lean",
      "new_id": "e951237572030b3bb30956c4c2cfd92cee2b1048",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/PreDefinition/WF/Unfold.lean"
    },
    {
      "type": "modify",
      "old_id": "9b468b4c175e1c3c6590dbf3bcf20f647341283c",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Match/MatchEqs.lean",
      "new_id": "1fcbed018483554bfa317dad45eef76ac5d69285",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Match/MatchEqs.lean"
    },
    {
      "type": "modify",
      "old_id": "845f17558f7bc9e4635f9795867ffb95ac4e9347",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Split.lean",
      "new_id": "3d3f57f0cd3131758acff444b21f13cd016491ff",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Split.lean"
    },
    {
      "type": "modify",
      "old_id": "e8ff6093b2b9c7f48ee1b688cb8845c450fa9dcc",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/SplitIf.lean",
      "new_id": "22e8ff920b101cc670cb07de1ca2c40d5b250928",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/SplitIf.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "e769af84b31e89439d528f3659424e7b3089e746",
      "new_mode": 33188,
      "new_path": "tests/lean/run/9322.lean"
    },
    {
      "type": "modify",
      "old_id": "457b31a551a18b55b8587fd192554e745017ec6d",
      "old_mode": 33188,
      "old_path": "tests/lean/run/splitOrderIssue.lean",
      "new_id": "c06d424751edf1c1cbc42b768c744faefa0d0a92",
      "new_mode": 33188,
      "new_path": "tests/lean/run/splitOrderIssue.lean"
    }
  ]
}