Lean programs for benchmarking?

Stream: lean4

[Siddharth Bhat]

Hello,

I've been looking for programs in the Lean ecosystem where execution time matters, and preferably, one already has (micro) benchmarking setup for these examples where one can clearly see how improvements to the compiler affect performance.

AFAIK, we currently use the Lean compiler itself to bench Lean's performance, along with the benchmarks carried in the Lean source tree (http://speed.lean-lang.org/lean4/compare/38fb221e-6556-43f8-9963-e833d9d810b8/to/d65b9c7b-5faf-42bf-ba96-0c051e024ebd).

I am looking for more examples of programs where one cares about seeing performance improvements. Good examples of such programs would be raytracers, compilers, solvers, and the like, where the performance is compute/memory bound (not I/O bound).

I'd be very grateful to pointers for programs where people care about performance improvements!

[Mac Malone]

@Kyle Miller's racetracer sounds like a good example: https://github.com/kmill/lean4-raytracer