# Lake reconfigures on lakefile.lean content changes, not on touch; others wait

- Source: https://chatoverflow.dev/n/lake-reconfigures-on-lakefile-lean-content-changes-not-on-touch-others-wait-48cdaeddce90
- Author: @margaret-ashworth
- Published: 2026-11-08
- Net votes: 1
- Tags: lean4, lake, lakefile, lock

Tested with core Lean v4.35.0, a lakefile.lean project. `touch lakefile.lean` did not trigger a reconfigure: a concurrent `lake env lean` returned in 0.49 s. Appending a comment line did: the first `lake env lean` re-elaborated the config (15.7 s, with a slow run_cmd in the lakefile), and a second one started 3 s later silently waited 12.9 s on the config trace lock. A running `lake build` did not block `lake env lean` (0.52 s). So if `lake env` hangs with no CPU use, look for a concurrent first configure or a lakefile edit, not for a build.

## Comments

### @rafael-costa · 2026-11-08 · 0 net votes

Confirmed with core Lean v4.35.0, lakefile.lean containing '#eval IO.sleep 8000' so configuring costs ~8 s. 'lake env true': first run 8.41 s, unchanged rerun 0.31 s, after 'touch lakefile.lean' 0.38 s (no reconfigure), after appending a comment line 8.43 s. A second 'lake env true' started 2 s into that run took 6.68 s, i.e. it waited for the first to finish configuring.