Lake compile scheduler can overcommit Lean worker pools on large import graphs, causing macOS SoC watchdog resets

Lake compile scheduler can overcommit Lean worker pools on large import graphs, causing macOS SoC watchdog resets

Prerequisites

• Searched existing Lean issues for similar Lake/build scheduler resource
  pressure reports.
• Reduced to a minimal self-contained public reproducer without Mathlib or
  Batteries.
  • Not yet. The current evidence comes from a large private Lean project and
    repeated live minimization is risky because the failure mode is a full
    system reboot.
• Tested against latest nightly.
  • Not yet. I can test a safe reproducer when available, but I do not want to
    run crash-finding clean builds on this workstation as the detector.

Description

On an Apple Mac Studio M3 Ultra system with 32 CPU cores and 512 GB unified
memory, lake build of a large Lean project repeatedly caused hard macOS
reboots. This is not a low-memory workstation. The macOS panic report does not
point at a normal Lean exception; it reports:

Unexpected SoC (system) watchdog reset occurred after panic diagnostics were completed
notes: missing stackshot buffer or size

I instrumented a local Lean/Lake 4.29.0-rc8 checkout and found the useful
failure signal in Lake's compile scheduling, not in the panic report.

Lake schedules external Lean compiler processes. Each Lean compiler process can
also use an internal worker pool. On this machine Lean's default worker count is
32. For large imported environments, the actual pressure is closer to:

active Lean compiler processes
* Lean child worker threads
* imported environment size

The repeated reboot envelope involved high-import Lean modules being compiled
with full j32 child workers, sometimes overlapping other high-import compiler
children. A local Lake pressure scheduler that accounts for imported artifact
count and child worker count prevents the recorded crash shapes and completed
clean-cache rebuilds.

I understand userspace should not be able to reboot macOS; Apple likely owns
the kernel/SoC watchdog failure. This issue is about whether Lake can avoid
creating a pathological resource-pressure shape in the first place.

Environment

macOS 26.2 (25C56)
Darwin Kernel Version 25.2.0
Machine: Mac Studio, Mac15,14
Chip: Apple M3 Ultra
CPU cores / Lean default worker count observed: 32
Unified memory: 512 GB
hw.memsize: 549755813888 bytes (512 GiB)
Lean: 4.29.0-rc8, commit 513160ea59dfd60defec325636bbc5215a8a6e7e
Lake: 5.0.0-src+513160e
Target project lean-toolchain: leanprover/lean4:v4.29.0-rc8

Full environment details are attached in
environment/environment.txt.

Observed Crash Evidence

Crash sample 1

panic: /Library/Logs/DiagnosticReports/panic-base-2026-05-17-092041.panic
panicString: Unexpected SoC (system) watchdog reset occurred after panic diagnostics were completed

Persisted active compiler pressure:

QuarterLagPairSquareDominanceSource.lean: 8272 imports * j32 = 264704
KPillarAngularSourceFinalAssembly.lean:   3323 imports * j32 = 106336
total active pressure:                   371040

Crash sample 2

panic: /Library/Logs/DiagnosticReports/panic-base-2026-05-17-093718.panic

Persisted active compiler pressure:

KPillarZeroFiberReflectionResidual.lean:   3319 imports * j32 = 106208
QuarterLagPairSquareDominanceSource.lean: 8272 imports * j27 = 223344
total active pressure:                    329552

Crash sample 3

panic: /Library/Logs/DiagnosticReports/panic-base-2026-05-17-095534.panic

Persisted active compiler pressure:

QuarterLagAngleCloseSqrtProductAssembly.lean: 8271 imports * j23 = 190233
KPillarZeroFiberReflectionClassifier.lean:    3320 imports * j32 = 106240
KPillarAngularSourceZeroFiberBridge.lean:     3322 imports * j1  = 3322
total active pressure:                        299795

Crash sample 4

panic: /Library/Logs/DiagnosticReports/panic-base-2026-05-17-111345.panic

Persisted active compiler pressure:

QuarterLagPairSquareDominanceSource.lean: 8272 imports * j32 = 264704

This sample disproved my earlier hypothesis that the problem was only
heavy/peer overlap. Full-thread admission of one extremely heavy imported
environment also appears unsafe on this machine.

Crash sample 5: direct Lean bypass

panic: /Library/Logs/DiagnosticReports/panic-base-2026-05-17-120846.000.panic

The crash-window process sample showed a manual/direct Lean command, not a
normal lake build compile action:

/Users/fieldriser/.elan/toolchains/fielddiag-4.29.0-rc8/bin/lake env lean \
  CascadeLiftReflection/CascadeTwinClosure/CascadeFourier/QuarterLagPairSquareDominanceSource.lean

