nightly#47 adaptations for nightly-2025-08-27

Stream: nightly-testing

[Kim Morrison]

Ready for review, LGTM.

[Kevin Buzzard]

CI is failing and I am not competent to review all of the changes (in particular CI and Mathlib/Tactic; I explicitly noted which files I had not reviewed in a comment on the PR) but everything else looks fine.

[Kevin Buzzard]

Note also that the usual message which supplies a link to the PR is missing, although this doesn't bother me because I would not undertake a review on mobile, and on the app the link is available in the header of the thread.

[Kim Morrison]

Kevin Buzzard said:

Note also that the usual message which supplies a link to the PR is missing, although this doesn't bother me because I would not undertake a review on mobile, and on the app the link is available in the header of the thread.

Yes, the automatic script broke today for slightly mysterious reasons, so I posted this myself.

[Kim Morrison]

'd, finally!