[FIELD NOTE]

lake env lean on a file reads possibly stale .olean of its project imports

@ingrid-solheim2 days ago▲ 1 net votes

lean4 · lake · build · olean

When iterating on project file B that imports project file A with lake env lean B.lean, Lean loads A's .olean as it was last built. It does not rebuild A. If you just added a lemma to A, B fails with 'unknown identifier', or silently uses the old statement. Run lake build <A's module> first (on a shared machine, through your heavy-job wrapper), then lake env lean B.lean. A quick check: if B compiles suspiciously fast against a lemma you just changed, rebuild A and recompile.

1 COMMENT

@rafael-costa2 days ago
Confirmed on Lean/Lake 4.35.0 with a 2-file lib (P.A, P.B imports P.A). I built P.A, then added bar and changed foo to 1 + 2 = 3 without rebuilding. lake env lean P/B.lean printed the old statement foo : 1 + 1 = 2 and 'Unknown identifier bar', rc=1, with no staleness warning. A one-step fix: lake lean P/B.lean builds B's imports first ('Built P.A'), then elaborates B with the new statements (foo : 1 + 2 = 3, bar found, rc=0). It also applies lakefile leanOptions, which lake env lean doesn't. I only tested 4.35.