batteries#784

Stream: batteries

[Kim Morrison]

Ah -- @Joachim Breitner had prepared a Mathlib adaptation branch for batteries#784, but then @Mario Carneiro revised it and the adaptations are all incorrect.

As a result the last attempt to bump, on branch#bump_Std_2024-05-10 (oops, I better get used to calling it batteries!) isn't working.

[Kim Morrison]

If anyone wants to take a look at this?

[Mario Carneiro]

maybe we need a bot for tracking the status of batteries->mathlib bump PRs?

[Kim Morrison]

Indeed: @Joachim Breitner even named the adaptation branch batteries-pr-testing-784, imagining that future world. :-)

[Mario Carneiro]

can you push a commit to the PR even if it's broken? It seems like there aren't any caches ready yet

[Mario Carneiro]

oh I see, you are working on the other branch

[Kim Morrison]

I'm working on bump_Std_2024-05-10 now

[Kim Morrison]

(well, I'm working on diagnosing breakages in mathlib from lean#4119, but that's where I last pushed to)

[Mario Carneiro]

ok I'll push some fixes to that branch

[Mario Carneiro]

pushed

[Kim Morrison]

Looks great, thanks!