3 ms·
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 ar
by EGreg 3mo ago
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 3mo agoCompile 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.