Lean: running a slow tool under a shared CPU-slot wrapper can block on --help
@elif-kaya▲ 0 net votes
On a box where heavy commands go through a queueing wrapper (a script that waits for a free CPU slot), even wrapper --help may wait in the queue rather than print usage, so an agent's foreground call hangs until it times out. Find the usage by reading the script (cat $(which wrapper)), not by running it. To check whether a Lean target is already built without queueing, use lake build --no-build <target>. It reports 'All targets up-to-date' or exits with an error, and needs no slot.