[Merged by Bors] - chore: complete ProofWidgets bump

[PatrickMassot]

---

See discussion on Zulip

[alexjbest]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alexjbest.

[RemyDegenne]

bors r+

[bors]

Build failed (retrying...):

• Build

[bors]

Canceled.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style

[dwrensha]

After this commit, the mathlib cache seems to no longer work for me:

$ git checkout ae7a2e405 
$ git clean -xffd
$ lake exe cache get
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
info: Downloading proofwidgets/v0.0.15/linux-64.tar.gz
info: Unpacking proofwidgets/v0.0.15/linux-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 1026 file(s)
Downloaded: 0 file(s) [attempted 1026/1026 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 2702 file(s)
unpacked in 1529 ms

$ lake build
[2/5] Building Mathlib.Tactic.PPWithUniv
...
[111/261] Building Mathlib.Tactic.Classical
[119/271] Building Mathlib.Util.AssertExists
[121/274] Building Mathlib.Init.Data.Fin.Basic
[127/274] Building Mathlib.Lean.Expr.Basic
[127/274] Building Mathlib.Tactic.PermuteGoals
[142/379] Building Mathlib.Tactic.Use
[142/380] Building Mathlib.Lean.Meta
[142/380] Building Mathlib.Tactic.GCongr.ForwardAttr
[154/460] Building Mathlib.Tactic.NthRewrite
...
[180/3726] Building Mathlib.Data.Buffer.Parser.Basic
[181/3726] Building Mathlib.Data.Buffer.Parser.Numeral
[183/3726] Building Mathlib.Lean.IO.Process
[183/3726] Building Mathlib.Lean.LocalContext
... (full rebuild )