Stream: lean4

Topic: Benchmarks for Lean 4

Agnishom Chattopadhyay (Mar 17 2021 at 19:38):

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 (Mar 17 2021 at 19:45):

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

Andrew Kent (Mar 17 2021 at 20:03):

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 (Mar 17 2021 at 22:04):

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

Agnishom Chattopadhyay (Mar 18 2021 at 13:57):

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 (Mar 18 2021 at 14:02):

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