Updates available but manual intervention required

[github-actions]

Try lake update and then investigate why this update causes lake build, lake test, or lake lint to fail.

Files changed

• lake-manifest.json
• lean-toolchain

Build Output

✖ [3414/3508] Building LeanByExample.TypeClass.Decidable (462ms)
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/TypeClass/Decidable.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/TypeClass/Decidable.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/TypeClass/Decidable.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/TypeClass/Decidable.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/TypeClass/Decidable.setup.json --json
info: LeanByExample/TypeClass/Decidable.lean:8:0: decide : (p : Prop) → [self : Decidable p] → Bool
info: LeanByExample/TypeClass/Decidable.lean:58:15: class Decidable (p : Prop) : Type
number of parameters: 1
fields:
  Decidable.decide : Bool
  Decidable.reflects_decide : (decide p).Reflects p
constructor:
  Decidable.intro {p : Prop} (decide : Bool) (reflects_decide : decide.Reflects p) : Decidable p
error: LeanByExample/TypeClass/Decidable.lean:58:0: ❌️ Docstring on `#guard_msgs` does not match generated message:

- info: inductive Decidable : Prop → Type
+ info: class Decidable (p : Prop) : Type
  number of parameters: 1
- constructors:
- Decidable.isFalse : {p : Prop} → ¬p → Decidable p
- Decidable.isTrue : {p : Prop} → p → Decidable p
+ fields:
+   Decidable.decide : Bool
+   Decidable.reflects_decide : (decide p).Reflects p
+ constructor:
+   Decidable.intro {p : Prop} (decide : Bool) (reflects_decide : decide.Reflects p) : Decidable p
✖ [3492/3673] Building LeanByExample.Declarative.GrindPattern.AttributeFailure (875ms)
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Declarative/GrindPattern/AttributeFailure.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Declarative/GrindPattern/AttributeFailure.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Declarative/GrindPattern/AttributeFailure.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Declarative/GrindPattern/AttributeFailure.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Declarative/GrindPattern/AttributeFailure.setup.json --json
error: LeanByExample/Declarative/GrindPattern/AttributeFailure.lean:33:11: invalid `grind` theorem, failed to find a usable pattern using different modifiers
error: LeanByExample/Declarative/GrindPattern/AttributeFailure.lean:32:0: ❌️ Docstring on `#guard_msgs` does not match generated message:

- error: invalid `grind` theorem, failed to find an usable pattern using different modifiers
+ error: invalid `grind` theorem, failed to find a usable pattern using different modifiers
⚠ [3558/3673] Replaying LeanByExample.Tactic.Mvcgen.TakeWhile
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Tactic/Mvcgen/TakeWhile.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/TakeWhile.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/TakeWhile.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/TakeWhile.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/TakeWhile.setup.json --json
warning: LeanByExample/Tactic/Mvcgen/TakeWhile.lean:36:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
warning: LeanByExample/Tactic/Mvcgen/TakeWhile.lean:58:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
⚠ [3559/3673] Replaying LeanByExample.Tactic.Mvcgen.Fibonacci
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Tactic/Mvcgen/Fibonacci.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/Fibonacci.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/Fibonacci.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/Fibonacci.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/Fibonacci.setup.json --json
warning: LeanByExample/Tactic/Mvcgen/Fibonacci.lean:32:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
⚠ [3560/3673] Replaying LeanByExample.Tactic.Mvcgen.PairsSumToZero
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Tactic/Mvcgen/PairsSumToZero.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/PairsSumToZero.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/PairsSumToZero.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/PairsSumToZero.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/PairsSumToZero.setup.json --json
warning: LeanByExample/Tactic/Mvcgen/PairsSumToZero.lean:41:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
⚠ [3561/3673] Replaying LeanByExample.Tactic.Mvcgen.DoubleSum
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Tactic/Mvcgen/DoubleSum.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/DoubleSum.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/DoubleSum.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/DoubleSum.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/DoubleSum.setup.json --json
warning: LeanByExample/Tactic/Mvcgen/DoubleSum.lean:40:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
⚠ [3562/3673] Replaying LeanByExample.Tactic.Mvcgen.BelowZero
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Tactic/Mvcgen/BelowZero.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/BelowZero.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/BelowZero.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/BelowZero.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/BelowZero.setup.json --json
warning: LeanByExample/Tactic/Mvcgen/BelowZero.lean:74:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
⚠ [3563/3673] Replaying LeanByExample.Tactic.Mvcgen.NaiveExpo
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Tactic/Mvcgen/NaiveExpo.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/NaiveExpo.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/NaiveExpo.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/NaiveExpo.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/NaiveExpo.setup.json --json
warning: LeanByExample/Tactic/Mvcgen/NaiveExpo.lean:18:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
⚠ [3564/3673] Replaying LeanByExample.Tactic.Mvcgen.Filter
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.35.0-rc2/bin/lean /home/runner/work/lean-by-example/lean-by-example/LeanByExample/Tactic/Mvcgen/Filter.lean -o /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/Filter.olean -i /home/runner/work/lean-by-example/lean-by-example/.lake/build/lib/lean/LeanByExample/Tactic/Mvcgen/Filter.ilean -c /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/Filter.c --setup /home/runner/work/lean-by-example/lean-by-example/.lake/build/ir/LeanByExample/Tactic/Mvcgen/Filter.setup.json --json
warning: LeanByExample/Tactic/Mvcgen/Filter.lean:27:2: syntax 'Lean.Parser.Tactic.mvcgen' has been deprecated: use `vcgen` instead

Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
⚠ [3565/3673] Replaying LeanByExample.Tactic.Mvcgen.BinaryExpo
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/ru...(truncated)