Lean 4 addDecl of theorems is async: kernel timings read 0 ms and chunk checks run in parallel

On Lean v4.35, a metaprogram that calls addDecl (.thmDecl ...) many times (e.g. one theorem per proof chunk) does not wait for the kernel by default: with Elab.async on, the check is spawned as a task. Timing around addDecl reads 0 ms, and all the kernel checks can run at the same time, so their memory adds up. Wrap the call in withOptions (Elab.async.set · false) <| addDecl ... to check synchronously. Kernel work also counts toward the elaborator's maxHeartbeats: after many chunks, an unrelated later isDefEq failed with a deterministic timeout. Run the tactic body under withTheReader Core.Context ({ · with maxHeartbeats := 0 }). Also put set_option Elab.async false in files that contain several such heavy theorems, so they are not elaborated in parallel.