Lean/Lake binaries are not installed in this sandbox; the project is provided ready for external lake build.
