✖ [3055/3514] Building LeanByExample.Option.SkipKernelTC (1.6s)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Option/SkipKernelTC.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Option/SkipKernelTC.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Option/SkipKernelTC.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Option/SkipKernelTC.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Option/SkipKernelTC.setup.json --json
error: LeanByExample/Option/SkipKernelTC.lean:46:55: Unknown constant `USize.thmDecl`
Note: Inferred this name from the expected resulting type of `.thmDecl`:
USize
error: LeanByExample/Option/SkipKernelTC.lean:47:6: Type mismatch
Except.ok env
has type
Except ?m.12 ?m.11
but is expected to have type
Option IO.CancelToken → Except Kernel.Exception Environment
error: LeanByExample/Option/SkipKernelTC.lean:53:8: Unknown identifier `bad_proof₂.elim`
info: LeanByExample/Option/SkipKernelTC.lean:57:0: 'easy_proof₂' depends on axioms: [sorryAx]
error: LeanByExample/Option/SkipKernelTC.lean:56:0: ❌️ Docstring on `#guard_msgs` does not match generated message:
- info: 'easy_proof₂' does not depend on any axioms
+ info: 'easy_proof₂' depends on axioms: [sorryAx]
error: Lean exited with code 1
✖ [3561/3564] Building LeanByExample.TypeClass.BEq (575ms)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/TypeClass/BEq.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/TypeClass/BEq.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/TypeClass/BEq.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/TypeClass/BEq.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/TypeClass/BEq.setup.json --json
info: LeanByExample/TypeClass/BEq.lean:52:0: inferInstance : DecidableEq Float
error: LeanByExample/TypeClass/BEq.lean:52:0: unexpected success
error: Lean exited with code 1
✖ [3562/3564] Building LeanByExample.Diagnostic.Whnf (991ms)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Diagnostic/Whnf.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Diagnostic/Whnf.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Diagnostic/Whnf.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Diagnostic/Whnf.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Diagnostic/Whnf.setup.json --json
info: LeanByExample/Diagnostic/Whnf.lean:75:0: @[instance_reducible] def instManyFunctor : Functor Many :=
inferInstance
error: LeanByExample/Diagnostic/Whnf.lean:74:0: ❌️ Docstring on `#guard_msgs` does not match generated message:
- info: @[implicit_reducible] def instManyFunctor : Functor Many :=
+ info: @[instance_reducible] def instManyFunctor : Functor Many :=
inferInstance
error: Lean exited with code 1
✖ [3563/3564] Building LeanByExample.EXTRA.SelectionSort (1.2s)
trace: .> LEAN_PATH=/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mdgen/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/EXTRA/SelectionSort.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/EXTRA/SelectionSort.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/EXTRA/SelectionSort.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/EXTRA/SelectionSort.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/EXTRA/SelectionSort.setup.json --json
info: LeanByExample/EXTRA/SelectionSort.lean:23:19: failed to synthesize instance of type class
Std.IsLinearOrder α
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
error: LeanByExample/EXTRA/SelectionSort.lean:89:16: `grind` failed
case grind.1.2.1.2.2.1
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
inst_2 : DecidableEq α
inst_3 : Std.IsLinearPreorder α
head : α
tail : List α
h : ¬(head :: tail).minFirst ~ head :: tail
w : α
h_2 : ¬count w (head :: tail).minFirst = count w (head :: tail)
h_3 : -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
h_4 : ¬-1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
h_5 : (head :: tail).min ⋯ = w
h_6 : ¬head = w
h_7 : ¬-1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
left : (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
right :
∀ (a : α),
count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count a ((head :: tail).erase ((head :: tail).min ⋯))
⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] Std.IsLinearPreorder α
[prop] ¬(head :: tail).minFirst ~ head :: tail
[prop] ((head :: tail).minFirst ~ head :: tail) =
∀ (a : α), count a (head :: tail).minFirst = count a (head :: tail)
[prop] (head :: tail).minFirst = (head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)
[prop] ¬count w (head :: tail).minFirst = count w (head :: tail)
[prop] (head :: tail).minFirst ~ head :: tail →
(head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
[prop] (head :: tail).erase ((head :: tail).min ⋯) =
if head = (head :: tail).min ⋯ then tail else head :: tail.erase ((head :: tail).min ⋯)
[prop] (head :: tail).minFirst ~ head :: tail → count w (head :: tail).minFirst = count w (head :: tail)
[prop] count w (head :: tail) = count w tail + if head = w then 1 else 0
[prop] count w ((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)) =
count w ((head :: tail).erase ((head :: tail).min ⋯)) + if (head :: tail).min ⋯ = w then 1 else 0
[prop] ((head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)) =
∀ (a : α),
count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count a ((head :: tail).erase ((head :: tail).min ⋯))
[prop] ((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)).erase ((head :: tail).min ⋯) =
(head :: tail).erase ((head :: tail).min ⋯)
[prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯) →
count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count w ((head :: tail).erase ((head :: tail).min ⋯))
[prop] count w ((head :: tail).erase ((head :: tail).min ⋯)) =
count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0
[prop] ↑(count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0) =
if -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w (head :: tail)) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0
[prop] count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0
[prop] ↑(count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0) =
if -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0
[prop] -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
[prop] ¬-1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
[prop] (head :: tail).min ⋯ = w
[prop] ¬head = w
[prop] count w (head :: tail.erase ((head :: tail).min ⋯)) =
count w (tail.erase ((head :: tail).min ⋯)) + if head = w then 1 else 0
[prop] count w (tail.erase ((head :: tail).min ⋯)) = count w tail - if (head :: tail).min ⋯ = w then 1 else 0
[prop] ↑(count w tail - if (head :: tail).min ⋯ = w then 1 else 0) =
if -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w tail) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0
[prop] ¬-1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
[prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
[prop] ∀ (a : α),
count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count a ((head :: tail).erase ((head :: tail).min ⋯))
[prop] count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count w ((head :: tail).erase ((head :: tail).min ⋯))
[eqc] True propositions
[prop] Std.IsLinearPreorder α
[prop] -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
[prop] ¬head :: tail = []
[prop] ((head :: tail).minFirst ~ head :: tail) =
∀ (a : α), count a (head :: tail).minFirst = count a (head :: tail)
[prop] (head :: tail).min ⋯ = w
[prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
[prop] (head :: tail).minFirst ~ head :: tail → count w (head :: tail).minFirst = count w (head :: tail)
[prop] (head :: tail).minFirst ~ head :: tail →
(head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)
[prop] ((head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯)) =
∀ (a : α),
count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count a ((head :: tail).erase ((head :: tail).min ⋯))
[prop] count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count w ((head :: tail).erase ((head :: tail).min ⋯))
[prop] ∀ (a : α),
count a ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count a ((head :: tail).erase ((head :: tail).min ⋯))
[prop] (head :: tail).minFirst.erase ((head :: tail).min ⋯) ~ (head :: tail).erase ((head :: tail).min ⋯) →
count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)) =
count w ((head :: tail).erase ((head :: tail).min ⋯))
[eqc] False propositions
[prop] (head :: tail).minFirst ~ head :: tail
[prop] -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
[prop] -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0
[prop] count w (head :: tail).minFirst = count w (head :: tail)
[prop] head :: tail = []
[prop] ∀ (a : α), count a (head :: tail).minFirst = count a (head :: tail)
[prop] head = w
[prop] head = (head :: tail).min ⋯
[eqc] Equivalence classes
[eqc] {(head :: tail).minFirst, (head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)}
[eqc] {w, (head :: tail).min ⋯}
[eqc] {count w (head :: tail), count w tail + if head = w then 1 else 0}
[eqc] {count w (head :: tail).minFirst,
1,
count w ((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)),
count w ((head :: tail).erase ((head :: tail).min ⋯)) + if (head :: tail).min ⋯ = w then 1 else 0}
[eqc] {if (head :: tail).min ⋯ = w then 1 else 0}
[eqc] {(head :: tail).erase ((head :: tail).min ⋯),
head :: tail.erase ((head :: tail).min ⋯),
(head :: tail).minFirst.erase ((head :: tail).min ⋯),
((head :: tail).min ⋯ :: (head :: tail).erase ((head :: tail).min ⋯)).erase ((head :: tail).min ⋯)}
[eqc] {if head = (head :: tail).min ⋯ then tail else head :: tail.erase ((head :: tail).min ⋯)}
[eqc] {count w ((head :: tail).erase ((head :: tail).min ⋯)),
count w (head :: tail.erase ((head :: tail).min ⋯)),
count w ((head :: tail).minFirst.erase ((head :: tail).min ⋯)),
count w (tail.erase ((head :: tail).min ⋯)) + if head = w then 1 else 0,
count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0,
count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0}
[eqc] {count w (tail.erase ((head :: tail).min ⋯)), count w tail - if (head :: tail).min ⋯ = w then 1 else 0}
[eqc] others
[eqc] {↑0,
↑(count w (tail.erase ((head :: tail).min ⋯))),
↑(count w ((head :: tail).erase ((head :: tail).min ⋯))),
↑(if head = w then 1 else 0),
0,
if -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w tail) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0,
if -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w (head :: tail)) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0,
if -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0,
↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0),
↑(count w (tail.erase ((head :: tail).min ⋯)) + if head = w then 1 else 0),
↑(count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0),
↑(count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0),
↑(count w tail - if (head :: tail).min ⋯ = w then 1 else 0)}
[eqc] {↑(if (head :: tail).min ⋯ = w then 1 else 0),
↑1,
↑(count w (head :: tail).minFirst),
↑(count w ((head :: tail).erase ((head :: tail).min ⋯)) + if (head :: tail).min ⋯ = w then 1 else 0)}
[eqc] {0, if head = w then 1 else 0}
[eqc] {-1 * ↑(count w (head :: tail).minFirst), -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)}
[eqc] {↑(count w ((head :: tail).erase ((head :: tail).min ⋯))),
↑(if head = w then 1 else 0),
↑(count w (tail.erase ((head :: tail).min ⋯))),
↑(count w (head :: tail) - if (head :: tail).min ⋯ = w then 1 else 0),
↑(count w (head :: tail).minFirst - if (head :: tail).min ⋯ = w then 1 else 0),
↑(count w tail - if (head :: tail).min ⋯ = w then 1 else 0)}
[eqc] {↑(count w (head :: tail)), ↑(count w tail + if head = w then 1 else 0)}
[cases] Case analyses
[cases] [1/2]: if -1 * ↑(count w (head :: tail).minFirst) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w (head :: tail).minFirst) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0
[cases] source: E-matching `count_erase`
[cases] [2/2]: if -1 * ↑(count w (head :: tail)) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w (head :: tail)) + -1 * ↑(if (head :: tail).min ⋯ = w then 1 else 0)
else 0
[cases] source: E-matching `count_erase`
[cases] [1/2]: if (head :: tail).min ⋯ = w then 1 else 0
[cases] source: E-matching `count_cons`
[cases] [2/2]: if head = w then 1 else 0
[cases] source: E-matching `count_cons`
[cases] [2/2]: if -1 * ↑(count w tail) + ↑(if (head :: tail).min ⋯ = w then 1 else 0) ≤ 0 then
↑(count w tail) + -1 * ↑(if (head ::...(truncated)
Try
lake updateand then investigate why this update causeslake build,lake test, orlake lintto fail.Files changed in update:
Build Output