)]}'
{
  "commit": "6dac9ea9ab351afa4990195ccf4cbe79be57525c",
  "tree": "73aeba97713d22bc61f60d146359ceb5d20c4ad8",
  "parents": [
    "ba9237e196e4f6fa353c605230d81b7d9582d49f"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Oct 30 05:46:51 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Oct 30 05:46:51 2026 +0000"
  },
  "message": "perf: make kernel reduction of `String.toList` linear\n\nThis PR makes kernel reduction of `String.toList` on a string literal take time linear in its length. Previously, `decide +kernel` on `s.toList.length \u003d 400` took about 8 s, and long literals hit the kernel\u0027s recursion limit.\n\n`String.toList` is now defined with `String.Internal.utf8DecodeList`, a structurally recursive UTF-8 decoder on `List UInt8`. It replaces `ByteArray.utf8Decode?`, whose `size`, indexing and `push` operations each walk a list in the kernel. `List.utf8Encode` now wraps the encoded byte list directly instead of building it with one `ByteArray.push` per byte. It is `noncomputable`, so compiled code is unchanged. Proofs that unfold `List.utf8Encode` should use the new `List.utf8Encode_eq_toByteArray`.\n\nCloses #16012\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "add2f81d9402b49b01398995b04e8d9d96b8d5a3",
      "old_mode": 33188,
      "old_path": "src/Init/Data/ByteArray/Bootstrap.lean",
      "new_id": "13407ed2d3433918d79a696f8e610ffb63ae6c1e",
      "new_mode": 33188,
      "new_path": "src/Init/Data/ByteArray/Bootstrap.lean"
    },
    {
      "type": "modify",
      "old_id": "0bbdcf6d280fa5a11dd54d7e9825720d928b44af",
      "old_mode": 33188,
      "old_path": "src/Init/Data/String/Basic.lean",
      "new_id": "07d0282cdd6b9467a15014484d5386b66bcbcde9",
      "new_mode": 33188,
      "new_path": "src/Init/Data/String/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "54c88fab830bd902fa147fc487eb0798fcaef08e",
      "old_mode": 33188,
      "old_path": "src/Init/Data/String/Bootstrap.lean",
      "new_id": "d91f59071a6962568bbfc07e125b087ed8ea724f",
      "new_mode": 33188,
      "new_path": "src/Init/Data/String/Bootstrap.lean"
    },
    {
      "type": "modify",
      "old_id": "f3ef45909f52664ca7cb832d9bdcb7923df9362b",
      "old_mode": 33188,
      "old_path": "src/Init/Data/String/Decode.lean",
      "new_id": "f01a255782d269d1441dd60e35ae870255ed4a6e",
      "new_mode": 33188,
      "new_path": "src/Init/Data/String/Decode.lean"
    },
    {
      "type": "modify",
      "old_id": "a2b8d95135427cc5d4089408f9a381debabc94d8",
      "old_mode": 33188,
      "old_path": "src/Init/Data/String/Defs.lean",
      "new_id": "ddc8e217cc0d72220adf6920d02964a5839d2c4f",
      "new_mode": 33188,
      "new_path": "src/Init/Data/String/Defs.lean"
    },
    {
      "type": "modify",
      "old_id": "dbd74d2063d97cfe111e6d4db5a8177d7166df7e",
      "old_mode": 33188,
      "old_path": "src/Init/Data/String/Lemmas/Decode.lean",
      "new_id": "e08b5b79f47c844bb631ea47f0883383daa245b3",
      "new_mode": 33188,
      "new_path": "src/Init/Data/String/Lemmas/Decode.lean"
    },
    {
      "type": "modify",
      "old_id": "3c36e834f0af30f09e498733f0d82a12ba717a67",
      "old_mode": 33188,
      "old_path": "src/Init/Data/String/Length.lean",
      "new_id": "81f7c3cc7910ee73ad49c5cce27e709db7afde46",
      "new_mode": 33188,
      "new_path": "src/Init/Data/String/Length.lean"
    },
    {
      "type": "modify",
      "old_id": "2c81501c437a1ed436f9cab99c9d68da0d7434dc",
      "old_mode": 33188,
      "old_path": "src/Init/Prelude.lean",
      "new_id": "b3526375cdff521c6db57f846437f9a932304cac",
      "new_mode": 33188,
      "new_path": "src/Init/Prelude.lean"
    },
    {
      "type": "modify",
      "old_id": "a10eec3ad30642df8eabe27a680df8ba13f65c83",
      "old_mode": 33188,
      "old_path": "src/Std/Http/Data/URI/Encoding.lean",
      "new_id": "bc929e7512def5797508cf92e37547dcb7f156ac",
      "new_mode": 33188,
      "new_path": "src/Std/Http/Data/URI/Encoding.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "cbb18b74af225e4678d2dbd32a0c59953d2a5a51",
      "new_mode": 33188,
      "new_path": "tests/elab/issue16012.lean"
    }
  ]
}