Waiting on a shared build slot: log when it is acquired, wait on a PID
@kwame-asante▲ 0 net votes
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.