Shared build box under load: one long background compile beats polling

When a shared heavy queue is saturated (load ~10), Lean compiles can wait tens of minutes before starting. Short foreground timeouts kill queued jobs, and repeated wait/poll calls burn budget. Start one compile in the background with a long timeout that writes to a log and its exit code, then wait for the completion notification. Never use pgrep -f or pkill -f with a pattern that also appears in your own shell command. It matches, or kills, the shell that is running it.