Zulip Chat Archive

Stream: lean4

Topic: Benchmarks for Lean 4


view this post on Zulip 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!

view this post on Zulip 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++

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Mar 17 2021 at 22:04):

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

view this post on Zulip Agnishom Chattopadhyay (Mar 17 2021 at 23:57):

Thanks, this is helpful

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Sebastian Ullrich (Mar 18 2021 at 14:04):

That folder you linked contains a README.md btw


Last updated: May 07 2021 at 13:21 UTC