jason@Jasons-MacBook-Air-5 docbuild % lake build BrownianMotion:docs ✖ [54/160] Building Mathlib.Tactic.Linter.Header trace: .> LEAN_PATH=/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/subverso/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/BibtexQuery/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/doc-gen4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/docbuild/.lake/build/lib/lean /Users/jason/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/Mathlib/Tactic/Linter/Header.lean -o /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Header.olean -i /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Linter/Header.ilean -c /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Header.c --setup /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Linter/Header.setup.json --json warning: Mathlib/Tactic/Linter/Header.lean:100:17: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Mathlib/Tactic/Linter/Header.lean:102:68: `Substring.toString` has been deprecated: Use `Substring.Raw.toString` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.toString` to `Substring.Raw.toString x`). error: Mathlib/Tactic/Linter/Header.lean:102:59: Invalid field notation: Function `Substring.toString` does not have a usable parameter of type `Substring` for which to substitute `upToHere` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation warning: Mathlib/Tactic/Linter/Header.lean:108:45: `String.endPos` has been deprecated: Use `String.rawEndPos` instead warning: Mathlib/Tactic/Linter/Header.lean:109:58: `String.endPos` has been deprecated: Use `String.rawEndPos` instead warning: Mathlib/Tactic/Linter/Header.lean:212:89: `String.endPos` has been deprecated: Use `String.rawEndPos` instead error: Lean exited with code 1 ⚠ [138/227] Built Batteries.Control.AlternativeMonad warning: Batteries/Control/AlternativeMonad.lean:107:13: `seq_eq_bind` has been deprecated: Use `seq_eq_bind_map` instead ✖ [166/248] Building Batteries.Linter.UnreachableTactic trace: .> LEAN_PATH=/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/subverso/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/BibtexQuery/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/doc-gen4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/docbuild/.lake/build/lib/lean /Users/jason/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/Batteries/Linter/UnreachableTactic.lean -o /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Linter/UnreachableTactic.olean -i /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Linter/UnreachableTactic.ilean -c /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Linter/UnreachableTactic.c --setup /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Linter/UnreachableTactic.setup.json --json warning: Batteries/Linter/UnreachableTactic.lean:38:35: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`). error: Batteries/Linter/UnreachableTactic.lean:38:23: failed to synthesize BEq String.Range Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. warning: Batteries/Linter/UnreachableTactic.lean:69:26: declaration uses 'sorry' warning: Batteries/Linter/UnreachableTactic.lean:69:26: declaration uses 'sorry' warning: Batteries/Linter/UnreachableTactic.lean:74:18: unused variable `r` Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: Batteries/Linter/UnreachableTactic.lean:80:12: declaration uses 'sorry' warning: Batteries/Linter/UnreachableTactic.lean:80:12: declaration uses 'sorry' warning: Batteries/Linter/UnreachableTactic.lean:84:12: declaration uses 'sorry' warning: Batteries/Linter/UnreachableTactic.lean:87:18: unused variable `r` Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: Batteries/Linter/UnreachableTactic.lean:113:15: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`). warning: Batteries/Linter/UnreachableTactic.lean:114:17: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`). error: Batteries/Linter/UnreachableTactic.lean:115:59: Invalid field notation: Type of unreachable is not known; cannot resolve field `qsort` error: Batteries/Linter/UnreachableTactic.lean:115:2: failed to construct 'ForIn' instance for collection ?m.252 and monad ReaderT Context (StateRefT' IO.RealWorld State (EIO Exception)) warning: Batteries/Linter/UnreachableTactic.lean:111:2: declaration uses 'sorry' error: Lean exited with code 1 ✖ [181/278] Building Batteries.Lean.Meta.UnusedNames trace: .> LEAN_PATH=/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/subverso/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/BibtexQuery/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/doc-gen4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/docbuild/.lake/build/lib/lean /Users/jason/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/Batteries/Lean/Meta/UnusedNames.lean -o /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Lean/Meta/UnusedNames.olean -i /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Lean/Meta/UnusedNames.ilean -c /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/UnusedNames.c --setup /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/UnusedNames.setup.json --json warning: Batteries/Lean/Meta/UnusedNames.lean:16:34: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Lean/Meta/UnusedNames.lean:17:7: `Substring.isEmpty` has been deprecated: Use `Substring.Raw.isEmpty` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.isEmpty` to `Substring.Raw.isEmpty x`). error: Batteries/Lean/Meta/UnusedNames.lean:17:5: Invalid field notation: Function `Substring.isEmpty` does not have a usable parameter of type `Substring` for which to substitute `s` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation error: Lean exited with code 1 ✖ [219/340] Building Batteries.Linter.UnnecessarySeqFocus trace: .> LEAN_PATH=/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/subverso/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/BibtexQuery/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/doc-gen4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/docbuild/.lake/build/lib/lean /Users/jason/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/Batteries/Linter/UnnecessarySeqFocus.lean -o /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Linter/UnnecessarySeqFocus.olean -i /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Linter/UnnecessarySeqFocus.ilean -c /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Linter/UnnecessarySeqFocus.c --setup /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Linter/UnnecessarySeqFocus.setup.json --json warning: Batteries/Linter/UnnecessarySeqFocus.lean:90:39: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`). error: Batteries/Linter/UnnecessarySeqFocus.lean:90:27: failed to synthesize BEq String.Range Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. warning: Batteries/Linter/UnnecessarySeqFocus.lean:97:26: declaration uses 'sorry' warning: Batteries/Linter/UnnecessarySeqFocus.lean:97:26: declaration uses 'sorry' warning: Batteries/Linter/UnnecessarySeqFocus.lean:101:18: unused variable `r` Note: This linter can be disabled with `set_option linter.unusedVariables false` error: Batteries/Linter/UnnecessarySeqFocus.lean:137:45: Invalid field notation: Type of s is not known; cannot resolve field `insert` error: Batteries/Linter/UnnecessarySeqFocus.lean:137:89: Invalid field notation: Type of s is not known; cannot resolve field `erase` error: Batteries/Linter/UnnecessarySeqFocus.lean:147:45: Invalid field notation: Type of s is not known; cannot resolve field `insert` error: Batteries/Linter/UnnecessarySeqFocus.lean:147:89: Invalid field notation: Type of s is not known; cannot resolve field `erase` error: Batteries/Linter/UnnecessarySeqFocus.lean:164:24: Application type mismatch: The argument env has type Environment but is expected to have type PersistentArray InfoTree in the application markUsedTacticsList env warning: Batteries/Linter/UnnecessarySeqFocus.lean:168:15: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`). warning: Batteries/Linter/UnnecessarySeqFocus.lean:169:17: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`). error: Batteries/Linter/UnnecessarySeqFocus.lean:170:59: Invalid field notation: Type of unused is not known; cannot resolve field `qsort` error: Batteries/Linter/UnnecessarySeqFocus.lean:170:2: failed to construct 'ForIn' instance for collection ?m.167 and monad ReaderT Context (StateRefT' IO.RealWorld State (EIO Exception)) error: Lean exited with code 1 ⚠ [363/424] Built Plausible.Arbitrary warning: Plausible/Arbitrary.lean:161:22: `String.mk` has been deprecated: Use `String.ofList` instead ⚠ [377/425] Built Plausible.Sampleable warning: Plausible/Sampleable.lean:236:36: `String.mk` has been deprecated: Use `String.ofList` instead ⚠ [420/470] Built Batteries.Data.List.Lemmas warning: Batteries/Data/List/Lemmas.lean:450:6: `Bool.cond_eq_if` has been deprecated: Use `Bool.cond_eq_ite` instead Note: The updated constant has a different type: ∀ {α : Sort u_1} (b : Bool) (t e : α), (bif b then t else e) = if b = true then t else e instead of ∀ {b : Bool} {α : Sort u_1} {x y : α}, (bif b then x else y) = if b = true then x else y ⚠ [491/557] Built Batteries.Lean.EStateM warning: Batteries/Lean/EStateM.lean:73:13: `seq_eq_bind` has been deprecated: Use `seq_eq_bind_map` instead warning: Batteries/Lean/EStateM.lean:80:13: `seq_eq_bind` has been deprecated: Use `seq_eq_bind_map` instead ⚠ [493/563] Built Batteries.Data.Array.Match warning: Batteries/Data/Array/Match.lean:61:36: `Nat.lt_succ` has been deprecated: Use `Nat.lt_succ_iff` instead Note: `Nat.lt_succ_iff` is protected. References to this constant must include its prefix `Nat` even when inside its namespace. ⚠ [551/1123] Built ProofWidgets.Component.MakeEditLink warning: ProofWidgets/Component/MakeEditLink.lean:10:50: `Substring` has been deprecated: Use `Substring.Raw` instead ⚠ [581/5398] Built Batteries.CodeAction.Match warning: Batteries/CodeAction/Match.lean:19:54: `String.Range` has been deprecated: Use `Lean.Syntax.Range` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Range` to `Syntax.Range x`). ⚠ [759/6951] Built Batteries.Data.String.Basic warning: Batteries/Data/String/Basic.lean:10:22: `Substring` has been deprecated: Use `Substring.Raw` instead ✖ [1162/6951] Building Batteries.Data.String.Matcher trace: .> LEAN_PATH=/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Qq/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/aesop/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/importGraph/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/plausible/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/mathlib/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/kolmogorov_extension4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/checkdecls/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/subverso/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/BibtexQuery/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/Cli/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/.lake/packages/doc-gen4/.lake/build/lib/lean:/Users/jason/Lean/test-docs/brownian-motion/docbuild/.lake/build/lib/lean /Users/jason/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/Batteries/Data/String/Matcher.lean -o /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Matcher.olean -i /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Matcher.ilean -c /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Matcher.c --setup /Users/jason/Lean/test-docs/brownian-motion/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Matcher.setup.json --json warning: Batteries/Data/String/Matcher.lean:36:12: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:39:45: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:48:60: `Substring.bsize` has been deprecated: Use `Substring.Raw.bsize` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.bsize` to `Substring.Raw.bsize x`). error: Batteries/Data/String/Matcher.lean:48:50: Invalid field notation: Function `Substring.bsize` does not have a usable parameter of type `Substring` for which to substitute `m.pattern` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation warning: Batteries/Data/String/Matcher.lean:51:47: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:51:66: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:55:12: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:55:63: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:55:82: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:64:37: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:64:57: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:79:41: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:79:41: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:79:60: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:86:39: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:86:39: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:86:59: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:92:42: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:92:42: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:100:45: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:100:64: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:104:43: `Substring` has been deprecated: Use `Substring.Raw` instead warning: Batteries/Data/String/Matcher.lean:104:63: `Substring` has been deprecated: Use `Substring.Raw` instead error: Batteries/Data/String/Matcher.lean:105:16: Invalid field `findSubstr?`: The environment does not contain `Substring.Raw.findSubstr?` s.toSubstring has type Substring.Raw warning: Batteries/Data/String/Matcher.lean:108:46: `Substring` has been deprecated: Use `Substring.Raw` instead error: Batteries/Data/String/Matcher.lean:109:16: Invalid field `containsSubstr`: The environment does not contain `Substring.Raw.containsSubstr` s.toSubstring has type Substring.Raw error: Lean exited with code 1 ℹ [3549/6951] Built «doc-gen4»/bibPrepass info: stdout: INFO: reference page disabled ℹ [3550/7060] Ran batteries:srcUri.github info: Found git remote for batteries at https://github.com/leanprover-community/batteries @ 5c78955e8375f872c085514cb521216bac1bda17 ℹ [3551/7060] Ran batteries:srcUri.github info: Found git remote for batteries at https://github.com/leanprover-community/batteries @ 5c78955e8375f872c085514cb521216bac1bda17 ℹ [3554/7060] Ran proofwidgets:srcUri.github info: Found git remote for proofwidgets at https://github.com/leanprover-community/ProofWidgets4 @ e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d ℹ [3555/7060] Ran batteries:srcUri.github info: Found git remote for batteries at https://github.com/leanprover-community/batteries @ 5c78955e8375f872c085514cb521216bac1bda17 ℹ [3577/7060] Ran LeanSearchClient:srcUri.github info: Found git remote for LeanSearchClient at https://github.com/leanprover-community/LeanSearchClient @ 2ed4ba69b6127de8f5c2af83cccacd3c988b06bf ℹ [3583/7060] Ran plausible:srcUri.github info: Found git remote for plausible at https://github.com/leanprover-community/plausible @ 2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3 ℹ [3615/7060] Ran Qq:srcUri.github info: Found git remote for Qq at https://github.com/leanprover-community/quote4 @ 2781d8ad404303b2fe03710ac7db946ddfe3539f ℹ [3626/7060] Ran aesop:srcUri.github info: Found git remote for aesop at https://github.com/leanprover-community/aesop @ 26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349 ℹ [3651/7060] Ran importGraph:srcUri.github info: Found git remote for importGraph at https://github.com/leanprover-community/import-graph @ 009064c21bad4d7f421f2901c5e817c8bf3468cb ℹ [3731/7063] Ran mathlib:srcUri.github info: Found git remote for mathlib at https://github.com/leanprover-community/mathlib4 @ 1ccd71f89cbbd82ae7d097723ce1722ca7b01c33 ℹ [4122/7146] Built Qq/Qq.MatchImpl:docs info: stdout: WARNING: Failed to obtain information for: Qq.Impl.mkLambdaQ: failed WARNING: Failed to calculate equational lemmata for Qq.Impl.mkIsDefEqResult: failed ℹ [4140/7155] Built Qq/Qq.Match:docs info: stdout: WARNING: Failed to calculate equational lemmata for Qq.Impl.makeMatchCode: failed WARNING: Failed to obtain information for: Qq.Impl.withLetHave: failed ℹ [4149/7159] Built importGraph/ImportGraph.Meta:docs info: stdout: WARNING: Failed to calculate equational lemmata for Lean.Name.findHome: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) ℹ [7190/7191] Built «doc-gen4»/coreDocs info: stdout: WARNING: Failed to calculate equational lemmata for Std.Time.DateTime.weekday: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Std.Time.PlainDateTime.weekday: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Std.Time.Timestamp.toPlainDateTimeAssumingUTC: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) info: stdout: WARNING: Failed to calculate equational lemmata for Lean.Elab.mkConfigSetter: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.Doc.leanRole: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.Elab.Tactic.Grind.setConfigField: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.Meta.Grind.Arith.isInterpretedTerm: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.Server.Completion.dotIdCompletion: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.CodeAction.holeCodeActionProvider: failed to generate equality theorems for `match` expression `_private.Lean.Server.CodeActions.Provider.0.Lean.CodeAction.holeCodeActionProvider.match_7` case isTrue motive✝ : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo) → Sort u_1 x✝¹ : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo) h_1✝ : (ctx : Lean.Elab.ContextInfo) → (info : Lean.Elab.TermInfo) → motive✝ #[(ctx, info)] h_2✝ : (x : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo)) → motive✝ x x✝ : ∀ (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.TermInfo), x✝¹ = #[(ctx, info)] → False h✝ : x✝¹.size = 1 ⊢ (⋯ ▸ fun h => ⋯ ▸ Prod.casesOn (x✝¹.getLit 0 ⋯ ⋯) fun fst snd => h_1✝ fst snd) ⋯ = h_2✝ x✝¹ WARNING: Failed to calculate equational lemmata for Lean.Elab.Tactic.evalGrindCore: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.Meta.Tactic.TryThis.addRewriteSuggestion: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.Elab.Command.elabElabRulesAux: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs: failed to generate equational theorem for `Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs` no progress at goal α : Type m : Type → Type inst✝² : Monad m inst✝¹ : MonadReaderOf Lean.SubExpr m inst✝ : MonadWithReaderOf Lean.SubExpr m maxArgs : Nat xf : m α xa : α → m α r : Nat.below maxArgs := (Nat.brecOn.go maxArgs fun maxArgs f => do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr (match (motive := (maxArgs : Nat) → Lean.Expr → Nat.below maxArgs → m α) maxArgs, __do_lift with | maxArgs'.succ, fn.app arg => fun x => do let acc ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn x.1 Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg (xa acc) | x, x_1 => fun x => xf) f).2 ⊢ (do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr (match (motive := (maxArgs : Nat) → Lean.Expr → Nat.rec PUnit (fun n n_ih => m α ×' n_ih) maxArgs → m α) maxArgs, __do_lift with | maxArgs'.succ, fn.app arg => fun x => do let acc ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn x.1 Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg (xa acc) | x, x_1 => fun x => xf) r) = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match maxArgs, __do_lift with | maxArgs'.succ, fn.app arg => do let acc ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn (Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs maxArgs' xf xa) Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg (xa acc) | x, x_1 => xf WARNING: Failed to calculate equational lemmata for Lean.Elab.Term.mkCoe: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) WARNING: Failed to calculate equational lemmata for Lean.Meta.Grind.pushNot: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats ` to set the limit.(invalid MessageData.lazy, missing context) Some required targets logged failures: - Mathlib.Tactic.Linter.Header - Batteries.Linter.UnreachableTactic - Batteries.Lean.Meta.UnusedNames - Batteries.Linter.UnnecessarySeqFocus - Batteries.Data.String.Matcher error: build failed