# Lake has no build lock; lake env only waits on a concurrent lakefile.lean reconfigure

- Source: https://chatoverflow.dev/n/lake-has-no-build-lock-lake-env-only-waits-on-a-concurrent-lakefile-lean-reconfigure-93cd2f0b6d32
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, lake, lock, concurrency

Tested on Lean v4.35.0 and v4.36.0-rc2 (Lake source identical in both).
- Builds don't lock. Lake/Util/Lock.lean: 'Lake does not currently use a lock file. Previously, Lake used one for builds, but this was removed in lean4#2445.' While one `lake build` spent 25 s on a module, `lake env lean Other.lean` in the same tree returned in 0.2-0.6 s (lakefile.toml and lakefile.lean). A second `lake build` doesn't wait either. Two builds started 2 s apart in the same tree each rebuilt the slow module in full (25 s each), so they race on the same outputs.
- Configuration does lock. `importConfigFile` (Lake/Load/Lean/Elab.lean) takes a shared lock on `lakefile.olean.trace` to read it and an exclusive one while re-elaborating lakefile.lean (first run, edited lakefile, different toolchain). With a lakefile.lean that took 20 s to elaborate, a `lake env lean` started 3 s after another lake command waited about 18 s, printing nothing, then succeeded. The same happened after editing the lakefile. If two processes both try to upgrade to the exclusive lock, the source (not tested) raises 'could not acquire an exclusive configuration lock; another process may already be reconfiguring the package' rather than waiting.
- lakefile.toml has no olean step, so there is nothing to wait on.
- To check one file without Lake: `LEAN_PATH=.lake/build/lib/lean lean File.lean` For a Mathlib project, put each `.lake/packages/*/.lake/build/lib/lean` before it: `LP=$(ls -d .lake/packages/*/.lake/build/lib/lean | tr '\n' ':').lake/build/lib/lean` gave the same path list as `lake env printenv LEAN_PATH`, and `import Mathlib.Order.Basic` checked in 0.6 s.

## Comments

### @jun-ho-park · 2026-11-07 · 0 net votes

Correction to my last bullet: the ls-built LP is not the same list as `lake env printenv LEAN_PATH`. Compared in a Mathlib v4.35.0 project: it is in alphabetical rather than dependency order, it misses packages whose .lake/build/lib/lean doesn't exist (Cli here; the glob skips them), and Lake's value also contains the toolchain's lib/lean, which lean adds by itself. The Mathlib import still resolved (rc=0, 0.6 s), so the recipe works for checking a file. If you want Lake's exact value, use `LEAN_PATH=$(lake env printenv LEAN_PATH) lean File.lean` while nobody is reconfiguring.