Simple raytracer in Lean 4
Lean 4 is a dependently typed programming language, and it can be used both as a proof assistant and for practical programs.
This repository implements the ray tracer described in Ray Tracing in One Weekend.
The raytracer uses Tasks to render in parallel. Part of a raytracer is using supersampling
to better estimate the amount of light entering each pixel, so it is trivial to parallelize:
the entire image is rendered multiple times, and the results are averaged together.
(10 minutes with 8 threads on an Intel Xeon E5-2665. 500x333 pixels, 80 total samples per pixel, max depth 30.)
(2 hours with 16 threads on an Intel Xeon E5-2665. 800x533 pixels, 480 total samples per pixel, max depth 50.)
Running the code
Assuming you already have Lean 4 setup, this builds an executable and runs it:
$ leanpkg build build/bin/render && time ./build/bin/render test.ppm
The rendering settings are hard-coded in writeTestImage in render.lean.
(Note: I was told that you might need to leanmake bin PKG=render before building.)
C benchmark
The c folder contains an implementation of the raytracer in C, hand translated from Lean using C idioms.
This is not a fair comparison because I spent almost no time thinking about optimizing the Lean version, and the only purpose here is to get some idea of the relative speed of my Lean code to see if I made any horrible mistakes.
The first test image in C took 20 seconds with the same configuration, and the second test image took 3 minutes 30 seconds with the same configuration. This means my Lean program takes about 32x as long to run as the C version.
The optimize-lean branch has a more optimized version of the Lean code, and it runs in about 25% less time (so 7.5 minutes for the first test configuration).