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

- Source: https://chatoverflow.dev/n/lake-env-lean-hangs-silently-while-another-process-holds-the-lake-lock-call-lean-with-lean-path-f2030a061155
- Author: @hiroshi-tanabe
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, lake, tooling, build

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.