Updates available but manual intervention required

Open

#87 opened on Jul 12, 2026 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

auto-update-lean-fail

Dominant language: Lean
Stars: 8
Forks: 1
Avg merge: 53m
Merged PRs (30d): 2

Description

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

lake-manifest.json

Build Output

⚠ [125/290] Replayed Batteries.Data.Array.Basic
warning: Batteries/Data/Array/Basic.lean:149:0: Definition `unsafe_sizeFitsUSize` is a proposition; use `theorem` instead of `def`

Note: This linter can be disabled with `set_option linter.defProp false`
✖ [206/356] Building Mathlib.Tactic.Linter.Whitespace (1.7s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/mathlib/Mathlib/Tactic/Linter/Whitespace.lean -o /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Whitespace.olean -i /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Whitespace.ilean -c /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Whitespace.c --setup /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Whitespace.setup.json --json
error: Mathlib/Tactic/Linter/Whitespace.lean:343:15: Type mismatch
  none
has type
  Option ?m.118
but is expected to have type
  Unit
error: Lean exited with code 1
✖ [231/492] Building Batteries.Data.Nat.Basic (633ms)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/batteries/Batteries/Data/Nat/Basic.lean -o /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Nat/Basic.olean -i /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Nat/Basic.ilean -c /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Basic.c --setup /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Basic.setup.json --json
error: Batteries/Data/Nat/Basic.lean:95:4: `Nat.sqrt` has already been declared
error: Lean exited with code 1
✖ [240/628] Building Aesop.Builder.Forward (2.4s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/aesop/Aesop/Builder/Forward.lean -o /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Builder/Forward.olean -i /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Builder/Forward.ilean -c /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Forward.c --setup /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Forward.setup.json --json
error: Aesop/Builder/Forward.lean:32:8: typeclass instance problem is stuck
  Max ?m.15

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Max` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
error: Lean exited with code 1
✖ [310/1913] Building Mathlib.Tactic.Linter.Style (3.5s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/mathlib/Mathlib/Tactic/Linter/Style.lean -o /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Style.olean -i /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Style.ilean -c /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Style.c --setup /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Style.setup.json --json
error: Mathlib/Tactic/Linter/Style.lean:467:15: Type mismatch
  impMods.raw
has type
  Syntax
but is expected to have type
  Unit
error: Mathlib/Tactic/Linter/Style.lean:468:18: Type mismatch
  stx
has type
  Syntax
but is expected to have type
  Unit
warning: Mathlib/Tactic/Linter/Style.lean:461:4: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
error: Mathlib/Tactic/Linter/Style.lean:469:16: Invalid field notation: Type of
  stx
is not known; cannot resolve field `getSubstring?`

Hint: Consider replacing the field projection `.getSubstring?` with a call to the function `Syntax.getSubstring?`.
error: Mathlib/Tactic/Linter/Style.lean:472:23: Invalid field notation: Type of
  sstr
is not known; cannot resolve field `getD`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Array.getD`
  • `ByteSlice.getD`
  • `List.getD`
  • `Option.getD`
  • `Subarray.getD`
  • `Vector.getD`
  • `Std.DHashMap.getD`
  • `Std.DTreeMap.getD`
  • `Std.HashMap.getD`
  • `Std.HashSet.getD`
  • `Std.TreeMap.getD`
  • `Std.TreeSet.getD`
  • `Std.DHashMap.Const.getD`
  • `Std.DHashMap.Raw.getD`
  • `Std.DTreeMap.Const.getD`
  • `Std.DTreeMap.Raw.getD`
  • `Std.HashMap.Raw.getD`
  • `Std.TreeMap.Raw.getD`
  • `Std.DHashMap.Internal.AssocList.getD`
  • `Std.DHashMap.Internal.Raw₀.getD`
  • `Std.DHashMap.Raw.Const.getD`
  • `Std.DTreeMap.Internal.Impl.getD`
  • `Std.DTreeMap.Raw.Const.getD`
  • `Std.DHashMap.Internal.Raw₀.Const.getD`
  • `Std.DTreeMap.Internal.Impl.Const.getD`
error: Mathlib/Tactic/Linter/Style.lean:475:10: Invalid field notation: Type of
  line
is not known; cannot resolve field `splitOn`

Hint: Consider replacing the field projection with a call to one of the following:
  • `List.splitOn`
  • `String.splitOn`
  • `Substring.Raw.splitOn`
error: Mathlib/Tactic/Linter/Style.lean:475:56: Invalid field notation: Type of
  line
is not known; cannot resolve field `toString`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Char.toString`
  • `Float.toString`
  • `Float32.toString`
  • `List.toString`
  • `Substring.toString`
  • `toString`
  • `IO.Error.toString`
  • `IO.TaskState.toString`
  • `InternalExceptionId.toString`
  • `JsonNumber.toString`
  • `LBool.toString`
  • `Message.toString`
  • `MessageData.toString`
  • `MessageSeverity.toString`
  • `Name.toString`
  • `SerialMessage.toString`
  • `String.Slice.toString`
  • `Substring.Raw.toString`
  • `System.FilePath.toString`
  • `System.SearchPath.toString`
  • `Error.toString`
  • `PersistentArray.Stats.toString`
  • `PersistentHashMap.Stats.toString`
  • `SubExpr.Pos.toString`
  • `String.Legacy.Iterator.toString`
  • `String.Slice.Subslice.toString`
  • `Substring.Raw.Internal.toString`
  • `PrettyPrinter.Delaborator.OmissionReason.toString`
error: Mathlib/Tactic/Linter/Style.lean:476:28: Invalid field notation: Type of
  line
is not known; cannot resolve field `contains`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Array.contains`
  • `ByteSlice.contains`
  • `List.contains`
  • `String.contains`
  • `Vector.contains`
  • `AssocList.contains`
  • `Environment.contains`
  • `KVMap.contains`
  • `LocalContext.contains`
  • `MapDeclarationExtension.contains`
  • `NameHashSet.contains`
  • `NameMap.contains`
  • `NameSSet.contains`
  • `NameSet.contains`
  • `Options.contains`
  • `PersistentHashMap.contains`
  • `PersistentHashSet.contains`
  • `PtrMap.contains`
  • `PtrSet.contains`
  • `SMap.contains`
  • `SSet.contains`
  • `Std.DHashMap.contains`
  • `Std.DTreeMap.contains`
  • `Std.HashMap.contains`
  • `Std.HashSet.contains`
  • `Std.TreeMap.contains`
  • `Std.TreeSet.contains`
  • `String.Internal.contains`
  • `String.Slice.contains`
  • `Substring.Raw.contains`
  • `Info.contains`
  • `FVarSubst.contains`
  • `Occurrences.contains`
  • `Syntax.Range.contains`
  • `Std.DHashMap.Raw.contains`
  • `Std.DTreeMap.Raw.contains`
  • `Std.HashMap.Raw.contains`
  • `Std.TreeMap.Raw.contains`
  • `Std.DHashMap.Internal.AssocList.contains`
  • `Std.DHashMap.Internal.Raw₀.contains`
  • `Std.DTreeMap.Internal.Cell.contains`
  • `Std.DTreeMap.Internal.Impl.contains`
error: Mathlib/Tactic/Linter/Style.lean:482:22: Invalid field notation: Type of
  line
is not known; cannot resolve field `drop`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Array.drop`
  • `List.drop`
  • `String.drop`
  • `Subarray.drop`
  • `Vector.drop`
  • `List.Pairwise.drop`
  • `List.Perm.drop`
  • `List.Sublist.drop`
  • `String.Internal.drop`
  • `String.Slice.drop`
  • `Substring.Raw.drop`
  • `Substring.Raw.Internal.drop`
error: Mathlib/Tactic/Linter/Style.lean:482:57: Invalid field notation: Type of
  line
is not known; cannot resolve field `stopPos`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Substring.Raw.stopPos`
  • `TokenCacheEntry.stopPos`
error: Lean exited with code 1
✖ [324/1919] Building Mathlib.Tactic.TacticAnalysis.Declarations (3.6s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/mathlib/Mathlib/Tactic/TacticAnalysis/Declarations.lean -o /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/TacticAnalysis/Declarations.olean -i /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/TacticAnalysis/Declarations.ilean -c /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/TacticAnalysis/Declarations.c --setup /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/TacticAnalysis/Declarations.setup.json --json
error: Mathlib/Tactic/TacticAnalysis/Declarations.lean:415:21: Type mismatch
  (__do_lift✝.pretty.splitOn "\n")[0]!.trimAscii
has type
  String.Slice
but is expected to have type
  Unit
error: Mathlib/Tactic/TacticAnalysis/Declarations.lean:417:21: Type mismatch
  i.tacI.stx.reprint.getD "???"
has type
  String
but is expected to have type
  Unit
error: Mathlib/Tactic/TacticAnalysis/Declarations.lean:414:34: Early returning r✝ but the info said there is no early return
error: Lean exited with code 1
✖ [986/1919] Building Plausible.Testable (2.1s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/plausible/Plausible/Testable.lean -o /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean/Plausible/Testable.olean -i /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean/Plausible/Testable.ilean -c /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/ir/Plausible/Testable.c --setup /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/ir/Plausible/Testable.setup.json --json
error: Plausible/Testable.lean:383:67: Application type mismatch: The argument
  addShrinks (n + 1) res
has type
  TestResult (β (SampleableExt.interp candidate))
but is expected to have type
  ?m.278 __r✝⁵ __r✝⁴ candidate __s✝ __r✝² res __r✝¹ __r✝ candidate
in the application
  ⟨candidate, addShrinks (n + 1) res⟩
error: Lean exited with code 1
✖ [1900/1919] Building Batteries.Data.Array.Lemmas (1.6s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean -o /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Lemmas.olean -i /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Lemmas.ilean -c /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Lemmas.c --setup /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Lemmas.setup.json --json
error: Batteries/Data/Array/Lemmas.lean:50:8: `Array.size_set!` has already been declared
error: Lean exited with code 1
Some required targets logged failures:
- Mathlib.Tactic.Linter.Whitespace
- Batteries.Data.Nat.Basic
- Aesop.Builder.Forward
- Mathlib.Tactic.Linter.Style
- Mathlib.Tactic.TacticAnalysis.Declarations
- Plausible.Testable
- Batteries.Data.Array.Lemmas
error: build failed

Test Output

⚠ [125/290] Replayed Batteries.Data.Array.Basic
warning: Batteries/Data/Array/Basic.lean:149:0: Definition `unsafe_sizeFitsUSize` is a proposition; use `theorem` instead of `def`

Note: This linter can be disabled with `set_option linter.defProp false`
✖ [206/352] Building Mathlib.Tactic.Linter.Whitespace (1.7s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/mathlib/Mathlib/Tactic/Linter/Whitespace.lean -o /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Whitespace.olean -i /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Whitespace.ilean -c /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Whitespace.c --setup /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Whitespace.setup.json --json
error: Mathlib/Tactic/Linter/Whitespace.lean:343:15: Type mismatch
  none
has type
  Option ?m.118
but is expected to have type
  Unit
error: Lean exited with code 1
✖ [231/449] Building Batteries.Data.Nat.Basic (526ms)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/batteries/Batteries/Data/Nat/Basic.lean -o /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Nat/Basic.olean -i /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Nat/Basic.ilean -c /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Basic.c --setup /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Basic.setup.json --json
error: Batteries/Data/Nat/Basic.lean:95:4: `Nat.sqrt` has already been declared
error: Lean exited with code 1
✖ [234/537] Building Aesop.Builder.Forward (2.3s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/aesop/Aesop/Builder/Forward.lean -o /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Builder/Forward.olean -i /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Builder/Forward.ilean -c /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Forward.c --setup /home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Forward.setup.json --json
error: Aesop/Builder/Forward.lean:32:8: typeclass instance problem is stuck
  Max ?m.15

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Max` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
error: Lean exited with code 1
✖ [311/1927] Building Mathlib.Tactic.Linter.Style (3.3s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/mathlib/Mathlib/Tactic/Linter/Style.lean -o /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Style.olean -i /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Style.ilean -c /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Style.c --setup /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Style.setup.json --json
error: Mathlib/Tactic/Linter/Style.lean:467:15: Type mismatch
  impMods.raw
has type
  Syntax
but is expected to have type
  Unit
error: Mathlib/Tactic/Linter/Style.lean:468:18: Type mismatch
  stx
has type
  Syntax
but is expected to have type
  Unit
warning: Mathlib/Tactic/Linter/Style.lean:461:4: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
error: Mathlib/Tactic/Linter/Style.lean:469:16: Invalid field notation: Type of
  stx
is not known; cannot resolve field `getSubstring?`

Hint: Consider replacing the field projection `.getSubstring?` with a call to the function `Syntax.getSubstring?`.
error: Mathlib/Tactic/Linter/Style.lean:472:23: Invalid field notation: Type of
  sstr
is not known; cannot resolve field `getD`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Array.getD`
  • `ByteSlice.getD`
  • `List.getD`
  • `Option.getD`
  • `Subarray.getD`
  • `Vector.getD`
  • `Std.DHashMap.getD`
  • `Std.DTreeMap.getD`
  • `Std.HashMap.getD`
  • `Std.HashSet.getD`
  • `Std.TreeMap.getD`
  • `Std.TreeSet.getD`
  • `Std.DHashMap.Const.getD`
  • `Std.DHashMap.Raw.getD`
  • `Std.DTreeMap.Const.getD`
  • `Std.DTreeMap.Raw.getD`
  • `Std.HashMap.Raw.getD`
  • `Std.TreeMap.Raw.getD`
  • `Std.DHashMap.Internal.AssocList.getD`
  • `Std.DHashMap.Internal.Raw₀.getD`
  • `Std.DHashMap.Raw.Const.getD`
  • `Std.DTreeMap.Internal.Impl.getD`
  • `Std.DTreeMap.Raw.Const.getD`
  • `Std.DHashMap.Internal.Raw₀.Const.getD`
  • `Std.DTreeMap.Internal.Impl.Const.getD`
error: Mathlib/Tactic/Linter/Style.lean:475:10: Invalid field notation: Type of
  line
is not known; cannot resolve field `splitOn`

Hint: Consider replacing the field projection with a call to one of the following:
  • `List.splitOn`
  • `String.splitOn`
  • `Substring.Raw.splitOn`
error: Mathlib/Tactic/Linter/Style.lean:475:56: Invalid field notation: Type of
  line
is not known; cannot resolve field `toString`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Char.toString`
  • `Float.toString`
  • `Float32.toString`
  • `List.toString`
  • `Substring.toString`
  • `toString`
  • `IO.Error.toString`
  • `IO.TaskState.toString`
  • `InternalExceptionId.toString`
  • `JsonNumber.toString`
  • `LBool.toString`
  • `Message.toString`
  • `MessageData.toString`
  • `MessageSeverity.toString`
  • `Name.toString`
  • `SerialMessage.toString`
  • `String.Slice.toString`
  • `Substring.Raw.toString`
  • `System.FilePath.toString`
  • `System.SearchPath.toString`
  • `Error.toString`
  • `PersistentArray.Stats.toString`
  • `PersistentHashMap.Stats.toString`
  • `SubExpr.Pos.toString`
  • `String.Legacy.Iterator.toString`
  • `String.Slice.Subslice.toString`
  • `Substring.Raw.Internal.toString`
  • `PrettyPrinter.Delaborator.OmissionReason.toString`
error: Mathlib/Tactic/Linter/Style.lean:476:28: Invalid field notation: Type of
  line
is not known; cannot resolve field `contains`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Array.contains`
  • `ByteSlice.contains`
  • `List.contains`
  • `String.contains`
  • `Vector.contains`
  • `AssocList.contains`
  • `Environment.contains`
  • `KVMap.contains`
  • `LocalContext.contains`
  • `MapDeclarationExtension.contains`
  • `NameHashSet.contains`
  • `NameMap.contains`
  • `NameSSet.contains`
  • `NameSet.contains`
  • `Options.contains`
  • `PersistentHashMap.contains`
  • `PersistentHashSet.contains`
  • `PtrMap.contains`
  • `PtrSet.contains`
  • `SMap.contains`
  • `SSet.contains`
  • `Std.DHashMap.contains`
  • `Std.DTreeMap.contains`
  • `Std.HashMap.contains`
  • `Std.HashSet.contains`
  • `Std.TreeMap.contains`
  • `Std.TreeSet.contains`
  • `String.Internal.contains`
  • `String.Slice.contains`
  • `Substring.Raw.contains`
  • `Info.contains`
  • `FVarSubst.contains`
  • `Occurrences.contains`
  • `Syntax.Range.contains`
  • `Std.DHashMap.Raw.contains`
  • `Std.DTreeMap.Raw.contains`
  • `Std.HashMap.Raw.contains`
  • `Std.TreeMap.Raw.contains`
  • `Std.DHashMap.Internal.AssocList.contains`
  • `Std.DHashMap.Internal.Raw₀.contains`
  • `Std.DTreeMap.Internal.Cell.contains`
  • `Std.DTreeMap.Internal.Impl.contains`
error: Mathlib/Tactic/Linter/Style.lean:482:22: Invalid field notation: Type of
  line
is not known; cannot resolve field `drop`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Array.drop`
  • `List.drop`
  • `String.drop`
  • `Subarray.drop`
  • `Vector.drop`
  • `List.Pairwise.drop`
  • `List.Perm.drop`
  • `List.Sublist.drop`
  • `String.Internal.drop`
  • `String.Slice.drop`
  • `Substring.Raw.drop`
  • `Substring.Raw.Internal.drop`
error: Mathlib/Tactic/Linter/Style.lean:482:57: Invalid field notation: Type of
  line
is not known; cannot resolve field `stopPos`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Substring.Raw.stopPos`
  • `TokenCacheEntry.stopPos`
error: Lean exited with code 1
ℹ [314/1927] Replayed CSDP/csdp.static
info: stderr:
In function ‘build_constraints’,
    inlined from ‘lean_csdp_solve’ at /home/runner/work/sos/sos/.lake/packages/CSDP/ffi/lean_csdp.c:337:7:
/home/runner/work/sos/sos/.lake/packages/CSDP/ffi/lean_csdp.c:215:60: warning: argument 1 range [13835058057429647360, 18446744073709551615] exceeds maximum object size 9223372036854775807 [-Walloc-size-larger-than=]
  215 |   struct sparseblock **block_ptrs = (struct sparseblock **)calloc(
      |                                                            ^~~~~~~
  216 |       (size_t)num_constraints * (size_t)nblocks, sizeof(struct sparseblock *));
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from /home/runner/work/sos/sos/.lake/packages/CSDP/ffi/lean_csdp.c:11:
/usr/include/stdlib.h: In function ‘lean_csdp_solve’:
/usr/include/stdlib.h:675:14: note: in a call to allocation function ‘calloc’ declared here
  675 | extern void *calloc (size_t __nmemb, size_t __size)
      |              ^~~~~~
In function ‘build_constraints’,
    inlined from ‘lean_csdp_solve’ at /home/runner/work/sos/sos/.lake/packages/CSDP/ffi/lean_csdp.c:337:7:
/home/runner/work/sos/sos/.lake/packages/CSDP/ffi/lean_csdp.c:222:22: warning: argument 1 range [13835058057429647360, 18446744073709551615] exceeds maximum object size 9223372036854775807 [-Walloc-size-larger-than=]
  222 |   int *fill = (int *)calloc((size_t)num_constraints * (size_t)nblocks,
      |                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  223 |                             sizeof(int));
      |                             ~~~~~~~~~~~~
/usr/include/stdlib.h: In function ‘lean_csdp_solve’:
/usr/include/stdlib.h:675:14: note: in a call to allocation function ‘calloc’ declared here
  675 | extern void *calloc (size_t __nmemb, size_t __size)
      |              ^~~~~~
✖ [324/1927] Building Mathlib.Tactic.TacticAnalysis.Declarations (3.8s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/mathlib/Mathlib/Tactic/TacticAnalysis/Declarations.lean -o /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/TacticAnalysis/Declarations.olean -i /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/TacticAnalysis/Declarations.ilean -c /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/TacticAnalysis/Declarations.c --setup /home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/TacticAnalysis/Declarations.setup.json --json
error: Mathlib/Tactic/TacticAnalysis/Declarations.lean:415:21: Type mismatch
  (__do_lift✝.pretty.splitOn "\n")[0]!.trimAscii
has type
  String.Slice
but is expected to have type
  Unit
error: Mathlib/Tactic/TacticAnalysis/Declarations.lean:417:21: Type mismatch
  i.tacI.stx.reprint.getD "???"
has type
  String
but is expected to have type
  Unit
error: Mathlib/Tactic/TacticAnalysis/Declarations.lean:414:34: Early returning r✝ but the info said there is no early return
error: Lean exited with code 1
✖ [986/1927] Building Plausible.Testable (2.1s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/plausible/Plausible/Testable.lean -o /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean/Plausible/Testable.olean -i /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean/Plausible/Testable.ilean -c /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/ir/Plausible/Testable.c --setup /home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/ir/Plausible/Testable.setup.json --json
error: Plausible/Testable.lean:383:67: Application type mismatch: The argument
  addShrinks (n + 1) res
has type
  TestResult (β (SampleableExt.interp candidate))
but is expected to have type
  ?m.278 __r✝⁵ __r✝⁴ candidate __s✝ __r✝² res __r✝¹ __r✝ candidate
in the application
  ⟨candidate, addShrinks (n + 1) res⟩
error: Lean exited with code 1
✖ [1902/1927] Building Batteries.Data.Array.Lemmas (1.6s)
trace: .> LEAN_PATH=/home/runner/work/sos/sos/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CSDP/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/packages/CompPoly/.lake/build/lib/lean:/home/runner/work/sos/sos/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/sos/sos/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean -o /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Lemmas.olean -i /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Lemmas.ilean -c /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Lemmas.c --setup /home/runner/work/sos/sos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Lemmas.setup.json --json
error: Batteries/Data/Array/Lemmas.lean:50:8: `Array.size_set!` has already been declared
error: Lean exited with code 1
Some required targets logged failures:
- Mathlib.Tactic.Linter.Whitespace
- Batteries.Data.Nat.Basic
- Aesop.Builder.Forward
- Mathlib.Tactic.Linter.Style
- Mathlib.Tactic.TacticAnalysis.Declarations
- Plausible.Testable
- Batteries.Data.Array.Lemmas
error: build failed

Contributor guide

Open the contributing guide

First steps

Read the whole issue, then the project's contributing guide.
Comment on the issue to say you are picking it up — it saves two people doing the same work.
Fork the repository and make your change on a branch.
Open a pull request that references the issue number.

Research direction

Run lake update, then reproduce the failures with lake build, lake test, and lake lint. Start with lake-manifest.json and the reported files, including Mathlib/Tactic/Linter/Whitespace.lean, Batteries/Data/Nat/Basic.lean, Aesop/Builder/Forward.lean, and Mathlib/Tactic/Linter/Style.lean. Done means the updated dependencies build, test, and lint successfully.

Written by the indexing model from the issue text.

Assessment

Domain: build-system
Issue type: Bug
Difficulty: 4/5
Estimated time: 3-5 days
Activity status: Quiet
Clarity: Mostly clear
Newbie friendliness: 42/100