child:
  lean CascadeLiftReflection/CascadeTwinClosure/CascadeFourier/QuarterLagPairSquareDominanceSource.lean

That selected the patched toolchain but bypassed the patched Lake build
scheduler. With no explicit -j, raw Lean defaulted to j32, recreating the
known-bad single-heavy shape:

QuarterLagPairSquareDominanceSource.lean: 8272 imports * j32 = 264704

Local Mitigation

I patched Lake locally to record and enforce a live pressure ledger for Lean
compiler children. The local policy that passed repeated clean-cache rebuilds:

LAKE_LEAN_IMPORT_THRESHOLD=0
LAKE_LEAN_PRESSURE_LIMIT=400000
LAKE_LEAN_HEAVY_IMPORT_THRESHOLD=8271
LAKE_LEAN_PEER_IMPORT_THRESHOLD=3319
LAKE_LEAN_HEAVY_CHILD_THREADS=10

Behavior:

• every nonzero-import Lean compile is tracked;
• ordinary modules keep normal/adaptive parallelism under the pressure ledger;
• 8271+ import modules are capped to j10;
• 8271+ import modules do not overlap active 3319+ import peer modules;
• 3319+ peer modules do not start while an 8271+ import module is active.

This is a diagnostic/operational mitigation, not necessarily the right final
upstream design.

After crash sample 5, I also wrapped the local toolchain's bin/lean around
the original binary at bin/lean.real. Direct/manual .lean invocations under
cascade_lift_reflection now get -j10 injected unless the command already
passes an explicit -j or is a normal lake build child. This closes the
lake env lean FILE.lean bypass without globally serializing ordinary
lake build.

Successful Validation

After clearing .lake/build and the pressure ledger:

/usr/bin/time -p lake build
Build completed successfully (8366 jobs).
real 284.72
user 354.73
sys 405.64

Successful run pressure summary:

pressure rows: 443
active ledger after completion: empty
max active pressure: 399994
max admitted aggregate worker threads: 121
max per-child worker threads: 32
pressure adjustments: 25
structural heavy/peer block events: 10

Critical successful entries:

QuarterLagAngleCloseSqrtProductAssembly.lean
  requested: 8271 imports * j32 = 264672
  blocked:   structural_incoming_heavy_with_active_peer
  active peers while blocked: 3319, 3322, 3323, 3329 imports
  admitted:  8271 imports * j10 = 82710
  exit:      0

QuarterLagPairSquareDominanceSource.lean
  requested: 8272 imports * j32 = 264704
  admitted:  8272 imports * j10 = 82720
  exit:      0

CascadeLiftReflection.lean
  requested: 8349 imports * j32 = 267168
  admitted:  8349 imports * j10 = 83490
  exit:      0

This mitigation is not a global serial build. Ordinary modules still admit
full j32 Lean children when the live pressure ledger has room; the successful
timed clean build reached 121 aggregate admitted worker threads. The policy
only throttles the recorded high-risk envelope: 8271+ import modules are
limited to j10, and those modules are prevented from overlapping active
3319+ import peers. The result was a clean-cache build in 284.72s, not the
multi-hour behavior seen under conservative fail-closed policies.

Expected Behavior

Lake should avoid scheduling external Lean compiler children in a way that
multiplies into unexpectedly high internal Lean worker pressure on large import
graphs. At minimum, there should be a documented way to make Lake account for
Lean child worker count and imported environment size.

Actual Behavior

Default Lake scheduling can allow multiple large imported Lean modules to run
as independent external processes while each process uses its own internal
worker pool. On this machine, the resulting pressure shape repeatedly triggered
macOS SoC watchdog resets.

Attached Material

The attached zip includes:

• full local incident report;
• local fix log;
• macOS panic reports;
• pressure ledgers for failed and successful runs;
• direct Lean wrapper and guard log for the lake env lean bypass;
• local Actions.lean diagnostic patch and unified diff from upstream commit
  513160ea59dfd60defec325636bbc5215a8a6e7e;
• environment details.

Requested Guidance

Would the Lean maintainers be open to a Lake-side resource-aware compile
scheduler or pressure-budget mechanism for Lean compiler children?

If yes, I can help move from this local diagnostic patch toward a smaller
upstreamable design. I expect that design should include a safer test/reproducer
than my private project, because the current full reproducer can reboot macOS.

Start by reviewing the attached local Actions.lean diagnostic patch and its unified diff, then compare its behavior with the documented lake build and bin/lean wrapper paths. Done should be a smaller upstreamable Lake scheduling design with a safe reproducer and tests or validation that demonstrate bounded worker pressure without relying on system reboots.