Control run-time execution of pure functions #8591
Description
Prerequisites
Please put an X between the brackets as you perform the following steps:
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - 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
It would be nice to have a way to guarantee, via function attributes or some other mechanism, that a given pure function call is performed at runtime. For this function call, the compiler would have to, at least,
- not perform constant extraction (or inlining followed by simplification) if the arguments are statically known
- not apply dead code elimination if the result is unused
- pass the C compiler the necessary attributes to make sure that its optimizations do not remove the function call.
Currently this is achievable by using a noinline and never_extract wrapper function to create an IO action, but this behavior may not be stable in future versions of the compiler.
Context
The issue arose when attempting to benchmark pure functions.
Related discussion on Zulip: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Constant.20folding.20and.20code.20elimination.20during.20compilation
Steps to Reproduce
Here is an example demonstrating different behavior of the old and new compiler:
def list_sum (u: Unit) := List.replicate 100_000_000 1 |>.foldl Nat.add 0
@[noinline, never_extract]
def test (u: Unit) := list_sum u
@[noinline]
def discardValue (_ : α) : IO Unit := pure ()
def main: IO Unit := discardValue <| test ()
The above code runs in multiple seconds, as intended, when compiled with the old compiler, but runs near-instantaneously when compiled with the new compiler.
A modified version of the above example currently behaves as intended with both the old and new compilers:
def list_sum (u: Unit) := List.replicate 100_000_000 1 |>.foldl Nat.add 0
@[noinline, never_extract]
def test (u: Unit) := list_sum u
@[noinline]
def opaquePure (x : α) : IO α := pure x
def main: IO Unit := do
let _ <- opaquePure <| test ()
return
Versions
Old compiler: version 4.19.0, x86_64-unknown-linux-gnu, commit 6caaee842e94, Release
New compiler: version 4.21.0-pre, commit 4dd770fc0a9e, Release (state of the new-codegen branch on May 25th, now an orphaned commit)
OS: Arch Linux
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.