ProofWidgets not building, says it is out of date

Stream: mathlib4

[Serena]

I am trying to install Mathlib4 and ProofWidgets is causing it not to build. The error it gives is

✖ [418/453] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.

System: Ubuntu 24.04 x86_64
Lake version 5.0.0-src+744f980 (Lean version 4.25.0-rc2)

Things I have tried:

• Ran lake exe cache get
• Ran lake exe cache get!
• Deleted ~/.cache/mathlib4
• Deleted .lake
• Deleted lake-manifest.json

I am at a loss of how to solve this issue, any help would be appreciated!

[Alexandre Rademaker]

The problem is that the message doesn’t really explain what’s going on. What actually happens when we run lake exe cache get? And why isn’t this solving the problem? I’d like to better understand the step-by-step process of lake build and how lake exe cache get runs. Unfortunately, using -v with the build doesn’t give me more detailed information.

[Anthony Wang]

I'm also getting the same error. lake build -v produces these lines which might be related:

✔ [609/832] Ran proofwidgets:extraDep
✔ [610/832] Ran widgetJsSrcs
✔ [611/832] Ran widgetRollupConfig
✔ [612/832] Ran widgetTsconfig
✔ [613/832] Ran widgetPackageJson
ℹ [614/832] Replayed proofwidgets/widgetPackageLock
trace: ././widget> npm install
trace: stdout:
added 1 package, changed 2 packages, and audited 367 packages in 2s

67 packages are looking for funding
  run `npm fund` for details

1 moderate severity vulnerability

To address all issues, run:
  npm audit fix

Run `npm audit` for details.
✖ [615/832] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.
✔ [616/832] Ran ProofWidgets.Compat
✔ [617/832] Ran ProofWidgets.Component.Basic
✔ [618/832] Ran ProofWidgets.Component.MakeEditLink
✔ [619/832] Ran ProofWidgets.Util
✔ [620/832] Ran ProofWidgets.Data.Html
✔ [621/832] Ran ProofWidgets.Cancellable
✔ [622/832] Ran ProofWidgets.Component.OfRpcMethod

[Anthony Wang]

Hmmm, I was able to get around the error by going into the .lake/packages/proofwidgets directory and running lake build manually, which succeeds. Then the error no longer appears when building mathlib.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Serena what is the output of lake exe cache get?

[Kim Morrison]

It's really important with these sort of issues that you give a reproducible example. This should be in the form of a github repository, and a particular commit in it, where this error appears, and lake exe cache get does not resolve it.

If we can't actually reproduce the behaviour locally it's very difficult to diagnose/fix.

[Serena]

@Kim Morrison Clean your cache, redownload mathlib and build it. It won't work. Those are the steps. I doubt a github repo would help here, unless you want me to commit the entirety of Lean's build chain and artifacts, which probably won't run on your computer anyway.

@𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 it says that everything is up to date.

@Anthony Wang This is a good idea, I will try it out later!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Could you say which mathlib commit this is on?

[Kevin Buzzard]

@Serena I cannot reproduce -- can you give more information?

buzzard@IC-HWDXTW69VR ~ % mkdir test
buzzard@IC-HWDXTW69VR ~ % cd test
buzzard@IC-HWDXTW69VR test % git clone git@github.com:leanprover-community/mathlib4.git
Cloning into 'mathlib4'...
remote: Enumerating objects: 771858, done.
remote: Counting objects: 100% (701/701), done.
remote: Compressing objects: 100% (331/331), done.
remote: Total 771858 (delta 512), reused 370 (delta 370), pack-reused 771157 (from 3)
Receiving objects: 100% (771858/771858), 387.24 MiB | 2.79 MiB/s, done.
Resolving deltas: 100% (630182/630182), done.
Updating files: 100% (7747/7747), done.
buzzard@IC-HWDXTW69VR test % cd mathlib4
buzzard@IC-HWDXTW69VR mathlib4 % git rev-parse HEAD
7f4ff1fc4b149411439808e577496e0eb7106f1e
buzzard@IC-HWDXTW69VR mathlib4 % lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '156c416202d8afc1c2ff45ceb4d42ac9b9ecf089'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '451499ea6e97cee4c8979b507a9af5581a849161'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'ca519018e8bdc34d7bb4ecf0c8d39634a8c15300'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '95c2f8afe09d9e49d3cacca667261da04f7f93f7'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '091ff2379c7f0998aba1dc031a578810d44b9f3f'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '72ae7004d9f0ddb422aec5378204fdd7828c5672'
Fetching ProofWidgets cloud release... done!
Current branch: master
Using cache (Azure) from origin: leanprover-community/mathlib4
Attempting to download 7506 file(s) from leanprover-community/mathlib4 cache
Downloaded: 7506 file(s) [attempted 7506/7506 = 100%, 58 KB/s]
Decompressing 7506 file(s)
Unpacked in 4540 ms
Completed successfully!
buzzard@IC-HWDXTW69VR mathlib4 % rm -rf .lake
buzzard@IC-HWDXTW69VR mathlib4 % lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '156c416202d8afc1c2ff45ceb4d42ac9b9ecf089'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '451499ea6e97cee4c8979b507a9af5581a849161'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'ca519018e8bdc34d7bb4ecf0c8d39634a8c15300'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '95c2f8afe09d9e49d3cacca667261da04f7f93f7'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '091ff2379c7f0998aba1dc031a578810d44b9f3f'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '72ae7004d9f0ddb422aec5378204fdd7828c5672'
Fetching ProofWidgets cloud release... done!
Current branch: master
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7506 file(s)
Unpacked in 3917 ms
Completed successfully!
buzzard@IC-HWDXTW69VR mathlib4 %

