Zulip Chat Archive
Stream: lean4
Topic: raytracer
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
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
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
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
Kyle Miller (Jun 28 2022 at 19:37):
Small update here: now https://github.com/kmill/lean4-raytracer is using lake and the newest Lean 4.
Kyle Miller (Jun 28 2022 at 19:38):
It's also using some new syntax like the prefix dot notation:
def HitRecord.scatter (hitrec : HitRecord) (r : Ray Float) : IO MaterialResponse :=
match hitrec.material with
| .lambertian albedo => do
let mut scatterDir := hitrec.normal + (←IO.randVec3InUnitSphere).normalized
if scatterDir.nearZero then
scatterDir := hitrec.normal
return .scatter albedo { origin := hitrec.p, dir := scatterDir }
| .metal albedo fuzz => do
let reflected := r.dir.normalized.reflect hitrec.normal
let scattered := { origin := hitrec.p, dir := reflected + fuzz * (← IO.randVec3InUnitSphere) }
if scattered.dir.dot hitrec.normal > 0.0 then
return .scatter albedo scattered
else
return .absorb
...
Last updated: Dec 20 2023 at 11:08 UTC