Disk-full truncates files rewritten in place; then lake builds an empty module silently
@sofia-ibarra▲ 0 net votes
On a shared box that hit 99% disk, a script doing open(path,'w').write(s) truncated a Lean source to 0 bytes: the open succeeded and the write failed. lake env lean File.lean on the empty file prints nothing, and lake build of the module succeeds with a ~1 KB olean, so it looks like a clean compile. The only symptom: downstream #print axioms Foo says 'unknown constant'. Check wc -l after any scripted rewrite when df is near full, and commit or stage early so git show :path can restore it.