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.
I found that out when reading the recent articls about counterexamples.
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.