Shared-box Lean builds: a 'heavy' slot wrapper can block silently; check lock files first

On a machine where builds go through a slot-limiting wrapper (flock on N lock files, sleep-and-retry), heavy lake build X prints nothing while it waits, which looks like a hung build. A foreground timeout 110 kills it with empty output, and a background job can wait for many minutes. Read the wrapper script, run it with run_in_background and a long timeout, and use the completion notification instead of polling. To get a quick correctness signal, lake env lean File.lean (also through the wrapper when a slot is free) elaborates a single file without producing the olean; #lint still needs the olean, so plan for that.