The execution of IO actions can cause flaky builds

[gaborcs]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Executing IO actions during the build can result in the build being flaky. For example, take the following code:

/-- info: 0 -/
#guard_msgs in
#eval IO.rand 0 1

Since IO.rand 0 1 can result in either 0 or 1, the assertion will sometimes succeed and sometimes fail.

Context

Flaky tests are a huge problem in the industry for bigger projects. Even the probability of each of your test cases passing is 0.999, the probability of 1000 such test cases all passing is 0.999^1000, which is about 0.368. That means your test suite will only pass about 36.8% of the time, which can really impact the happiness and productivity of a team.

I would argue that flaky builds would be even worse than flaky tests, because in most languages we expect our build system to be stable.

I think Lean is in a unique position to provide an extremely good environment for software verification. The combination of its powerful type system, and the ability to ensure that test suites are not flaky by enforcing purity could provide the best environment of all programming languages. It would be a shame if flaky tests, and especially flaky builds, would ruin the experience.

Steps to Reproduce

See above.

Expected behavior: IO actions shouldn't be executed during the build, because they are non-deterministic.

Versions

4.9.0-nightly-2024-05-17

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[nomeata]

Thanks for your report. The example is of course relatively silly, and the response would be “just don't do that”. But that doesn't seem to address your concern.

It seems you are suggesting that no arbitrary IO must be run during build time, with the goal to prevent any non-deterministic IO. I sympathize, and such a design might make many things easier (caching, incrementality, etc.). But I fear it's not realistic given lean's intentionally very open and extensible design. For example, how would you use an external SAT solver during elaboration then?

All we can do, I fear, is to work hard to keep any and each build time operation deterministic.

[eric-wieser]

To give another example of where IO during build time is desirable; it allows code-generation by reading a json file or similar, and adding declarations to the environment. Of course, reading a deterministic data file and reading /dev/urandom are quite different things, and banning one but not the other in the type system sounds rather awkward.

[gaborcs]

Thank you for the quick responses, those are interesting examples of where IO during build time is desirable. I wonder if these use cases could somehow be supported without allowing arbitrary IO.

Now that I’ve thought about it a bit more, I think there may be issues with allowing arbitrary IO actions that are even more serious than flakiness:

• If you paste some Lean code into VS Code, it will be automatically executed instantly. Same goes for suggestions by GitHub Copilot. That seems dangerous in my opinion.
• If you want to execute an operation such as rm -rf /some/directory, you may have rm -rf / in the editor at some point as you type it. Executing something like that automatically could have pretty disastrous effects.

[nomeata]

The first point is absolutely valid: lean gives no protection against malicious code that can easily own your machine if you build it. This is unfortunate, and needs to be communicated clearly (or, at least, care needs to be taken to not claim the opposite). But again, restricting builds on the type level to only do safe and benign things is hard and not on the roadmap for now.

I don't fully understand the second point. Lean doesn't execute arbitrary IO just because some shell command is somewhere in the source code, and typically you don't write such commands directly where lean is continuously elaborating it. More likely you write some tactic or utility function, and eventually call it during some build or elaboration. Maybe one can construct a case where a partial command is executed… but it seems to be quite a corner case.

[gaborcs]

Okay, I guess allowing arbitrary IO may be the right choice if we consider Lean a research language, as it opens up a lot of options such as the ones you’ve mentioned. I don’t think I’ll be comfortable recommending Lean for production usage in my team, but it could be a good choice for my own small hobby/learning projects if I’m careful. :)

[eric-wieser]

• If you want to execute an operation such as rm -rf /some/directory, you may have rm -rf / in the editor at some point as you type it. Executing something like that automatically could have pretty disastrous effect

you can end up in the situation you describe with

def ohno : IO Unit := do
  IO.FS.removeDir "" -- typing here is dangerous

#eval ohno

though the solution is to avoid using #eval in these cases. This does sound like something it would be nice to protect new users against.

[tydeu]

@eric-wieser Maybe it is worth separating out this specific feature request into its own RFC (either here or on the VSCode extension issue tracker)? For example, something like "request permission before running #eval-like commands in a file in an interactive session").

[leodemoura]

Closing issue with the "closing soon" tag.