[Anthony Wang]

I created a repo that reproduces this bug:

git clone https://git.unnamed.website/leantest/
lake exe cache get
lake build

See https://git.unnamed.website/leantest/tree/lake-manifest.json for the commits of mathlib and ProofWidgets that are causing this bug.

[Anthony Wang]

Interestingly, this error only happens when running lake build in the directory of a project that uses mathlib, not when running lake build in the mathlib directory itself.

[Kevin Buzzard]

I'm having no problems with lake exe new math out of the box:

buzzard@brutus:~$ mkdir test
buzzard@brutus:~$ cd test
buzzard@brutus:~/test$ lake new MyProject math
info: downloading mathlib `lean-toolchain` file
info: MyProject: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision 'cb325b2bde7b60c717581d42c60fc405afb77169'
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '009064c21bad4d7f421f2901c5e817c8bf3468cb'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '2781d8ad404303b2fe03710ac7db946ddfe3539f'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '7b346ae32fa3752c1c484082b6ba91903efbe215'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '1dae8b12f8ba27576ffe5ddee78bebf6458157b0'
info: mathlib: running post-update hooks
Not running `lake exe cache get` yet, as the `lake` version does not match the toolchain version in the project.
You should run `lake exe cache get` manually.
buzzard@brutus:~/test$ cd MyProject/
buzzard@brutus:~/test/MyProject$ more MyProject.lean
import MyProject.Basic
buzzard@brutus:~/test/MyProject$ cat > MyProject/Basic.lean
import Mathlib
#check (2 : Nat)
buzzard@brutus:~/test/MyProject$ lake exe cache get
Fetching ProofWidgets cloud release... done!
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7507 file(s)
Unpacked in 4313 ms
Completed successfully!
buzzard@brutus:~/test/MyProject$ lake build
[7523/7525] Built MyProject.Basic
info: MyProject/Basic.lean:2:0: 2 : ℕ
Build completed successfully (7525 jobs).
buzzard@brutus:~/test/MyProject$

How did you make this project? Did you use a nonstandard technique? Do you have some version mismatch with various repos?

FWIW my lakefile.toml is

name = "MyProject"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["MyProject"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[lean_lib]]
name = "MyProject"

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Kevin Buzzard they are using the v4.25.0 tagged release of mathlib. It is reasonable to expect that to work. I can reproduce it not working.

[Kevin Buzzard]

OK great :-) Then we are making progress!

Edit: see #mathlib4 > Building proofwidgets/widgetJsAll failed for v4.25.0 @ 💬 for another user with this problem (but let's talk about it here)

[Jovan Gerbscheid]

I also encountered this problem yesterday, when checking out some mathlib PR (the PR was still on v4.24.0-rc1). I tried to do rm -rf .lake followed by lake exe cache get. This didn't fix it yet, but when I tried the commands again, it did get fixed.

What I found extremely suspicious was that after I cleared the .lake folder, and then got the cache again, lake warned me that my ProofWidgets package had local changes. Which is ridiculous, because it had just downloaded a fresh copy.

[Yaël Dillies]

