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.