[Merged by Bors] - chore: CI detects ProofWidgets toolchain mismatch

[kim-em]

See zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/ProofWidgets.20not.20building.2C.20says.20it.20is.20out.20of.20date/near/556720459

Ideally, this would fail right now, demonstrating that it is working, but of course CI only runs from the master version.

Update: now that #31720 is in, this can be merged.

[github-actions]

PR summary 015b41b4dc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[bryangingechen]

Naïve question: Is proofwidgets the only dependency where this sort of thing needs to be checked? Could this happen with another new dependency that we add in the future?

[kim-em]

Naïve question: Is proofwidgets the only dependency where this sort of thing needs to be checked? Could this happen with another new dependency that we add in the future?

So far it is only ProofWidgets, which does some shenanigans that I don't fully understand to retrieve precompiled artifacts so we don't need node installed to build Mathlib.

It's possible that Canonical will have similar difficulties if we ever manage to add that to Mathlib.

[bryangingechen]

I just checked a recent commit of mathlib4 master and other than proofwidgets, it looks like LeanSearchClient is also on v4.25.0-rc1. I'm guessing it doesn't matter there and it'd be too strict for us to demand that all .lake/packages/*/lean-toolchain agree with lean-toolchain?

[kim-em]

I just checked a recent commit of mathlib4 master and other than proofwidgets, it looks like LeanSearchClient is also on v4.25.0-rc1. I'm guessing it doesn't matter there and it'd be too strict for us to demand that all .lake/packages/*/lean-toolchain agree with lean-toolchain?

Yes, it would be a pain if the really minor libraries that don't depend on much Lean API needed to be bumped every release as well.

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step