box for benchmarking

Stream: lean4

[Arthur Paulino]

Is there something in core like box (as defined below) for benchmarking purposes?

@[never_extract] def box (_ : α) : Unit := ()

I want to call functions and ignore their returns, but I don't want their calls to be simplified away

[Aaron Liu]

Maybe docs#dbgTrace

[Arthur Paulino]

That would pollute stdout. I'm fine with box as I implemented above. I was just wondering if core already had something for this specific purpose.

[Aaron Liu]

Here's a list of all constants that are marked @[never_extract]:

• outOfBounds
• sorryAx
• panicWithPos
• panic
• dbgTraceIfShared
• panicWithPosWithDecl
• dbgStackTrace
• panicCore
• dbgTrace

[Mario Carneiro]

I usually just implement box on the fly exactly like that

[Mario Carneiro]

actually you probably want to have an opaque identity function, not a unit function

[Mario Carneiro]

unit functions are frequently (always?) deleted

[Arthur Paulino]

Even with never_extract?

[Arthur Paulino]

I can test it later. I still haven't had the chance

[Mario Carneiro]

Arthur Paulino said:

Even with never_extract?

never_extract turns off closed term extraction, meaning that if you have box 1 then this will not be lifted to a top level definition even though it's a closed term. It does not actually change the execution semantics, and lean still does optimizations that would be legal for any pure function. If you want to avoid something getting optimized out it needs to be placed in the data flow, which is why things like dbgTrace have a callback.

[Sam Burnham]

I tried a similar approach to prevent function optimization when benchmarking the Fibonacci function, but unless I mark fib itself with never_extract the benchmark time is constant around 170ns. This occurs even for inputs like fib 45 which clearly take several seconds to run. How can I place the result in the data flow or otherwise create a black box wrapper function?

@[never_extract]
def blackBox : α → α := id

-- Copy of  `dbgTrace` logic
set_option linter.unusedVariables.funArgs false in
@[never_extract]
def blackBox' (s : String) (f : Unit → α) : α := f ()

--@[never_extract]
def fib (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | 1 => 1
  | n' + 2 => fib (n' + 1) + fib (n')

def main : IO Unit := do
  let start ← IO.monoNanosNow
  let result := blackBox fib 40
  --let result := blackBox' "" (fun _ => fib) 40 -- This also doesn't work
  let finish ← IO.monoNanosNow
  let diff := Float.ofNat (finish - start) / 1000000000
  IO.println s!"Fib result: {result}"
  IO.println s!"Time: {diff}s"

[Robin Arnez]

It still inlines blackBox; you need to use noinline

[Sam Burnham]

That works! Thank you

[Simon Dima]

See also this issue on benchmarking pure functions I opened last week