)]}'
{
  "commit": "75fe98fcbd691c4820783d100949dee7dadb39c1",
  "tree": "368107ca3bb2a1735604228bbaf3e9fd966267fa",
  "parents": [
    "137a88d9d363d6f0c60de75d4cef02a26f38962e"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Sep 04 14:52:04 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Sep 04 14:55:20 2026 +0000"
  },
  "message": "perf: let Lean\u0027s allocations skip mimalloc\u0027s free-list scrub\n\nThis PR drops one store from every small allocation by telling mimalloc that Lean initializes an object\u0027s header before the object can be read, worth 0.2% to 0.3% of user instructions on elaboration.\n\n`mi_page_malloc_zero` clears the free-list pointer in a freshly allocated block so that it cannot leak internal data to the caller. That pointer occupies the first word of the block, which for Lean is the object header, and every allocation site writes the header before anything reads it, so the store is dead. `script/mimalloc-lean.patch` puts the scrub behind `MI_BLOCK_SCRUB`, which the runtime\u0027s mimalloc variants set to 0; the guard also keeps `MI_SECURE` builds scrubbing regardless. Upstream once guarded this store with `MI_SECURE` and left the guard behind as a comment, which is what the patch reinstates under a name that states the contract.\n\n```diff\n mov    rcx, [rax]                     ; pop the block\n mov    [rdx+0x8], rcx\n inc    WORD PTR [rdx+0x10]            ; page-\u003eused++\n-mov    QWORD PTR [rax], 0x0           ; scrub the free-list pointer\n mov    WORD PTR [rax+0x4], di         ; m_cs_sz\n```\n\nMeasured by swapping `libleanshared.so` between two full builds, single-threaded with `-DElab.async\u003dfalse` on a pinned core with ASLR disabled: `tests/elab_bench/big_omega.lean` 18.7804G to 18.7402G user instructions (-0.214%), `import Lean` 1.93625G to 1.93010G (-0.318%).\n\nCo-Authored-By: Claude Opus 5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "9956791c3953ead74392c1fc2c0da0fad8386088",
      "old_mode": 33188,
      "old_path": "CMakeLists.txt",
      "new_id": "23f5893a86b8628a5135159856a0bd13af78cfb4",
      "new_mode": 33188,
      "new_path": "CMakeLists.txt"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "2379dceb51ec4ab4007b57147524611b0444a73b",
      "new_mode": 33188,
      "new_path": "script/mimalloc-lean.patch"
    },
    {
      "type": "modify",
      "old_id": "10819279e27910d662a03284c4e263ee9654bf30",
      "old_mode": 33188,
      "old_path": "src/runtime/CMakeLists.txt",
      "new_id": "cb55c3a2b10073b6e9f149292c5535810552192d",
      "new_mode": 33188,
      "new_path": "src/runtime/CMakeLists.txt"
    }
  ]
}