)]}'
{
  "commit": "246e37b0c09115e93a1978efc9bfc31d67659725",
  "tree": "5a46c9203ca75f92a54a191d8316cfab1836d779",
  "parents": [
    "137a88d9d363d6f0c60de75d4cef02a26f38962e"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Sep 04 14:32:44 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Sep 04 14:40:19 2026 +0000"
  },
  "message": "perf: compile the reference-counted deletion machinery with mimalloc\n\nThis PR moves big-object allocation and the reference-counted deletion machinery into the translation unit that compiles mimalloc, so that mimalloc\u0027s fast paths inline into them, worth 0.2% to 0.4% of user instructions on elaboration.\n\n`lean_free_object`, `lean_alloc_object` and the `lean_del_core` deletion loop move from `object.cpp` to a new `object_rc.cpp`, which `mimalloc.cpp` includes rather than compiling on its own; without mimalloc it is built as an ordinary translation unit. `lean_dealloc` moves to `object.h` so both see it, and `deactivate_task` and `deactivate_promise` lose their internal linkage, as `object_rc.cpp` now calls them across translation units.\n\nThe visible effect is on `lean_free_object`, whose per-kind `mi_free_size` calls collapse once mimalloc\u0027s definitions are in scope, since `mi_free_size` is `mi_free` in a release build:\n\n```diff\n-mov    eax, [rdi+0x4]                  ; six-way switch on the object kind,\n-shr    ecx, 0x18                       ; each arm computing a byte size for\n-cmp    ecx, 0x5                        ; mi_free_size\n-ja     \u003cmi_free\u003e\n-jmp    rcx                             ; jump table\n+movzx  eax, BYTE PTR [rdi+0x7]         ; only MPZ still needs its destructor\n+cmp    eax, 0xfa000000\n+jne    \u003cmi_free\u003e\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.7812G to 18.7407G user instructions (-0.215%), `import Lean` 1.93569G to 1.92795G (-0.400%).\n\nThe compiled benchmarks that stress constructor churn are unaffected, at 0.000% on `rbmap`, `rbmap_fbip`, `hashmap` and `unionfind`. Their hot deletion path is `lean_free_small_object`, which is `static inline` in `lean.h` and so already inlines `mi_free` into compiled code; what this PR reaches is the runtime\u0027s own C++ paths for arrays, strings, closures and big objects, which elaboration exercises and those benchmarks do not.\n\nCo-Authored-By: Claude Opus 5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "10819279e27910d662a03284c4e263ee9654bf30",
      "old_mode": 33188,
      "old_path": "src/runtime/CMakeLists.txt",
      "new_id": "ecedffa506e0eae37ef98a3f52d7870383a36940",
      "new_mode": 33188,
      "new_path": "src/runtime/CMakeLists.txt"
    },
    {
      "type": "modify",
      "old_id": "9a4d944d71115ef0c58e3227081338261369e286",
      "old_mode": 33188,
      "old_path": "src/runtime/mimalloc.cpp",
      "new_id": "db323292a7e8b54a3dcf1c35f60d83e62cfef1cb",
      "new_mode": 33188,
      "new_path": "src/runtime/mimalloc.cpp"
    },
    {
      "type": "modify",
      "old_id": "9954c2c5d77d82fcc6bd50aa2e0591218a41d5f4",
      "old_mode": 33188,
      "old_path": "src/runtime/object.cpp",
      "new_id": "63066c92f29bcf768628f2a3891aa80cb89b3853",
      "new_mode": 33188,
      "new_path": "src/runtime/object.cpp"
    },
    {
      "type": "modify",
      "old_id": "c531919348f4e42d171c99f36061728a5c2f172b",
      "old_mode": 33188,
      "old_path": "src/runtime/object.h",
      "new_id": "57eda37bf09d438534ad6154321b2e7387dabb02",
      "new_mode": 33188,
      "new_path": "src/runtime/object.h"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "85431fb3473c4c77abdbb3233bb30584e464cc59",
      "new_mode": 33188,
      "new_path": "src/runtime/object_rc.cpp"
    }
  ]
}