test failure due to warning: manifest out of date

Stream: nightly-testing

[Joachim Breitner]

The mathlib lean pr CI test at https://github.com/leanprover-community/mathlib4/actions/runs/9349390412/job/25730574569 fails with

warning: manifest out of date: git revision of dependency 'batteries' changed; use `lake update batteries` to update it
Test succeeded with noisy output: ./test/Inhabit.lean

which seems unrelated to my PR. Is this already on anyone's radar?

[Kim Morrison]

Ah, I had noticed this, but not fixed it. It is a combination of stricter testing of noisy-ness at Mathlib, and the fact that we had been updating the require statement in mathlib lean-pr-testing-NNNN branches, but without running lake update.

lean#4333 should hopefully address the later. (Although it is a bit scary running lake update in automation!)

[Kim Morrison]

I think I will also adjust Mathlib's testing framework so manifest out of date warnings don't cause tests to fail.

[Kim Morrison]

batteries#818

[Kim Morrison]

And addressing this from yet another direction, let's run lake update on the nightly-testing branch automatically: #13488

[Kim Morrison]

And #13489 will start Mathlib regularly updating its dependencies (via a PR, which will stay open if it fails, thereby blocking future automatic updates). I've been wanting this for a while, as I think I do the majority of lake updates in Mathlib still, and would like to not! :-)

[Kim Morrison]

And this has been updated to post on zulip about failures, too.