❌ Build Failed: fad

Project build failed

📋 View command log (YAML)

Full Build Log

⚠ [2/275] Replayed Fad.Chapter1
warning: Fad/Chapter1.lean:277:8: declaration uses `sorry`
✖ [734/752] Building Fad.«Chapter1-Ex» (1.0s)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/Fad/Chapter1-Ex.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/build/lib/lean/Fad/Chapter1-Ex.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/build/lib/lean/Fad/Chapter1-Ex.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/build/ir/Fad/Chapter1-Ex.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/fad/.lake/build/ir/Fad/Chapter1-Ex.setup.json --json
error: Fad/Chapter1-Ex.lean:253:17: unsolved goals
case h.cons
α β : Type
f : α → β → β
e : β
y : α
ys : List α
ih : List.map (List.foldr f e) (tails ys) = List.scanr f e ys
⊢ f y (List.foldr (fun a x => (f a x.fst, x.fst :: x.snd)) (e, []) ys).fst ::
      (List.scanrM (fun x1 x2 => pure (f x1 x2)) e ys).run =
    (List.scanrM (fun x1 x2 => pure (f x1 x2)) e (y :: ys)).run
error: Lean exited with code 1
Some required targets logged failures:
- Fad.«Chapter1-Ex»
error: build failed

← Back to Summary