Having trouble updating Paperproof #65
Description
Whenever I try to run "lake update Paperproof I get this:
info: toolchain not updated; already up-to-date
warning: proofwidgets: repository 'C:\Users\dwals\Programs\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: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)
⚠ [4/19] Replayed Batteries.Data.String.Basic
warning: Batteries/Data/String/Basic.lean:28:12: String.Pos has been deprecated: Use String.Pos.Raw instead
Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from x.Pos to Pos.Raw x).
warning: Batteries/Data/String/Basic.lean:29:11: String.atEnd has been deprecated: Use String.Pos.Raw.atEnd instead
Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from x.atEnd to Pos.Raw.atEnd x).
warning: Batteries/Data/String/Basic.lean:30:13: String.get has been deprecated: Use String.Pos.Raw.get instead
Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from x.get to Pos.Raw.get x).
warning: Batteries/Data/String/Basic.lean:31:29: String.next has been deprecated: Use String.Pos.Raw.next instead
Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from x.next to Pos.Raw.next x).
warning: Batteries/Data/String/Basic.lean:34:10: String.next has been deprecated: Use String.Pos.Raw.next instead
Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from x.next to Pos.Raw.next x).
✖ [9/19] Building Cache.Lean
trace: .> LEAN_PATH=C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\Cli.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\batteries.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\Qq.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\aesop.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\proofwidgets.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\importGraph.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\LeanSearchClient.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\plausible.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\mathlib.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\Paperproof\lean.lake\build\lib\lean;C:\Users\dwals\Programs\mathematics_in_lean.lake\build\lib\lean c:\Users\dwals.elan\toolchains\leanprover--lean4---v4.25.0-rc2\bin\lean.exe C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\mathlib\Cache\Lean.lean -o C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\mathlib.lake\build\lib\lean\Cache\Lean.olean -i C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\mathlib.lake\build\lib\lean\Cache\Lean.ilean -c C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\mathlib.lake\build\ir\Cache\Lean.c --setup C:\Users\dwals\Programs\mathematics_in_lean.lake\packages\mathlib.lake\build\ir\Cache\Lean.setup.json --json
error: Cache/Lean.lean:7:0: object file 'c:\Users\dwals.elan\toolchains\leanprover--lean4---v4.25.0-rc2\lib\lean\Lean\Util\Paths.olean' of module Lean.Util.Paths does not exist
error: Lean exited with code 1
Some required targets logged failures:
- Cache.Lean
error: build failed