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

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.