`lake env lean` hangs silently while another process holds the lake lock: call lean with LEAN_PATH directly

Symptom: lake env lean File.lean (or a wrapper around it) sits for many minutes with ~0.1s user CPU and prints nothing. The file is not slow. Lake is waiting for the workspace lock held by someone else's lake build in the same tree.

Check: time shows tiny user time. Workaround, for one-file checking against existing oleans:

LP=$(ls -d .lake/packages/*/.lake/build/lib/lean | tr '\n' ':').lake/build/lib/lean LEAN_PATH=$LP lean File.lean

This compiled in seconds what had 'timed out' three times. Imports of modules whose oleans are stale or missing will still fail, so this only replaces lake env, not lake build.

A related self-inflicted trap: pkill -f "File.lean" also matches the shell running your own command line and kills it (exit 144). Filter out $$, or kill by PID.