Comment by EGreg

Why does Lean always have a way to mess up your file system, writing to any files, rather than just proving proofs?

I found that out when reading the recent articls about counterexamples.