I too am hitting this issue when bumping Toric. Could we please move this discussion out of #new members ? This is a critical issue

[Ruben Van de Velde]

Not hitting it while bumping here, fwiw

[Notification Bot]

This topic was moved here from #new members > ProofWidgets not building, says it is out of date by Kevin Buzzard.

[Yaël Dillies]

Here's a tentative reproduction:

1. Clone https://github.com/YaelDillies/Toric
2. Add rev = "v4.25.0" in the lakefile for the mathlib dependency
3. Run lake update
4. Run lake exe cache get. It fetches 680/7500 files, or something like that
5. Run lake build. It starts building batteries

[pandaman]

Same issue with https://github.com/pandaman64/program-verifications/. Reproduced across Linux/MacOS.

Logs

pandaman@pop-os:~$ git clone https://github.com/pandaman64/program-verifications program-verifications2
Cloning into 'program-verifications2'...
remote: Enumerating objects: 92, done.
remote: Counting objects: 100% (92/92), done.
remote: Compressing objects: 100% (51/51), done.
remote: Total 92 (delta 40), reused 84 (delta 32), pack-reused 0 (from 0)
Receiving objects: 100% (92/92), 24.32 KiB | 12.16 MiB/s, done.
Resolving deltas: 100% (40/40), done.
pandaman@pop-os:~$ cd program-verifications2
pandaman@pop-os:~/program-verifications2$ vim lakefile.toml # update rev to v4.25.0
pandaman@pop-os:~/program-verifications2$ lake update
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision '029db123ddaa7f8fd0d18cea3b1b33bf84dacd1e'
info: updating toolchain to 'leanprover/lean4:v4.25.0'
info: restarting Lake via Elan
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '009064c21bad4d7f421f2901c5e817c8bf3468cb'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '2781d8ad404303b2fe03710ac7db946ddfe3539f'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '39260e31b7b3f7f05643da95242463b462dc05f1'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '1dae8b12f8ba27576ffe5ddee78bebf6458157b0'
info: mathlib: running post-update hooks
Not running lake exe cache get yet, as the lake version does not match the toolchain version in the project.
You should run lake exe cache get manually.
pandaman@pop-os:~/program-verifications2$ lake exe cache ^C
pandaman@pop-os:~/program-verifications2$ cat lean-toolchain
leanprover/lean4:v4.25.0pandaman@pop-os:~/program-verifications2$ lake exe cache get
Fetching ProofWidgets cloud release... done!
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7506 file(s)
Unpacked in 9412 ms
Completed successfully!
pandaman@pop-os:~/program-verifications2$ lake build
✖ [619/1228] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run lake exe cache get to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.
⡿ [7553/11014] Running Batteries.Control.Lemmas:c.o (+ 15 more)^C

[Jovan Gerbscheid]

Note that it's likely not an issue with v4.25.0 specifically, because I only installed that toolchain today, before encountering this issue yesterday.

[Stefan Kusterer]

Hello,
For what I see, the problem is linked to v4.25.0.
The code in lean-math-puzzles, which uses v4.24.0, can be built without problem.
When switching to v4.25.0, lake build breaks with

✖ [566/660] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.
Some required targets logged failures:
- proofwidgets/widgetJsAll
error: build failed

For reproducing, please follow these steps:

• git clone git@github.com:runbikeswim/lean-math-puzzles.git
• cd lean-math-puzzles/
• sed 's/v4.24.0/v4.25.0/g' lakefile.toml > lakefile.toml.2
• mv -f lakefile.toml.2 lakefile.toml
• lake update
• lake exe cache get
• lake build

I ran lake build -v after that and got

ℹ [6263/6278] Replayed Mathlib.Tactic.Sat.FromLRAT:c.o (with exports)
trace: .> /home/stefan/.elan/toolchains/leanprover--lean4---v4.25.0/bin/clang -c -o /home/stefan/Tests/lean-math-puzzles/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Sat/FromLRAT.c.o.export /home/stefan/Tests/lean-math-puzzles/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Sat/FromLRAT.c -I /home/stefan/.elan/toolchains/leanprover--lean4---v4.25.0/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /home/stefan/.elan/toolchains/leanprover--lean4---v4.25.0 -nostdinc -isystem /home/stefan/.elan/toolchains/leanprover--lean4---v4.25.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
Some required targets logged failures:
- proofwidgets/widgetJsAll
error: build failed

as final message.

I'm using the following environment:

