Benchmarks for Lean 4

Stream: lean4

[Agnishom Chattopadhyay]

I am very interested in Lean 4 because it is simultaneously a language which allows for proofs as well as computations with IO.

I remember seeing some performance benchmarks for programs in Lean 4. Can someone point out where I can find these results?

I am also seeing some setup for benchmarks here but I do not know how to run them with my Nix installation. Can anybody tell me what the observed results are? (or give me instructions on how to set up my nix so that I can run these?)

Thanks!

[Agnishom Chattopadhyay]

In particular, I want to see how it does compared to other programming languages including OCaml/Haskell/C++

[Andrew Kent]

It looks like there is a Test Speedcenter Benchmarks portion of the Github Actions workflow -- that may contain some helpful info/examples of how to run things.

[Sebastian Ullrich]

The benchmark suite is originally from https://arxiv.org/pdf/1908.05647.pdf#section.8

[Agnishom Chattopadhyay]

Thanks, this is helpful

[Agnishom Chattopadhyay]

In figure 7, I see in the description that the numbers have been "normalized by the Lean base run time". What does this entail?

[Sebastian Ullrich]

They are divided by the number in the first column (of the base benchmark, in the case of the rbmap_X variations)

[Sebastian Ullrich]

That folder you linked contains a README.md btw