[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.

[siknad]

Compile time evaluation is used in Lean all the time for metaprogramming (e.g. proof automation). Any `IO` can be run there (which allows running external solvers, reading a dataset from disk etc).

Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.