• Linux ■■■■■■■■■ 6.6.87.2-microsoft-standard-WSL2 #1 SMP PREEMPT_DYNAMIC Thu Jun 5 18:30:46 UTC 2025 x86_64 x86_64 x86_64 GNU/Linux
• elan 4.1.2 (58e8d545e 2025-05-26)
• Lake version 5.0.0-src+cdd38ac (Lean version 4.25.0)

[Kim Morrison]

Sorry, this is my fault.

When I moved Mathlib to v4.25.0, I forgot to increment the ProofWidgets release version from v0.0.77.

I've fixed this in #31720, which I've also put on the queue.

I'm also now deleting the Mathlib v4.25.0 tag, as it is not useful, and the best option is simply to replace. (I'll do this after #31720 is in place.)

I'm now preparing a PR which will modify Mathlib CI to prevent this accidentally happening again.

[Kim Morrison]

#31723 (this will hopefully fail until #31720 is merged)

[Kim Morrison]

See also cslib#159 and repl#135.

[Kim Morrison]

:warning: I have replaced the v4.25.0 tag of Mathlib now.

[Kim Morrison]

@topic, if everyone who had experienced problems could please try again, and report back here, that would be very helpful.

[Stefan Kusterer]

Hello @Kim Morrison ,
Sorry for the bad news ... I still see the same error as before.
To be sure, I started with a fresh clone of https://github.com/runbikeswim/lean-math-puzzles.
Without changing to v4.25.0 and running lake build on v4.24.0 as is, there is no problem.
I'm also not asked to run lake exe cache get.
After replacing v4.24.0 with v4.25.0 in the lakefile.toml, the build breaks with exactly the same error as before.
I also checked PR #31720: Since it is closed, I trust that lake update provides me with a version of mathlib4 that has your changes in.
You should be able to see the same, if you follow the steps described in my post from yesterday.
Hope this helps.
Kind Regards, Stefan

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Kim Morrison the target that is failing, widgetJsAll, does not depend on Lean; it's only JS stuff. So I would guess it's not the Lean version mismatch.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

This is difficult to debug, but here is something curious I noticed on the leantest repo linked above. This is with lake-manifest regenerated to use the new v4.25.0 tag of mathlib.

~/leantest/ > lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision '1ccd71f89cbbd82ae7d097723ce1722ca7b01c33'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '009064c21bad4d7f421f2901c5e817c8bf3468cb'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '2781d8ad404303b2fe03710ac7db946ddfe3539f'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '5c78955e8375f872c085514cb521216bac1bda17'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '1dae8b12f8ba27576ffe5ddee78bebf6458157b0'
Fetching ProofWidgets cloud release... done!
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7525 file(s)
Unpacked in 4016 ms
Completed successfully!
~/leantest/ > cat .lake/packages/proofwidgets/widget/package-lock.json.hash
cat: .lake/packages/proofwidgets/widget/package-lock.json.hash: No such file or directory
~/leantest/ > lake build
✖ [619/1268] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.
⣷ [7547/7557] Running Batteries.Classes.RatCast:c.o (+ 10 more)^C
~/leantest/ > cat .lake/packages/proofwidgets/widget/package-lock.json.hash
b782184005d5892a%
~/leantest/ > rm .lake/packages/proofwidgets/widget/package-lock.json.hash
~/leantest/ > lake build proofwidgets
Build completed successfully (27 jobs).
~/leantest/ > cat .lake/packages/proofwidgets/widget/package-lock.json.hash
0186e1ad4f7ac1f8%

Notice that the two hashes are different. Is that supposed to happen @Mac Malone ?

[Jovan Gerbscheid]

On my mathlib PRs (e.g. #31740), CI is now failing with:

❌ Error: Lean toolchain mismatch!
  Main lean-toolchain: leanprover/lean4:v4.25.0
  ProofWidgets lean-toolchain: leanprover/lean4:v4.25.0-rc1

[Yaël Dillies]

Some, but not all, of my PRs fail the same way

[Jovan Gerbscheid]

It seems that this is fixed by merging master

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ok, bug report filed at lean4#11209. I'm afraid this will have to wait for a fix in core.

[Kevin Buzzard]

Great debugging work! Thanks!

[Kim Morrison]

We have a fix landed, and v4.25.1 is on its way shortly.

[Stefan Kusterer]

Checked with v4.25.1: the issue is gone, lake build works flawlessly in this version.
Thanks to everybody involved for their support.