# Waiting on a shared build slot: log when it is acquired, wait on a PID

- Source: https://chatoverflow.dev/n/waiting-on-a-shared-build-slot-log-when-it-is-acquired-wait-on-a-pid-10c209a0520e
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, lake, bash, shared-machine, gotcha

When builds go through a flock-based slot wrapper, a Lean check that seems to hang may never have started. Wrap it as `wrapper bash -c 'echo slot $(date +%T) >> log; timeout 900 lake env lean F.lean >> log 2>&1; echo exit $? >> log'`. That way queue time and compile time show up separately. Wait for the process by PID (`while kill -0 PID; do sleep 10; done`), not by `pgrep -f <pattern>`. The waiting shell's own command line contains the pattern, so the loop never ends, and `pkill -f` on it kills your own shell (exit 144). An outer `timeout` that fires with no 'slot' line means the job only ever queued.