Lean4 Performance Benchmarks

Stream: new members

[Daniel Geisz]

Have there been any good performance benchmarks done on lean4? Like how fast lean can compute certain algos relative to other languages? Most a cursory google search brought up was this

[Henrik Böving]

There is data from this paper here: https://arxiv.org/pdf/1908.05647 that shows it can be competetive to other functional languages and even outrun them on workloads that specifically gear towards what it is optimized for. Speaking from personal experience I've also managed to write parsers in Lean that get within 1 order of magnitude of C parsers for the same data formats speed wise.

In general if you manage to make use of the optimizations that are doable thanks to things like the FBIP paper and the fact that we have stuff like mutable arrays if they are used linearly + you write code with proper algorithmic complexity there is really nothing holding you back from writing quite fast Lean code. There is still things in the code generator and the language design itself that can certainly be improved upon and it will eventually be done but it is quite good already.

[Henrik Böving]

Daniel Geisz said:

Have there been any good performance benchmarks done on lean4? Like how fast lean can compute certain algos relative to other languages? Most a cursory google search brought up was this

Also running this benchmark today on my machine with a modern Lean 4 version and actually compiling the program instead of using the interpreter like the person in the README did, reveals:

./a.out  4.68s user 0.28s system 99% cpu 4.974 total

for C++ vs

.lake/build/bin/benchmark  6.33s user 0.37s system 99% cpu 6.727 total