)]}'
{
  "commit": "8b388fe4a29c80de20a06ffe1238586e69b8de14",
  "tree": "135909ac3856e54a3c8c63484ae91e93319388c2",
  "parents": [
    "28b99ec01f6275235fedecbac8e382cac682bf80"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "qim.morrison@gmail.com",
    "time": "Tue Jun 30 22:50:43 2026 +1000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "qim.morrison@gmail.com",
    "time": "Tue Jun 30 22:50:43 2026 +1000"
  },
  "message": "perf: map Array.mapFinIdx/mapIdx in place\n\n`Array.mapFinIdxM` (and hence `mapFinIdx`, `mapIdxM`, `mapIdx`) ran only its\npush-based reference implementation: it reads each element with `as[i]`, a\nborrow that leaves the element shared with the still-live input array. Any\nin-place work the mapping function attempts on an element therefore copies it,\nso a column-style operation that touches one entry of each row of an\n`Array (Array _)` is O(rows * cols) instead of O(rows), and the gap widens\nwithout bound as the rows get wider.\n\nGive `mapFinIdxM` an `@[implemented_by]` unsafe implementation mirroring\n`mapMUnsafe`: it nulls each slot (`uset i default`) before invoking `f`, so on a\nuniquely-owned input each element arrives exclusive (refcount 1) and may be\nmutated in place. The reference body is unchanged, so every lemma about\n`mapFinIdxM` still holds; the `@[inline]` is dropped (kept `@[expose]`) because\ninlining the reference body at call sites would bypass `@[implemented_by]`, just\nas `mapM` is not `@[inline]`.\n\ntests/compile/arrayMapIdxInPlace.lean is a deterministic regression test using\n`dbgTraceIfShared`: before this change the `mapFinIdx`/`mapIdx` cases each\nprinted one \"row shared\" trace per row; now they print none, matching\n`Array.map`.\n\nCo-Authored-By: Claude Opus 4.8 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "3104770cdfad0607acef5d674b5147776c1f41b2",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Array/Basic.lean",
      "new_id": "19aa16e590c7e1f967ce19fa892329037da0926b",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array/Basic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "f69838b6b9db6b946ff38882ea4768a342cff159",
      "new_mode": 33188,
      "new_path": "tests/compile/arrayMapIdxInPlace.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "2784d7cdbf897d2e397a3d807795fc461131e55f",
      "new_mode": 33188,
      "new_path": "tests/compile/arrayMapIdxInPlace.lean.out.expected"
    }
  ]
}