Zulip Chat Archive

Stream: lean4

Topic: raytracer


view this post on Zulip Kyle Miller (Jan 31 2021 at 23:48):

Mostly for the fun of it, I followed the Ray Tracing in One Weekend book but in Lean rather than C++. It was overall a pleasant experience -- Lean is a nicely designed functional language!

My code isn't particularly fast (and I wasn't particularly focused on performance), but at least it's easily parallelized.

In case it's interesting, here's the code along with a rendered test image: https://github.com/kmill/lean4-raytracer

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 05:55):

I was browsing the repos tagged with lean4 on GitHub and I stumbled upon another raytracer in Lean 4 by @Reed Mullanix: https://github.com/TOTBWF/lean4-raytrace

view this post on Zulip Reed Mullanix (Feb 07 2021 at 05:57):

The other one is _much_ better than mine! I do like how I implemented images, but beyond that their code doesn't have this abomination:

partial def UInt8.ofFloat (x : Float) : UInt8 :=
  if x >= 255 then 255
  else if x < 0 then 0
  else go 0 255

  where
    go (lo : Nat) (hi : Nat) : UInt8 :=
      let mid := (lo + hi)/2
      if hi <= lo then (UInt8.ofNat $ lo - 1)
      else if x < (Float.ofNat mid) then go lo mid else go (mid + 1) hi

view this post on Zulip Leonardo de Moura (Feb 07 2021 at 22:30):

@Reed Mullanix We have added the following coercions
https://github.com/leanprover/lean4/blob/master/src/Init/Data/Float.lean#L79-L83


Last updated: May 07 2021 at 13:21 UTC