Zulip Chat Archive

Hello, I was following the instructions to update Mathlib. I was in mathematics_in_lean folder obtained from git. Then I copied and pasted curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain to update the lean-toolchain file. It's the next step that failed. When I ran lake update, heres what I got:

info: toolchain not updated; already up-to-date
warning: /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/lakefile.lean:160:13: Lake.Package.name has been deprecated: Use baseName, keyName, or prettyName instead
warning: /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/lakefile.lean:160:24: Lake.Package.name has been deprecated: Use baseName, keyName, or prettyName instead
warning: /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/lakefile.lean:166:20: Lake.Package.name has been deprecated: Use baseName, keyName, or prettyName instead
warning: proofwidgets: repository '/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/proofwidgets' has local changes
info: mathlib: running post-update hooks
⚠ [3/19] Replayed Batteries.Data.Array.Match
warning: Batteries/Data/Array/Match.lean:58: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.
warning: Batteries/Data/Array/Match.lean:64:43: Stream has been deprecated: Use Std.Stream instead

Note: The updated constant has a different type:

Type u → outParam (Type v) → Type (max u v)

instead of

Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)
warning: Batteries/Data/Array/Match.lean:85:30: Stream has been deprecated: Use Std.Stream instead

Note: The updated constant has a different type:

Type u → outParam (Type v) → Type (max u v)

instead of

Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)
warning: Batteries/Data/Array/Match.lean:93:35: Stream has been deprecated: Use Std.Stream instead

Note: The updated constant has a different type:

Type u → outParam (Type v) → Type (max u v)

instead of

Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)
✖ [5/19] Building Cache.Lean
trace: .> LEAN_PATH=/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/Cli/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/batteries/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/Qq/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/aesop/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/importGraph/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/plausible/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/build/lib/lean /Users/Patron/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/Cache/Lean.lean -o /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Lean.olean -i /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Lean.ilean -c /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.c --setup /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.setup.json --json
error: Cache/Lean.lean:7:0: object file '/Users/Patron/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean/Lean/Util/Paths.olean' of module Lean.Util.Paths does not exist
error: Lean exited with code 1
✖ [11/19] Building Batteries.Data.String.Basic
trace: .> LEAN_PATH=/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/Cli/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/batteries/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/Qq/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/aesop/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/importGraph/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/plausible/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/mathlib/.lake/build/lib/lean:/Users/Patron/Documents/mylean/mathematics_in_lean/.lake/build/lib/lean /Users/Patron/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/batteries/Batteries/Data/String/Basic.lean -o /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.olean -i /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.ilean -c /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.c --setup /Users/Patron/Documents/mylean/mathematics_in_lean/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.setup.json --json
warning: Batteries/Data/String/Basic.lean:7:22: Substring has been deprecated: Use Substring.Raw instead
warning: Batteries/Data/String/Basic.lean:7:36: String.toSubstring has been deprecated: Use String.toRawSubstring instead
error: Batteries/Data/String/Basic.lean:28:12: type expected, got