Cache doesn't work if I add a second target

Stream: lean4

[Geoffrey Irving]

I expect I'm making a basic error, but currently when I add a second target the Std and Mathlib caches fail to hit. The cache was working well until I extended my lakefile.lean to look like

import Lake
open Lake DSL

package ray where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`pp.proofs.withType, false⟩,
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩
  ]

require mathlib from git "https://github.com/leanprover-community/mathlib4"

@[default_target]
lean_lib Ray

-- NEW STUFF FOLLOWS

lean_exe gradient_test {
  root := `Ray.Render.GradientTest
}

target png.o pkg : FilePath := do
  let o := pkg.buildDir / "Ray/Render/png.o"
  let src ← inputFile <| pkg.dir / "Ray/Render/png.cc"
  let args := #["-I", (←getLeanIncludeDir).toString, "-I/opt/homebrew/include"]
  buildO "png.cc" o src args #["-fPIC"] "c++" getLeanTrace

extern_lib libray pkg := do
  let name := nameToStaticLib "ray"
  let png ← fetch <| pkg.target ``png.o
  buildStaticLib (pkg.nativeLibDir / name) #[png]

I can still build the default target ray via lake build as normal, but if I do lake build gradient_test it starts building Std on me:

% lake build gradient_test
[992/1561] Compiling Std.Tactic.RCases
[1027/1752] Compiling Std.Data.List.Basic
[1077/1899] Compiling Std.Tactic.LeftRight
[1079/1905] Compiling Std.Tactic.Replace
[1084/1910] Compiling Std.Tactic.Omega.Config
[1083/1910] Compiling Std.Lean.Expr
[1084/1913] Compiling Std.Lean.HashSet
[1085/1946] Compiling Std.Tactic.Omega.LinearCombo
[1086/3043] Compiling Std.Lean.Meta.Simp
[1087/3043] Compiling Std.Tactic.Omega.OmegaM
[1088/3043] Compiling Std.Tactic.NormCast
[1089/3043] Compiling Std.Tactic.Omega.Constraint
[1090/3043] Compiling Std.Data.HashMap.Basic
[1091/3043] Compiling Std.Tactic.Omega.Core
[1092/3043] Compiling Std.Tactic.Omega.Logic
[1093/3043] Compiling Std.Tactic.FalseOrByContra
[1095/3043] Compiling Std.Tactic.Omega.MinNatAbs
[1096/3043] Compiling Std.Tactic.Omega
...

[Mario Carneiro]

that's expected behavior

[Mario Carneiro]

it's not Building std, it's Compiling it

[Geoffrey Irving]

Aha!

[Geoffrey Irving]

Is there a compilation cache as well?

[Mario Carneiro]

no, because it's OS dependent

[Mario Carneiro]

but it's a lot faster than building

[Geoffrey Irving]

I'm going to have computational targets that depend on a huge portion of mathlib.

[Geoffrey Irving]

Ah, I'll just wait then. Thanks!

[Mario Carneiro]

it takes something like 2 minutes to Compile all of mathlib

[Geoffrey Irving]

And...it's done. :)

Apologies for impatience: I was assuming it was going to take ages.

[Geoffrey Irving]

Or at least it hit an error message that's my fault.

[Geoffrey Irving]

Thank you! And now I have a .png image generated from Lean. :)

https://github.com/girving/ray/blob/main/Ray/Render/GradientTest.lean

gradient.png

[Johan Commelin]

Didnt @Kyle Miller write a ray tracer in lean4?

[Geoffrey Irving]

Yes: https://github.com/kmill/lean4-raytracer

[Geoffrey Irving]

(I think without a correctness proof, though.)

[Geoffrey Irving]

(Though correctness proofs are mostly out of reach for ray tracers.)

[Kyle Miller]

For a correctness proof, you could say that the monte carlo simulation converges to the true "rendering equation", i.e., show that (in the limit) this is the image you would see form given the light field for the scene.

[Kyle Miller]

You would take as a given how different kinds of materials scatter and absorb light.

[Geoffrey Irving]

Yes, but I think you can’t actually make that proof work.

[Geoffrey Irving]

It requires knowing numerical errors aren’t systematic.

[Kyle Miller]

I was going to add that you'd prove this for the algorithm with real numbers in place of floats, and then hope that there are no numerics issues :wink:

[Kyle Miller]

It doesn't seem impossible to figure out a way to deal with the numerics, but I have no idea how you'd do it.

[Mario Carneiro]

and also with true random number generators I guess

[Geoffrey Irving]

Actually I think it does work even with numerical issues, in the same way my Mandelbrot renders will work. In each case you can use intervals to show that point estimates are conservative, and then use theory to say something about the integrals. For Mandelbrot renders I can use the Koebe quarter theorem to exactly turn point estimates into intervals, but the integral trick will do the same for ray tracing: it would show that the expectation of the intervals (which is an interval) would contain the rendering equation result.

[Geoffrey Irving]

And then one does an empirical mean and guesses that the interval smallness reflects the expectation being accurate.

[Geoffrey Irving]

Though you might need a maximum radiance bound to make the theoretical result sensibly tight, and this is hard to get in general (maybe you have to add a bit of diffusion to get one of those).

[Geoffrey Irving]

(Without the radiance bound I think the rendering equation isn’t necessarily integrable.)

[Geoffrey Irving]

I guess you can just add integrability to the hypotheses, which seems fine to do.