Zulip Chat Archive

  -- Found 5 errors in 3485 declarations (plus 15441 automatically generated ones) in Batteries with 13 linters

  /- The `defLemma` linter reports:
  INCORRECT DEF/LEMMA: -/
  -- Batteries.Data.LazyList
  ././././Batteries/Data/LazyList.lean:21:1: error: @LazyList.binductionOn_1 is a def, should be lemma/theorem

  /- The `docBlame` linter reports:
  DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
  -- Batteries.Data.LazyList
  ././././Batteries/Data/LazyList.lean:21:1: error: @LazyList.below_1 definition missing documentation string
  ././././Batteries/Data/LazyList.lean:21:1: error: @LazyList.ibelow_1 definition missing documentation string
  ././././Batteries/Data/LazyList.lean:21:1: error: @LazyList.binductionOn_1 definition missing documentation string
  ././././Batteries/Data/LazyList.lean:21:1: error: @LazyList.brecOn_1 definition missing documentation string

Joachim Breitner (Jul 16 2024 at 14:31):

Yes, there is an adoption branch somewhere

Kim Morrison (Jul 16 2024 at 14:32):

Great, thanks!

Joachim Breitner (Jul 16 2024 at 14:32):

https://github.com/nomeata/batteries/tree/lean-pr-testing-4658
resp.
https://github.com/leanprover-community/batteries/commit/9cbf18e129b8721aa0841e04d89fcd36fbcf6de8

Kim Morrison (Jul 16 2024 at 14:37):

Ah! The fact that they are not on the main repo always confuses me.

Kim Morrison (Jul 16 2024 at 14:38):

I am going to give you write access on Batteries. Perhaps future lean-pr-testing-NNN branches you can push there directly?

Joachim Breitner (Jul 16 2024 at 14:38):

Yes, me too. Would it be possible to simply give everyone who can modify a lean-pr-testing-* branch on mathlib to also be able to modify such branches on batteries? (It helps me if you give me access, of course and thanks, but not the next person)

Kim Morrison (Jul 16 2024 at 14:39):

That's not really possible; there are too many, and we are trying to scale back that access in any case.

Kim Morrison (Jul 16 2024 at 14:39):

(Done.)

github mathlib4 bot (Jul 16 2024 at 14:43):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jul 16 2024 at 14:48):

#885 adaptations for nightly-2024-07-16

github mathlib4 bot (Jul 17 2024 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jul 18 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jul 18 2024 at 17:00):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jul 18 2024 at 17:03):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jul 18 2024 at 17:15):

batteries#886 adaptations for nightly-2024-07-18

github mathlib4 bot (Jul 18 2024 at 17:17):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jul 26 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jul 26 2024 at 11:12):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jul 26 2024 at 11:16):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jul 26 2024 at 11:29):

adaptations for nightly-2024-07-26 batteries#893

github mathlib4 bot (Jul 27 2024 at 09:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jul 29 2024 at 11:19):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jul 29 2024 at 11:27):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jul 29 2024 at 12:45):

chore: adaptations for nightly-2024-07-29
batteries#896

github mathlib4 bot (Jul 30 2024 at 00:16):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jul 30 2024 at 08:56):

chore: adaptations for nightly-2024-07-30 batteries#898

Kim Morrison (Jul 31 2024 at 02:46):

Note to self (or anyone): when batteries breaks tonight, merge nightly-testing-pre-2024-07-31 into nightly-testing.

github mathlib4 bot (Jul 31 2024 at 05:39):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jul 31 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Jul 31 2024 at 09:18):

Should come good shortly.

github mathlib4 bot (Jul 31 2024 at 09:20):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 01 2024 at 05:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 01 2024 at 10:31):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 05 2024 at 02:07):

batteries#906 adaptations for nightly-2024-08-03

I'll need to merge this one soon.

github mathlib4 bot (Aug 05 2024 at 02:17):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 08 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 08 2024 at 10:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 08 2024 at 10:54):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 08 2024 at 11:02):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 08 2024 at 11:27):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 08 2024 at 11:45):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 08 2024 at 11:47):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 08 2024 at 12:06):

batteries#910 (already 'd)

github mathlib4 bot (Aug 09 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 09 2024 at 10:44):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 10 2024 at 11:38):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 10 2024 at 11:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 12 2024 at 02:37):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 12 2024 at 02:37):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 12 2024 at 07:19):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 12 2024 at 07:24):

batteries#912

github mathlib4 bot (Aug 12 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 13 2024 at 00:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 13 2024 at 00:37):

batteries#913

github mathlib4 bot (Aug 13 2024 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 13 2024 at 19:34):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 14 2024 at 02:29):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 15 2024 at 23:20):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 15 2024 at 23:39):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 15 2024 at 23:40):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 16 2024 at 22:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 16 2024 at 23:05):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 16 2024 at 23:38):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 17 2024 at 00:28):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 17 2024 at 02:20):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 17 2024 at 04:15):

batteries#923 chore: adaptations for nightly-2024-08-16

github mathlib4 bot (Aug 17 2024 at 06:02):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 17 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 19 2024 at 02:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 19 2024 at 03:58):

adaptations for nightly-2024-08-17 batteries#926

github mathlib4 bot (Aug 19 2024 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 20 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 20 2024 at 12:04):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 20 2024 at 12:27):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 20 2024 at 12:33):

batteries#927

github mathlib4 bot (Aug 21 2024 at 02:46):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 22 2024 at 08:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 22 2024 at 08:20):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 22 2024 at 08:24):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 25 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 25 2024 at 09:29):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 26 2024 at 07:03):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 26 2024 at 07:05):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 27 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Aug 27 2024 at 10:38):

I've merged lean-pr-testing-5020.

Kim Morrison (Aug 27 2024 at 10:38):

oops.... just needed to merge lean-pr-testing-5147

github mathlib4 bot (Aug 27 2024 at 10:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 27 2024 at 10:48):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Aug 27 2024 at 11:02):

batteries#937

github mathlib4 bot (Aug 28 2024 at 08:44):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Aug 29 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Aug 29 2024 at 09:33):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 05 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 05 2024 at 23:18):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Sep 05 2024 at 23:51):

batteries#944

github mathlib4 bot (Sep 06 2024 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 08 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 08 2024 at 23:01):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 08 2024 at 23:05):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 09 2024 at 05:04):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 09 2024 at 05:17):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 09 2024 at 05:17):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 09 2024 at 05:18):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 09 2024 at 05:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 10 2024 at 08:42):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Sep 10 2024 at 08:45):

I miss Mathlib's long line syntax linter. :-( No fun having to wait for CI, and read line numbers.

github mathlib4 bot (Sep 10 2024 at 08:46):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Sep 10 2024 at 08:48):

batteries#946

Ruben Van de Velde (Sep 10 2024 at 11:09):

One might submit the linter to batteries :innocent:

Damiano Testa (Sep 10 2024 at 11:21):

Speaking of this, I was thinking that I am not too happy now with the file Mathlib.Tactic.Linter.Lint containing many linters (in particular the longLine one). What would you think of splitting the file up into the individual linters and similarly splitting the test files?

Damiano Testa (Sep 10 2024 at 11:22):

Besides clarity, another advantage of splitting is that the longFile (note the difference!) linter embeds the length of the file in its message, which I think is appropriate, but it does mean that editing the test file typically breaks the later messages.

github mathlib4 bot (Sep 11 2024 at 08:38):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 11 2024 at 08:40):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 12 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 12 2024 at 09:26):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Sep 12 2024 at 09:30):

batteries#947

github mathlib4 bot (Sep 13 2024 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 19 2024 at 08:27):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 19 2024 at 08:28):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 19 2024 at 08:29):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 20 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 20 2024 at 11:32):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 23 2024 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 23 2024 at 10:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 23 2024 at 10:55):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 26 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 26 2024 at 09:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 26 2024 at 10:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 26 2024 at 10:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 26 2024 at 10:14):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 26 2024 at 11:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 26 2024 at 14:18):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 26 2024 at 23:40):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 28 2024 at 18:23):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 28 2024 at 20:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 28 2024 at 23:25):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 28 2024 at 23:44):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Sep 29 2024 at 08:25):

batteries#971 is the update to 2024-09-27. I'll need this in by Tuesday to complete the release of v4.13.0.

github mathlib4 bot (Sep 29 2024 at 08:25):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Sep 30 2024 at 08:56):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 30 2024 at 09:31):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 30 2024 at 09:34):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Sep 30 2024 at 09:37):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Sep 30 2024 at 09:42):

To get this working I commented out UnionFind and HashMap.WF.

The main change is that I changed the signature of Array.modify lemmas, so that the array lookup hypothesis on the left hand side is found by unification, in lean#5536.

@Mario Carneiro, might you have a chance to look at this?

Kim Morrison (Sep 30 2024 at 09:43):

Unfortunately there is some time pressure here, as I am planning on cutting v4.13.0-rc1 from nightly-2024-10-01. The earliest that this could happen is +24 hours from now, and much more likely +36 hours before I'm ready to move Batteries + Mathlib to it.

Kim Morrison (Sep 30 2024 at 09:44):

If no one is available to do this in that time frame, this would be good to know, so I can make time to do it myself.

Kim Morrison (Sep 30 2024 at 09:46):

@François G. Dorais and @Matthew Ballard, I won't ping you on these sorts of messages going forward, this is just a heads up that if you would like to know what is going on when I ask for help repairing the parts of Batteries that Mathlib doesn't depend on, this topic is where it happens. (Unless someone asks me to do it elsewhere!)

Kim Morrison (Sep 30 2024 at 09:46):

Oh, and all the commenting out happened in e7da8aa8232793f23492830aa0a11dece54371a2, so hopefully just reverting that provides the place to start from.

Matthew Ballard (Sep 30 2024 at 12:02):

Apologies, I’m not going to have any time to look at this today.

Mario Carneiro (Sep 30 2024 at 13:03):

@Kim Morrison this looks very similar to the last issue you asked me to solve, there is a rogue List.toArray where there used to be Array.mk. Does nightly-testing have the fix you were working on already?

Mario Carneiro (Sep 30 2024 at 13:09):

@Kim Morrison Array.toList_length got renamed to Array.length_toList without a deprecation

Mario Carneiro (Sep 30 2024 at 13:12):

fixes pushed

github mathlib4 bot (Sep 30 2024 at 13:13):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Sep 30 2024 at 13:44):

Mario Carneiro said:

Kim Morrison Array.toList_length got renamed to Array.length_toList without a deprecation

There's already a intermediate rename this month, and the deprecation is in place for the name that existed as of the last release.

Kim Morrison (Sep 30 2024 at 13:44):

(I renamed from data_length to toList_length and then to length_toList. :woman_facepalming:)

Kim Morrison (Sep 30 2024 at 13:45):

Mario Carneiro said:

fixes pushed

Fantastic, thank you!

github mathlib4 bot (Oct 01 2024 at 06:09):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Oct 02 2024 at 07:16):

batteries#976 brings Batteries bump/v4.13.0 branch up to 2024-10-01.

github mathlib4 bot (Oct 02 2024 at 07:16):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 02 2024 at 10:18):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 02 2024 at 10:21):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Oct 03 2024 at 11:00):

batteries#978 brings us to nightly-2024-10-03, which will shortly become v4.13.0-rc1.

github mathlib4 bot (Oct 03 2024 at 12:14):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Mario Carneiro (Oct 06 2024 at 05:37):

Kim Morrison said:

Mario Carneiro said:

Kim Morrison Array.toList_length got renamed to Array.length_toList without a deprecation

There's already a intermediate rename this month, and the deprecation is in place for the name that existed as of the last release.

@Kim Morrison Caught another missed deprecation in the field: Array.data to Array.toList itself! All the theorems are aliased but not the function itself.

github mathlib4 bot (Oct 07 2024 at 16:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Oct 13 2024 at 11:21):

Mario Carneiro said:

Kim Morrison said:

Mario Carneiro said:

Kim Morrison Array.toList_length got renamed to Array.length_toList without a deprecation

There's already a intermediate rename this month, and the deprecation is in place for the name that existed as of the last release.

Kim Morrison Caught another missed deprecation in the field: Array.data to Array.toList itself! All the theorems are aliased but not the function itself.

lean#5687

github mathlib4 bot (Oct 14 2024 at 04:05):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 15 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 15 2024 at 10:16):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 15 2024 at 10:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 16 2024 at 04:37):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 16 2024 at 04:44):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 16 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 16 2024 at 09:28):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 16 2024 at 11:04):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 16 2024 at 11:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 17 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 17 2024 at 10:36):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 17 2024 at 10:38):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 17 2024 at 10:38):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Oct 17 2024 at 10:38):

I've commented out HashMap.WF again, as it is broken on nightly-testing. I think this is changes from lean#5323. I did merge lean-pr-testing-5323, which fixed some problems, but not the ones in HashMap.WF.

Pinging @Henrik Böving and @Mario Carneiro, but otherwise moving on for now.

Henrik Böving (Oct 17 2024 at 11:05):

Interesting given that this built before...

Henrik Böving (Oct 17 2024 at 11:07):

This doesn't look like any errors that I encountered while working on the UInt stuff, might be an interaction with some other changes don't know.

Kim Morrison (Oct 17 2024 at 11:08):

Okay, hopefully Mario can take a look. It's not urgent, as nothing uses HashMap.WF anymore, so we have ~2 weeks to get it right. :-)

Kim Morrison (Oct 17 2024 at 11:09):

Hopefully the discussion at https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Unifying.20.60Batteries.2EHashMap.60.20and.20.60Std.2EHashMap.60.2E/near/477103618 will eventually get us out of needing to do this!

github mathlib4 bot (Oct 17 2024 at 11:43):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Mario Carneiro (Oct 18 2024 at 00:16):

@Kim Morrison Why is Nat.sum in core to begin with? That function was supposed to stay in batteries, not be upstreamed and then deprecate removed

Mario Carneiro (Oct 18 2024 at 00:19):

pushed a fix for the HashMap.WF stuff

Mario Carneiro (Oct 18 2024 at 00:21):

Note that the reason Nat.sum exists is because you need a monoid class to prove stuff about List.sum

Mario Carneiro (Oct 18 2024 at 00:22):

I am not sure what you want to do to replace Nat.sum_append if you are deprecating Nat.sum

Kim Morrison (Oct 18 2024 at 01:23):

One can prove lemmas about a List.sum (α := Nat) rather than using Nat.sum. I initially needed to move Nat.sum up, because there are many theorems about lists that need to talk about sums of natural numbers. However I then realised both that it was causing unnecessary duplication (we ended up have copies of lemmas, stated in Lean using Nat.sum and then repeated with List.sum in Mathlib), and that List.sum suffices (note that Nat.sum is no longer mentioned in Mathlib). If you'd like a Nat.sum restored in Batteries we can do that.

Mario Carneiro (Oct 18 2024 at 01:24):

What are you using Nat.sum/List.sum for in core?

Mario Carneiro (Oct 18 2024 at 01:25):

Obviously mathlib has no need for Nat.sum, it has actual finite sums

Mario Carneiro (Oct 18 2024 at 01:26):

One can prove lemmas about a List.sum (α := Nat) rather than using Nat.sum.

I don't think we have any precedent for doing that. Once you start using typeclasses you have to be consistent about it

Kim Morrison (Oct 18 2024 at 01:28):

Mario Carneiro said:

pushed a fix for the HashMap.WF stuff

Where did you push this? I don't see it on nightly-testing.

Mario Carneiro (Oct 18 2024 at 01:29):

oops, push failed, it should be up now

github mathlib4 bot (Oct 18 2024 at 01:29):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Mario Carneiro (Oct 18 2024 at 01:30):

(we ended up have copies of lemmas, stated in Lean using Nat.sum and then repeated with List.sum in Mathlib),

This is expected, most of the API of Nat has this characteristic. We decided a while ago that it's an okay level of duplication to have a basic API for Nat/Int/Rat in batteries (now mostly upstreamed to core) and redo it with the algebraic hierarchy in mathlib, so that so that people who don't want to take on the costs of mathlib's alg. hierarchy aren't completely without tools to prove things

Kim Morrison (Oct 18 2024 at 01:32):

batteries#1000 chore: adaptations up to nightly-2024-10-17

This is a PR to bump/v4.14.0. (Apologies for taking the nice round number!)

Mario Carneiro (Oct 18 2024 at 01:33):

List.sum also has the issue that for a nonassociative operation the order matters, there is not one unique obvious option, so the naming is arguably too general

Kim Morrison (Oct 18 2024 at 01:34):

Yes, there was a problem that List.sum used to use foldl while Nat.sum used foldr. List.sum was switched to foldr a week or two ago.

Mario Carneiro (Oct 18 2024 at 01:35):

maybe it should be suml and sumr?

François G. Dorais (Oct 18 2024 at 06:39):

Should we resurrect batteries#535?

Kim Morrison (Oct 18 2024 at 07:55):

I don't see any pressing need.

github mathlib4 bot (Oct 18 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 18 2024 at 09:14):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 18 2024 at 09:14):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 18 2024 at 09:34):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Oct 18 2024 at 09:35):

I'll wait to post the nightly-2024-10-18 adaptation PR so reviewers can look at #1000 first.

Kim Morrison (Oct 18 2024 at 09:36):

(Because these are PRs to bump/v4.14.0, which needs to have origin/main periodically merged into it, only one such PR can reliably be in flight at a time.)

Ruben Van de Velde (Oct 18 2024 at 09:38):

batteries#1000

github mathlib4 bot (Oct 18 2024 at 20:45):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 19 2024 at 09:05):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 19 2024 at 09:21):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 21 2024 at 10:13):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 21 2024 at 10:17):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 21 2024 at 10:20):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Oct 21 2024 at 10:25):

batteries#1004: adaptations for nightly-2024-10-21

github mathlib4 bot (Oct 21 2024 at 10:26):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 22 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 22 2024 at 09:30):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 22 2024 at 09:33):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 24 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 24 2024 at 09:58):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Oct 30 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 30 2024 at 09:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Oct 30 2024 at 09:56):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Oct 31 2024 at 00:38):

adaptations for nightly-2024-10-18 thru 2024-10-30 batteries#1020

github mathlib4 bot (Oct 31 2024 at 00:38):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 01 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 01 2024 at 09:43):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 01 2024 at 09:45):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 01 2024 at 09:53):

I'm going to go merge batteries#1020 now, so I can prepare the next PR.

Kim Morrison (Nov 01 2024 at 10:20):

adaptations for nightly-2024-11-01 batteries#1022

github mathlib4 bot (Nov 02 2024 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 04 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 04 2024 at 09:11):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 04 2024 at 09:14):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 07 2024 at 20:56):

Hmm, Mathlib failure was due to a failure in Batteries, where are you, bot?

Kim Morrison (Nov 07 2024 at 20:57):

It seems that nightly-testing's toolchain has not been automatically bumped.

Kim Morrison (Nov 07 2024 at 21:01):

batteries#1027 adaptations for nightly-2024-11-07

github mathlib4 bot (Nov 07 2024 at 21:01):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 12 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Nov 12 2024 at 09:37):

Merging lean-pr-testing-5988

github mathlib4 bot (Nov 12 2024 at 09:38):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 12 2024 at 09:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 12 2024 at 09:52):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 12 2024 at 09:54):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 12 2024 at 09:57):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 12 2024 at 09:59):

Note that this :check: is only because I've commented out UnionFind. I'll get back to that, but if anyone else would like to do the remaining repair there that would be very helpful!

Kim Morrison (Nov 12 2024 at 10:21):

I'm out of time for today, so I'm going to leave Batteries nightly-testing branch with all of UnionFind commented out for now.

github mathlib4 bot (Nov 12 2024 at 10:26):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Mario Carneiro (Nov 12 2024 at 14:26):

fixed

github mathlib4 bot (Nov 12 2024 at 14:27):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 13 2024 at 00:17):

batteries#1040 adaptations for nightly-2024-11-12

github mathlib4 bot (Nov 13 2024 at 00:27):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 13 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Nov 13 2024 at 10:30):

merged lean-pr-testing-6054

github mathlib4 bot (Nov 13 2024 at 10:31):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Nov 13 2024 at 10:35):

Uhoh, I've broken the linter. Failures in BatteriesTest/lint_simpNF.lean. The constructor for Simp.Context is now private, and we are all meant to be using Simp.mkContext (This is lean#6054). I thought I'd successfully done that everywhere, but I've apparently broken something.

Kim Morrison (Nov 13 2024 at 10:35):

Not sure I'll have a chance to investigate it tonight.

Kim Morrison (Nov 13 2024 at 10:35):

If anyone would like to take a look, it's on nightly-testing.

Kim Morrison (Nov 13 2024 at 10:38):

Relevant diff is https://github.com/leanprover-community/batteries/compare/899b919a14070694837a6cbbab3f4fec463f0eb3...1514a1e2add9e320e49f389f389db27119cba21d

github mathlib4 bot (Nov 13 2024 at 10:44):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 13 2024 at 23:24):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Nov 14 2024 at 00:13):

Kim Morrison said:

If anyone would like to take a look, it's on nightly-testing.

All sorted, mistake on my part using the new interface, I'd dropped all the default simp lemmas...

github mathlib4 bot (Nov 14 2024 at 00:13):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 14 2024 at 02:09):

batteries#1048 adaptations for nightly-2024-11-13

github mathlib4 bot (Nov 14 2024 at 02:31):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 14 2024 at 08:51):

batteries#1049 adaptations for nightly-2024-11-14

github mathlib4 bot (Nov 15 2024 at 03:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 18 2024 at 08:39):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 18 2024 at 08:40):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 18 2024 at 09:47):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 19 2024 at 00:43):

batteries#1053 adaptations for nightly-2024-11-18

github mathlib4 bot (Nov 19 2024 at 04:30):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 19 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 19 2024 at 09:56):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 19 2024 at 10:28):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 20 2024 at 21:33):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 20 2024 at 21:38):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 20 2024 at 21:46):

This success is fake: I've commented out a bunch. I'll get back to it later, but want Mathlib up and running quickly.

github mathlib4 bot (Nov 20 2024 at 22:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 21 2024 at 00:03):

This time it is for real.

github mathlib4 bot (Nov 21 2024 at 04:43):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Nov 21 2024 at 04:45):

Haha, it wasn't actually real, I still had to rewrite some theorems. Hopefully soon.

github mathlib4 bot (Nov 21 2024 at 04:46):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 21 2024 at 04:58):

batteries#1058 adaptations for nightly-2024-11-20

github mathlib4 bot (Nov 21 2024 at 04:58):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 23 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 23 2024 at 09:43):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 24 2024 at 23:45):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 25 2024 at 00:27):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Nov 25 2024 at 00:29):

adapations for nightly-testing-2024-11-24 batteries#1064

Kim Morrison (Nov 25 2024 at 00:30):

In particular, @François G. Dorais, would you please double check the emendations I made to your recently merged changes from batteries#1062?

François G. Dorais (Nov 25 2024 at 07:22):

Thank you for cleaning up those horrible names!

github mathlib4 bot (Nov 25 2024 at 08:45):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 25 2024 at 08:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 25 2024 at 10:40):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 25 2024 at 10:47):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 26 2024 at 06:10):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 26 2024 at 06:23):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 26 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 26 2024 at 10:14):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 27 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 27 2024 at 10:58):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 27 2024 at 11:03):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 27 2024 at 11:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Nov 27 2024 at 11:36):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Nov 27 2024 at 21:10):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Dec 02 2024 at 02:45):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 02 2024 at 02:47):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Dec 02 2024 at 02:48):

batteries#1072 chore: adaptations for nightly-2024-12-01

Kim Morrison (Dec 02 2024 at 02:49):

All just upstreaming or deprecations, so I'm going to send this in. v4.15.0-rc1 is out now, based on nightly-2024-12-01.

github mathlib4 bot (Dec 02 2024 at 02:56):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Dec 03 2024 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 03 2024 at 09:18):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Dec 09 2024 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 09 2024 at 09:30):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Dec 13 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Dec 13 2024 at 21:14):

Minor problems in Batteries/Data/HashMap/WF.lean.

github mathlib4 bot (Dec 13 2024 at 21:16):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Dec 16 2024 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 17 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 18 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 19 2024 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 19 2024 at 09:55):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Dec 21 2024 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Dec 21 2024 at 10:05):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 04 2025 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 04 2025 at 20:12):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 04 2025 at 21:31):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 04 2025 at 23:25):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jan 04 2025 at 23:45):

batteries#1084 installs the reminder bot

github mathlib4 bot (Jan 04 2025 at 23:59):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jan 05 2025 at 00:11):

Hmm, bot didn't fire, secrets are probably bad.

github mathlib4 bot (Jan 05 2025 at 00:17):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

Kim Morrison (Jan 05 2025 at 00:19):

Kim Morrison said:

Hmm, bot didn't fire, secrets are probably bad.

Actually, the problem was that the reminder scripts assume that bump/v4.17.0 is on a nightly toolchain, and it wasn't. We've made that mistake repeatedly, so probably need to make the scripts more robust.

Kim Morrison (Jan 05 2025 at 00:37):

#20478

github mathlib4 bot (Jan 05 2025 at 02:56):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 06 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 06 2025 at 09:18):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 09 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 09 2025 at 13:33):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 20 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 20 2025 at 10:24):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Jan 20 2025 at 10:24):

batteries#1095

github mathlib4 bot (Jan 20 2025 at 10:26):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 21 2025 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 21 2025 at 09:18):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 29 2025 at 12:01):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 29 2025 at 12:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 29 2025 at 18:56):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 29 2025 at 22:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 30 2025 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 30 2025 at 09:34):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Jan 31 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 31 2025 at 11:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 31 2025 at 11:09):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Jan 31 2025 at 11:23):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Feb 03 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 03 2025 at 09:16):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Feb 03 2025 at 12:57):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 03 2025 at 13:04):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Feb 05 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 05 2025 at 23:25):

:check: The latest CI for Batteries' nightly-testing branch has succeeded!

github mathlib4 bot (Feb 05 2025 at 23:39):

:warning: Warning: The lean-toolchain file in the latest bump branch does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
Current content:
This needs to be fixed for the nightly testing process to work correctly.

github mathlib4 bot (Feb 05 2025 at 23:50):

Kim Morrison (Feb 06 2025 at 00:01):

This looks like a bug in the bot. The branch exists, and contains leanprover/lean4:nightly-2025-02-03

Kim Morrison (Feb 06 2025 at 00:04):

batteries#1118

github mathlib4 bot (Feb 06 2025 at 00:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! ({os.getenv('SHA')}}))

Kim Morrison (Feb 06 2025 at 00:17):

batteries#1119

github mathlib4 bot (Feb 06 2025 at 00:20):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (https://github.com/leanprover-community/batteries/commit/)

Kim Morrison (Feb 06 2025 at 00:21):

Still not there...

Kim Morrison (Feb 06 2025 at 00:30):

batteries#1120

github mathlib4 bot (Feb 06 2025 at 00:33):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f7590d0ee51b424f779c856a8166dd24b772cafb)

github mathlib4 bot (Feb 06 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (72c38de77b94808a890063525e50b233a5f62133)

github mathlib4 bot (Feb 07 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 08 2025 at 09:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 09 2025 at 06:29):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 09 2025 at 06:37):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 09 2025 at 06:39):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (25deaa9b851b602fc9788629b6c49746291e8e97)

github mathlib4 bot (Feb 09 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (fcc3faa429c1ab53c0504b076e03c852512a04e3)

github mathlib4 bot (Feb 10 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (c8369e7a76c69f728f738f85c5a4dbba838c61e2)

github mathlib4 bot (Feb 11 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (bdb06bd685f0bba45bb669e1681a63f0be61045d)

github mathlib4 bot (Feb 12 2025 at 22:33):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 12 2025 at 22:35):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (df80b107a49ce399ee9bd37d7aefeb3b8c8356ae)

github mathlib4 bot (Feb 13 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (61797027042caa3fad7c0966a74746fa8e7745e9)

github mathlib4 bot (Feb 14 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 14 2025 at 11:57):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3fd58e703603a5fd897757fcf5883c40334cf64a)

github mathlib4 bot (Feb 15 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (fae4a246720d38b45d5b0e159a461e948c9f702a)

github mathlib4 bot (Feb 16 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b6fb6c7661809c9a960bcdd9c15f48a3b14c8dfe)

github mathlib4 bot (Feb 17 2025 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 17 2025 at 11:09):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (38af7c17fedc637d6cb491d557c82ac6477a8295)

github mathlib4 bot (Feb 18 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Feb 18 2025 at 11:18):

@Mario Carneiro, I've commented out HashMap/WF.lean again. Reverting d2e5965be2c2b380ee282e34e56888d9b52cecea on nightly-testing will restore it.

github mathlib4 bot (Feb 18 2025 at 11:20):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 18 2025 at 11:20):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Feb 18 2025 at 11:22):

Sigh. I commented things out the wrong way, and it resulted in long lines... Did it again with /- -/. Now reverting 6d000e6be62be2959f86b30fa661d6b29b992761 will restore it...

github mathlib4 bot (Feb 18 2025 at 11:23):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (6d000e6be62be2959f86b30fa661d6b29b992761)

Damiano Testa (Feb 18 2025 at 12:42):

Would it help if the longLines linter allowed 102 characters, if the first 2 are --?

Yaël Dillies (Feb 18 2025 at 12:45):

It would have to be 103 since vscode inserts -- to comment out code

Mario Carneiro (Feb 18 2025 at 15:49):

@Kim Morrison is this also fixed by lean#7121?

Mario Carneiro (Feb 18 2025 at 15:57):

apparently not, I just pushed a revert + fix

github mathlib4 bot (Feb 18 2025 at 15:58):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (6d000e6be62be2959f86b30fa661d6b29b992761)

Damiano Testa (Feb 18 2025 at 19:20):

Yaël Dillies said:

It would have to be 103 since vscode inserts -- to comment out code

There is also the issue that people will realise that they can write 103 characters when the line starts with -- making this trick obsolete. There was a brief time interval where the long line linter allowed lines that were 101 characters long and people took advantage of it... :man_facepalming:

Damiano Testa (Feb 18 2025 at 19:21):

Alternatively, any line that contains http is exempt from the linter, so commenting with -- http already works without triggering the linter.

github mathlib4 bot (Feb 19 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 19 2025 at 11:10):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 19 2025 at 11:11):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (0ca4f970fb8fc2b667d13d7693657cee1cd606e5)

Damiano Testa (Feb 19 2025 at 13:48):

Damiano Testa said:

Alternatively, any line that contains http is exempt from the linter, so commenting with -- http already works without triggering the linter.

Come to think of it, I am surprised that there are no places in mathlib where a variable is called http to bypass the long line linter:

variable (http : Nat) -- now finally I can write for however long I want on this line and CI will not complain

github mathlib4 bot (Feb 20 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8688f0e92e0f63fadcd903c2362b146460fcd68c)

github mathlib4 bot (Feb 21 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (46dac121482731659f4bf26ac4c3cec6b5db8c68)

github mathlib4 bot (Feb 22 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8f4bb9e221f878e417a732a7ed7e81c1d7a7088b)

github mathlib4 bot (Feb 25 2025 at 00:21):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Feb 25 2025 at 00:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b7ef82d55a1f324f61929f60decd8bba122d75fe)

github mathlib4 bot (Feb 25 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e6768063ac23a0cd19b569f9c308b21c4eb6b3e7)

github mathlib4 bot (Feb 26 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (efb215ac6d577f364a9352977c39ecf59ea3c241)

github mathlib4 bot (Feb 27 2025 at 09:09):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (89a1884792b286e7d37ffb4ce87de2b69b2ed318)

github mathlib4 bot (Feb 28 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Ruben Van de Velde (Feb 28 2025 at 09:23):

  error: ././././Batteries/Data/ByteArray.lean:58:33: invalid argument name 'eq' for function 'Array.getElem_set_self'
  warning: ././././Batteries/Data/ByteArray.lean:62:2: `Array.get_set_ne` has been deprecated: use `Array.get_set_ne` instead

Kim Morrison (Feb 28 2025 at 22:43):

It would be lovely if the bot could post such snippets!

github mathlib4 bot (Feb 28 2025 at 23:46):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (933be6594e245f381dfe165182c928b8ef8ae168)

github mathlib4 bot (Mar 01 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (15858a2642a617a78add83f5c5ef7a83214cdeb2)

github mathlib4 bot (Mar 02 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (157ed708ea731b6814bde9eb4ee4833b58c4a8a1)

github mathlib4 bot (Mar 03 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (414fe82a12a5b238f2da252827f232285b23ed4c)

github mathlib4 bot (Mar 04 2025 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 04 2025 at 09:54):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3a21059ae64b54282d4c4a725ecdd8a7910841f0)

github mathlib4 bot (Mar 05 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (32dd37aa5235e6c9ba20a283ec18c7fbb3f86f7b)

github mathlib4 bot (Mar 06 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (60a4e4afc67318f42ff828b7b1b54bb2ae593786)

github mathlib4 bot (Mar 07 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (c59cd4772767032df97ca47d32e3f0969771e7b3)

github mathlib4 bot (Mar 08 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e62449f6672c55f439f6cf6980d02578612a0959)

github mathlib4 bot (Mar 09 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (2ef28ee8b4d886033fa9ebee0142bf05ec562873)

github mathlib4 bot (Mar 10 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e9dea218d9eddf9252b0fcbcf99896cd881acc8b)

github mathlib4 bot (Mar 11 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (c29d17e31e5f0ce872d2bbd9adb58b907b76e0f4)

github mathlib4 bot (Mar 12 2025 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 12 2025 at 13:30):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 12 2025 at 16:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (de6d1d9daebdc0b2f0055e3330000c1932ecf0a5)

github mathlib4 bot (Mar 14 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 14 2025 at 09:23):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (1b9aecc49bb859a85370756550b0eb088ee7468d)

github mathlib4 bot (Mar 15 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (49d20ab3c5b6c21537482ebe64b36cf05552d051)

github mathlib4 bot (Mar 17 2025 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 17 2025 at 12:14):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Mar 17 2025 at 12:17):

github mathlib4 bot said:

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Hmm, @Sebastian Ullrich, this test failure looks like async fallout.

Sebastian Ullrich (Mar 17 2025 at 16:17):

Ughh, another very questionable metaprogram. I fixed it.

github mathlib4 bot (Mar 17 2025 at 16:18):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Sebastian Ullrich (Mar 17 2025 at 16:22):

Oh nice I triggered a VS Code bug around read-only files

github mathlib4 bot (Mar 17 2025 at 16:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a539cf8051a319fdc7e9c121567a8f4d87931d01)

github mathlib4 bot (Mar 18 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (cbbe64e9506cf7407c0de9742bd6cf7962dc74c3)

github mathlib4 bot (Mar 19 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (886efa1fae17ed65c2bb48f6a39144e26b4cd7e4)

github mathlib4 bot (Mar 20 2025 at 22:29):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (2bbf13b69997ad2787d32b1160650e0bf5df74e5)

github mathlib4 bot (Mar 22 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (22cfb595dca0e49201694a5ade27669556e8831e)

github mathlib4 bot (Mar 24 2025 at 15:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d1f699f179eed936052df953151f26c37287e95a)

github mathlib4 bot (Mar 25 2025 at 09:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (75c92e6ed1b45fd56b915f25bd7b3d51a6af372e)

github mathlib4 bot (Mar 26 2025 at 09:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 26 2025 at 09:17):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 26 2025 at 09:19):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (96750a4310a2c9e552824fc7158ba06f710ee438)

github mathlib4 bot (Mar 27 2025 at 09:08):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 27 2025 at 09:37):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Mar 27 2025 at 09:45):

~~@Mac Malone, could you please update scripts/runLinter.lean on Batteries nightly-testing branch?~~

~~Lake.BuildInfo.libraryFacet has been deprecated, and but the suggested replacement Lake.LeanLib.facetCore is not usable as a@[match_pattern].~~

Sorry, I found the lean-pr-testing-7185 branch, thanks!

github mathlib4 bot (Mar 27 2025 at 09:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d3e2ff2195c4936a59bce988dcefcea46dedd752)

github mathlib4 bot (Mar 28 2025 at 09:42):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 28 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (30eadf68f76f3dcf634ab1a0cbcb805bd16347b2)

github mathlib4 bot (Mar 28 2025 at 10:17):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 28 2025 at 10:56):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (30eadf68f76f3dcf634ab1a0cbcb805bd16347b2)

github mathlib4 bot (Mar 30 2025 at 09:07):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (681b48efa9afe0e589e11a67b7bcc7674ad8100c)

github mathlib4 bot (Mar 30 2025 at 13:37):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (bc469dca5995c63d4c5a3480b68acbf73b7bb988)

github mathlib4 bot (Mar 31 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 31 2025 at 09:54):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (7454681e896d0ad876762bc401385ad03f53f8bc)

github mathlib4 bot (Mar 31 2025 at 10:03):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Mar 31 2025 at 10:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (7454681e896d0ad876762bc401385ad03f53f8bc)

github mathlib4 bot (Apr 01 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 01 2025 at 11:21):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (81c7d8d409fe853e8e161f887da12f71e67a4d9f)

github mathlib4 bot (Apr 02 2025 at 11:29):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (356f87dd6bb08f8e3dfecdf312902b3ba744d1ec)

github mathlib4 bot (Apr 03 2025 at 15:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 03 2025 at 23:12):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d108f3b11ec69d021a5d1c3be0f5226ebe7f73e8)

github mathlib4 bot (Apr 04 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (34bed5b0bae9a88571b29196bc6a18e977b0c870)

github mathlib4 bot (Apr 05 2025 at 09:48):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 06 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 06 2025 at 22:40):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 06 2025 at 22:41):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (76d8dbfe137870ce5f55fc8dd48fd801d996ec15)

github mathlib4 bot (Apr 07 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f561cb6e91249cba9ece253b85a4ed9f6a83461a)

github mathlib4 bot (Apr 08 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (50fa22b726602c96c8aac4cb42b531e9108ba08a)

github mathlib4 bot (Apr 09 2025 at 13:00):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (54de7fcc8fe54f6a9efa6913f82bb883b5aef428)

github mathlib4 bot (Apr 10 2025 at 08:54):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d0366f7db4449376ffe7eba14abfe7b392243a8c)

github mathlib4 bot (Apr 14 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 14 2025 at 10:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ff21e11ace28dbcebc6cf20e8035f3ac3900f3ca)

github mathlib4 bot (Apr 16 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 16 2025 at 22:23):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (106179f09644fe8e545540e4fc0cf255c29577e6)

github mathlib4 bot (Apr 17 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (Apr 17 2025 at 10:57):

Fixed by merging lean-pr-testing- branches in.

github mathlib4 bot (Apr 17 2025 at 10:59):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d957401381d91f8425e4f5dc0c1db80271680d5b)

github mathlib4 bot (Apr 18 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ccb729ea33dd69dbb11dc4fddf8fae87ba028b34)

github mathlib4 bot (Apr 19 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f35ebf8aaad822ffe52351a950272c67baea11dd)

github mathlib4 bot (Apr 20 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (1e942ed4c01ecc718c43062aeea864700799f7d8)

github mathlib4 bot (Apr 21 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f63e2da2c97562430540536190768adf9a80963e)

github mathlib4 bot (Apr 22 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (cac9814f8ab9617731132f06a19d5bac602da1f0)

github mathlib4 bot (Apr 23 2025 at 13:01):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b7c854659a47912283e30f077eaffae66f581161)

github mathlib4 bot (Apr 24 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ecc420518f8f2d69925a6c22bad0bfecacfb5d09)

github mathlib4 bot (Apr 25 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (Apr 25 2025 at 10:11):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (286cc68121f180f65ad8e0bf5477ee3562448215)

Kim Morrison (Apr 25 2025 at 10:11):

I have commented out Batteries.RBNode.Path.zoom_del, which is broken on nightly-2025-04-25. I have not investigated: it is not needed downstream. @Mario Carneiro, could you have a look at your convenience?

github mathlib4 bot (Apr 26 2025 at 09:48):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Sebastian Ullrich (Apr 26 2025 at 10:09):

(only deprecations)

Kim Morrison (Apr 26 2025 at 12:53):

Fixed by merging lean-pr-testing-8000

github mathlib4 bot (Apr 26 2025 at 12:58):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (691012f8af16d798b52f24ff54afe386db372ebf)

github mathlib4 bot (Apr 27 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f39898c3b2ccb880c809fe71d5f17e0580083055)

Mario Carneiro (Apr 27 2025 at 20:41):

Kim Morrison said:

I have commented out Batteries.RBNode.Path.zoom_del, which is broken on nightly-2025-04-25. I have not investigated: it is not needed downstream. Mario Carneiro, could you have a look at your convenience?

fixed

github mathlib4 bot (Apr 27 2025 at 20:42):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f39898c3b2ccb880c809fe71d5f17e0580083055)

github mathlib4 bot (Apr 28 2025 at 10:35):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (10c9af04f478fdab0a9986666bd409f667c66877)

github mathlib4 bot (Apr 29 2025 at 09:20):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Markus Himmel (Apr 29 2025 at 09:24):

Sorry, after I saw that the testing branch for lean#8144 was merged into mathlib, I manually merged the corresponding testing branch into batteries (lean#8144 doesn't cause the Batteries build to fail but it needs adjustments to a lemma statement). Then I noticed that Batteries nightly-testing isn't on nightly-2025-04-29 even though mathlib is, so I manually bumped the toolchain (but in the commit message I accidentally wrote 2025-04-28 instead of 2025-04-29 :woman_facepalming:). I hope I didn't confuse any bots or humans.

github mathlib4 bot (Apr 29 2025 at 09:25):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e44568d1ebb500723a2f02076b4afd29a17925e5)

github mathlib4 bot (Apr 30 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ad85961fb2443f811b7386a5b3f5f12c50101258)

github mathlib4 bot (May 01 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (67a2a93da9045a7d16d77d61d2a8552f3b864b53)

github mathlib4 bot (May 02 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (28bf3fb94484af678a4c5d947526ccf1a26479b2)

github mathlib4 bot (May 03 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (bb8010e8869d6980bf352026b3322fc58fe2d7f8)

github mathlib4 bot (May 04 2025 at 09:48):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 05 2025 at 09:50):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (May 05 2025 at 11:34):

Just needed lean-pr-testing-8216 merged.

github mathlib4 bot (May 05 2025 at 11:36):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (dbc813af49dcc0bbc1d676f5ee4c14bf0f888327)

github mathlib4 bot (May 06 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a4a8ea8dc1dcfd1e57e714d2d45ac4616f5fed72)

github mathlib4 bot (May 07 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (fe9cba08e2051a3fdd65c46f6caa5aa3076f5b52)

github mathlib4 bot (May 08 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (4f457b5eef36a42b4426022d9b0b956c397ccf5e)

github mathlib4 bot (May 09 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e44eecdb461bc5a976dc1a2306605d82e022ef1a)

github mathlib4 bot (May 10 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (68bd53833775be628e3240c8ad483592b578fa1e)

github mathlib4 bot (May 11 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (128c629f08911c7e9354572c01561867df084a63)

github mathlib4 bot (May 12 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3007e0de358b943a0d4b3415b80cfb74e8980805)

github mathlib4 bot (May 13 2025 at 13:02):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a78b91642d68ee2b02f0239fe2f068e920f7c6c0)

github mathlib4 bot (May 14 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 14 2025 at 10:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 14 2025 at 10:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3380f851dba8bd16934302f22d1186ab7a9f8a94)

github mathlib4 bot (May 15 2025 at 09:40):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 15 2025 at 09:43):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (0f5071e957a60b3876a71902cd018f7b6625ea53)

github mathlib4 bot (May 16 2025 at 09:30):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 16 2025 at 11:05):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9fb04c93eee9fb9e8c34030c1891000f827b3437)

github mathlib4 bot (May 17 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 17 2025 at 10:35):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f54613ab874c98b28575147d79c676b89981df6c)

github mathlib4 bot (May 19 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (6651d5df12a921d15e6b0fdab8f51effd0ccec60)

github mathlib4 bot (May 20 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 20 2025 at 11:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 21 2025 at 00:01):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 21 2025 at 00:24):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b2ac281f8ec5cffa65ee84b2e4f9aacb28f371b4)

github mathlib4 bot (May 21 2025 at 09:50):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 21 2025 at 10:21):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 21 2025 at 22:55):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ca3cd508e6cfc49ccbd166877214238a1f50a3bb)

github mathlib4 bot (May 22 2025 at 13:02):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ecb656bc81b9b6cd8771c42dcd0f616dae4c9329)

github mathlib4 bot (May 22 2025 at 14:37):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 22 2025 at 22:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ecb656bc81b9b6cd8771c42dcd0f616dae4c9329)

github mathlib4 bot (May 23 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 23 2025 at 14:24):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 24 2025 at 08:55):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

Kim Morrison (May 24 2025 at 08:57):

Oops, needed to merge lean-pr-testing-8037

github mathlib4 bot (May 24 2025 at 08:59):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 24 2025 at 09:02):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (4b6838599e6fbf993014aa6453b42427a376de7d)

github mathlib4 bot (May 24 2025 at 09:34):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed.

github mathlib4 bot (May 24 2025 at 09:37):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (4b6838599e6fbf993014aa6453b42427a376de7d)

github mathlib4 bot (May 24 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (65db7b5d55eef5650e6fd644216783d8be833ef9)

github mathlib4 bot (May 25 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d5643f9165551051a18c95bcfba9c4e5afa62f95)

github mathlib4 bot (May 25 2025 at 13:23):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (d5643f9165551051a18c95bcfba9c4e5afa62f95)

github mathlib4 bot (May 26 2025 at 13:00):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (e312ab8938d5d8783944ff09613f62c9e0306186).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (May 29 2025 at 09:49):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (e5ffc6bd73d63d22e0f2ea9c4b3fa1d9761266b8).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (May 29 2025 at 23:36):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (33ce662d447121e0a98b1e806b966d3742e0c5b5)

github mathlib4 bot (May 30 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (47c0bf66d944847bc51f8f6403e42c03a84f5ba4)

github mathlib4 bot (May 31 2025 at 09:49):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (e5ffc6bd73d63d22e0f2ea9c4b3fa1d9761266b8).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 01 2025 at 02:33):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (22c2cc487453f7f28cebe459213a1a877f629361)

github mathlib4 bot (Jun 01 2025 at 09:49):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (a708530be928e33e576ba76ddc3b278024147919)

github mathlib4 bot (Jun 02 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (8aeda3c8ace5d7c4d1d8255598816b0c409468ef)

github mathlib4 bot (Jun 03 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (65077b31b6dfa634c706e67c8ab2145700ef49a8)

github mathlib4 bot (Jun 04 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (47fbc18e770a55e452a2a8ad28ab751c0c934da4)

github mathlib4 bot (Jun 05 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (f9fbd900b778bec00292986fbd6da7b5778f6d96)

github mathlib4 bot (Jun 06 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (0e42f6ac3e699fd485d181c9c29852e97de96414)

github mathlib4 bot (Jun 07 2025 at 09:49):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (4765a4ee7ab89f407e4bc1d2aa1dbae83bd95e16).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 08 2025 at 09:49):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (4765a4ee7ab89f407e4bc1d2aa1dbae83bd95e16).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 09 2025 at 00:57):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (a6848548537d21596baff3f9453695b7d1f766f6).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jun 09 2025 at 09:38):

This just needed lean-pr-testing-8419 merged.

github mathlib4 bot (Jun 09 2025 at 09:39):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (a6848548537d21596baff3f9453695b7d1f766f6).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 09 2025 at 09:54):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (b1e0be31d21aff484442bb3fb87c0c937cc3a277).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 09 2025 at 09:56):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (a385a57f2981798842f649548af94335a5e3b041)

github mathlib4 bot (Jun 09 2025 at 13:02):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (89fa4695a65d9d4b532822b00cd7b562627a6463)

github mathlib4 bot (Jun 10 2025 at 09:49):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (ef9acd3acba42efed1162b7e9112e668c09916aa).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 10 2025 at 15:49):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (89fa4695a65d9d4b532822b00cd7b562627a6463)

github mathlib4 bot (Jun 11 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (a4da59e30a389969b4131fe81bff7a46d348075f)

github mathlib4 bot (Jun 12 2025 at 13:02):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 12 2025 at 16:03):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 12 2025 at 16:09):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 13 2025 at 09:49):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 13 2025 at 15:33):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 13 2025 at 15:36):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 13 2025 at 15:40):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (7547d99dd8b292191613ec24e6de075ca926dc35)

github mathlib4 bot (Jun 13 2025 at 15:41):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 13 2025 at 20:36):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (7547d99dd8b292191613ec24e6de075ca926dc35)

github mathlib4 bot (Jun 14 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (83ff3624cad7448ee4a4a09a885d8e63631ab980)

github mathlib4 bot (Jun 15 2025 at 15:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (84e8d08ac22d99eb5a29efbaa3df2b880682ffe2)

github mathlib4 bot (Jun 16 2025 at 13:03):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (944ae512567396bbd9e015178bcb3b90501c64f5)

github mathlib4 bot (Jun 17 2025 at 12:02):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (5e6a77528fb6cace1f0adf2563e4e1bc1da541ae).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jun 17 2025 at 12:02):

I've merged lean-pr-testing-8820 into nightly-testing.

Kim Morrison (Jun 17 2025 at 12:03):

This should be done by a bot in discover-lean-pr-testing.yml. Are any Batteries maintainers/contributors available to help diagnose why this is not working? I'd like to not have that on my plate.

github mathlib4 bot (Jun 17 2025 at 12:04):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (251e74283f70d284818676aeff9ed83f84932d9a)

github mathlib4 bot (Jun 18 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (435318b2cb64ee6a5e934e816fb9526fa24ae763)

github mathlib4 bot (Jun 19 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (46378255db20beeb35de72262d9638f97989321a)

github mathlib4 bot (Jun 20 2025 at 13:02):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (fc0cfc7da33b6c218bf96a4f3a537b53c1126672)

github mathlib4 bot (Jun 21 2025 at 09:49):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (43d0460740bbb8999c0e07cd4ea878677be92989).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 22 2025 at 03:54):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (43d0460740bbb8999c0e07cd4ea878677be92989).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 22 2025 at 03:55):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (6ed24da5520050f8e73083ae195709765c2b6b74)

github mathlib4 bot (Jun 22 2025 at 09:48):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (43d0460740bbb8999c0e07cd4ea878677be92989).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jun 23 2025 at 02:35):

This is working locally, I'm not sure why the bot hasn't posted a success message.

Bryan Gin-ge Chen (Jun 23 2025 at 04:00):

This bot is probably also stuck per #mathlib4 > CI @ 💬

github mathlib4 bot (Jun 23 2025 at 04:36):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (43d0460740bbb8999c0e07cd4ea878677be92989).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 23 2025 at 13:02):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (43d0460740bbb8999c0e07cd4ea878677be92989).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 24 2025 at 00:01):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (43d0460740bbb8999c0e07cd4ea878677be92989).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 24 2025 at 00:06):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (b71fde901aa47b6da11ed800746e9f0c868b119f)

github mathlib4 bot (Jun 24 2025 at 13:02):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (d12fdadd81cb96980327cc02587fc14dea65a6e0).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 25 2025 at 09:51):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (d9c0430fabd21f269f728a9864b72bc0df7cfd81)

github mathlib4 bot (Jun 26 2025 at 09:50):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (640cf1e46cb879f898f8a22ecca9473a3fa27341)

github mathlib4 bot (Jun 27 2025 at 13:01):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (d12fdadd81cb96980327cc02587fc14dea65a6e0).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jun 28 2025 at 03:06):

This is building for me locally, I'm not sure why the bot hasn't posted.

Sebastian Ullrich (Jun 28 2025 at 06:47):

https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/bot.20not.20running.20CI again?

github mathlib4 bot (Jun 28 2025 at 12:59):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (d12fdadd81cb96980327cc02587fc14dea65a6e0).
You can git fetch; git checkout nightly-testing and push a fix.

Sebastian Ullrich (Jun 28 2025 at 13:08):

test failures from error message changes

github mathlib4 bot (Jun 29 2025 at 06:23):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (893e597eb5d6485928dea11650fa7c94b365863a)

github mathlib4 bot (Jun 29 2025 at 09:49):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (f4949769e9ae7867a69e99735d638eed0df37eaf)

github mathlib4 bot (Jun 30 2025 at 09:50):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (8d2067bf518731a70a255d4a61b5c103922c772e).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 30 2025 at 10:09):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (8d2067bf518731a70a255d4a61b5c103922c772e).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 30 2025 at 10:13):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (8d2067bf518731a70a255d4a61b5c103922c772e).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 30 2025 at 10:23):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (8d2067bf518731a70a255d4a61b5c103922c772e).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jun 30 2025 at 10:24):

I am so frustrated here. It lints locally!?

github mathlib4 bot (Jun 30 2025 at 10:28):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (8d2067bf518731a70a255d4a61b5c103922c772e).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jun 30 2025 at 10:28):

@Kyle Miller, any ideas here?

Kim Morrison (Jun 30 2025 at 10:29):

def findUnusedHaves (_e : Expr) : MetaM (Array MessageData) := do
  -- adaptation note: kmill 2025-06-29. `Expr.letFun?` is deprecated.
  -- This linter needs to be updated for `Expr.letE (nondep := true)`, but it has false
  -- positives, so I am disabling it for now.
  return #[]

is triggering the unusedArguments linter, and I can't make it go away

Kim Morrison (Jun 30 2025 at 10:29):

or rather, I can locally, but CI seems to ignore the @[nolint unusedArguments].

Kim Morrison (Jun 30 2025 at 10:29):

I've also tried putting it in nolints.json, also to no avail

Kim Morrison (Jun 30 2025 at 10:31):

I'm just going to comment out more

Kim Morrison (Jun 30 2025 at 10:31):

hopefully it makes sense later :-(

github mathlib4 bot (Jun 30 2025 at 10:32):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (8d2067bf518731a70a255d4a61b5c103922c772e).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jun 30 2025 at 10:52):

Grah, this definition doesn't even exist. The linter at Batteries is horribly broken?

Sebastian Ullrich (Jun 30 2025 at 10:59):

It must be some kind of caching bug then, no? According to the Lake Build output, nothing was actually rebuilt?

github mathlib4 bot (Jun 30 2025 at 11:07):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (8d2067bf518731a70a255d4a61b5c103922c772e).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 30 2025 at 11:47):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (02a0cebe7bb095cf512eab9ca1239a997942a17a).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jun 30 2025 at 14:20):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (02a0cebe7bb095cf512eab9ca1239a997942a17a).
You can git fetch; git checkout nightly-testing and push a fix.

Kyle Miller (Jun 30 2025 at 14:22):

I'm confused, this commit hash isn't the right one.... Since 02a0ceb, we've missed 3bb9f90fa77d4f26ccc2fadbaa3fd3df2c9975f0 and ff9268e6fe0d33938b884b62f2a1148da0faab2d.

I modified Batteries/Tactic/Lint/Misc.lean, but looking at the action log, it still seems to be finding a cache. How do we clear the cache?

Mario Carneiro (Jun 30 2025 at 14:23):

this is probably #general > v4.21.0-rc3 @ 💬 then

Mario Carneiro (Jun 30 2025 at 14:24):

but wait, since when is batteries cached?

Kyle Miller (Jun 30 2025 at 14:25):

I'm ignorant about CI and am just believing what I'm reading around https://github.com/leanprover-community/batteries/actions/runs/15975490502/job/45056752182#step:3:55

Mario Carneiro (Jun 30 2025 at 14:31):

this is probably a relative of the same issue then. The cache key used by lean-action is
lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}

Sebastian Ullrich (Jun 30 2025 at 19:57):

No, this is lean#9101, coming to an RC near you soon

github mathlib4 bot (Jun 30 2025 at 23:07):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (3adabe76bed51fc81d04ae65bb7c3893333e3d63).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 01 2025 at 02:46):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (94520d8352f759a05132c6d5cfdf723b6ff72dde).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jul 01 2025 at 05:25):

(Still failing until we move the nightly to 2025-07-01.)

github mathlib4 bot (Jul 01 2025 at 12:10):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (00588ec7a0bc4305d050a56d3f68a3612b012b71).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 01 2025 at 12:11):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (7f17eb21da4f021aca7532d81b638bf975792e18).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 01 2025 at 12:12):

:cross_mark: The latest CI for Batteries' branch#nightly-testing has failed (6eebe20c8ed38ff2ae7fb728c6567e35369cc3e2).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 01 2025 at 12:20):

:check: The latest CI for Batteries' branch#nightly-testing has succeeded! (446eb47c3752b68f09b67ff94d01d022a57564dd)

Robin Arnez (Jul 01 2025 at 12:31):

Oh "branch#nightly-testing" is wrong here too!

Robin Arnez (Jul 01 2025 at 12:33):

Here: batteries#1305

github mathlib4 bot (Jul 01 2025 at 12:57):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (446eb47c3752b68f09b67ff94d01d022a57564dd)

github mathlib4 bot (Jul 02 2025 at 09:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (14ac7be905d97a24c53a3247ebf5c5d9c00adc26).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 02 2025 at 10:56):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8a6376cc91aa54b98a4b0d27d5652f696e1d6bbc)

github mathlib4 bot (Jul 03 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (065d41a73d6f8a1589683479295055095f529ccc)

github mathlib4 bot (Jul 04 2025 at 03:28):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (3cabaef23886b82ba46f07018f2786d9496477d6).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 04 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (1e7f722e0df8df1413f36fc4c886ddcffe372a18)

github mathlib4 bot (Jul 05 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f45e5aa3ee6666b45a55cec4051c4deeb0b3f8c4)

github mathlib4 bot (Jul 06 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (5148d1394e73e4c3db14e5b5240eaefb70f8205c)

github mathlib4 bot (Jul 07 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f7cc1bd569fd0947de75a2e5171d622417fb1d11)

github mathlib4 bot (Jul 08 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (5ab89cd880a67cbc11fa190e84913cc3a3d5dad1)

github mathlib4 bot (Jul 09 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (7a3aafff97fdee5144e6a49f8ef0e588bdfaaa7b)

github mathlib4 bot (Jul 10 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (bf10dcece78bfcc201303edfd07b22e450584559)

github mathlib4 bot (Jul 11 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3ba31a4ebcce68cccfbe0e94141a072ae5955277)

github mathlib4 bot (Jul 12 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (793963dd89a3be23bce60edec9ff853917d25621)

github mathlib4 bot (Jul 13 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f4ccc1c46a468a105497e546f558d7b350ea14c0)

github mathlib4 bot (Jul 14 2025 at 09:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d4050a610e9f4d3a9dcf26deb76b395b8cd19bf9)

github mathlib4 bot (Jul 15 2025 at 13:04):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3aa708ebc14b0243562b4a43d9dcfd953e214f57)

github mathlib4 bot (Jul 16 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f3de4fb740b73ddda55ba21b166d3d838c56214e)

github mathlib4 bot (Jul 17 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (2b45a2b9d470a09b138f705b9efdfb9538301bb2)

github mathlib4 bot (Jul 18 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f4fc275968753ac8fdf4980d1d61630d549461b8)

github mathlib4 bot (Jul 19 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (357e60c8a20e7969255eb42df1a33e90ac527486).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 21 2025 at 09:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8d69f1f6f1b3fbdff311db8c7b9a48e12d852aab)

github mathlib4 bot (Jul 22 2025 at 09:52):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (810dbd859421799fb4816bef7e55414ecac6e731).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 23 2025 at 00:24):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (810dbd859421799fb4816bef7e55414ecac6e731).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Jul 23 2025 at 00:31):

I've fixed some of the problems, but there are broken proofs in Batteries/Data/String/Lemmas.lean. @Mario Carneiro or @Bulhwi Cha, would you be able to fix these, please?

github mathlib4 bot (Jul 23 2025 at 00:31):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (810dbd859421799fb4816bef7e55414ecac6e731).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 23 2025 at 00:32):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (810dbd859421799fb4816bef7e55414ecac6e731).
You can git fetch; git checkout nightly-testing and push a fix.

Bulhwi Cha (Jul 23 2025 at 02:40):

I'm sorry, but I've had little time to contribute to Lean projects since last fall.

Mario Carneiro (Jul 23 2025 at 03:06):

will investigate some time tomorrow

Kim Morrison (Jul 23 2025 at 03:18):

In the interest of getting a green nightly-testing, I've commented out the contents of String/Lemmas.lean in Batteries' nightly-testing until then.

Mario Carneiro (Jul 23 2025 at 03:19):

sha?

Kim Morrison (Jul 23 2025 at 03:19):

dddfa035f77152b137a4b99bad9178ebbe6f8aea

github mathlib4 bot (Jul 23 2025 at 03:19):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (dddfa035f77152b137a4b99bad9178ebbe6f8aea)

github mathlib4 bot (Jul 23 2025 at 15:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f6d0f34f23413248c8de755c3879851a20b204c7)

Robin Arnez (Jul 23 2025 at 16:41):

This was due to lean4#9441 (changing the definition of String.prev). I have a fix here: batteries#1340

github mathlib4 bot (Jul 23 2025 at 21:01):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f6d0f34f23413248c8de755c3879851a20b204c7)

Kim Morrison (Jul 24 2025 at 00:36):

Robin Arnez said:

This was due to lean4#9441 (changing the definition of String.prev). I have a fix here: batteries#1340

Thanks @Robin Arnez. I've restored the downstream dependencies in mathlib's nightly-testing now.

github mathlib4 bot (Jul 24 2025 at 03:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f6d0f34f23413248c8de755c3879851a20b204c7)

github mathlib4 bot (Jul 24 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (84bd5d97b2dac527f8e9136dde765c91824e79af)

github mathlib4 bot (Jul 25 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8b05afe65f22db9ca057170f8d07df9c721383b4)

github mathlib4 bot (Jul 26 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e1c6d49e42f1257c0d9667843c17f72970bc6489)

github mathlib4 bot (Jul 27 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9e4212692f2b966f07305bdcf9ec494d5a4011a2)

github mathlib4 bot (Jul 28 2025 at 09:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (21d4291f16acdfc3549c79f77b6bfc54d1cc8c5f)

github mathlib4 bot (Jul 29 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (cb7c5a0b5a1016a457887560f2e3ebd8a96016dd)

github mathlib4 bot (Jul 30 2025 at 09:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (46f90e298d9c545f3771878526e8f4c0b9de6fb6).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Jul 31 2025 at 00:17):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (18a9f42419cdde5550bea1f520b7d6bf4cffe065)

github mathlib4 bot (Jul 31 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ca83dd91390bb0d2dac6c48837e785dd446b11f2)

github mathlib4 bot (Aug 01 2025 at 13:05):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6a49e4c22164b1d18665837cf1e148131c7a6c4d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 02 2025 at 09:32):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6a49e4c22164b1d18665837cf1e148131c7a6c4d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 02 2025 at 10:43):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (276a2fc2da67b44cf8ba00ccc0fc2165c5efcd7b)

github mathlib4 bot (Aug 03 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (310002d1dc5fc141f9b413c50a7ccaeb8dca1fbb)

github mathlib4 bot (Aug 04 2025 at 00:38):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (43c277c79b269b5eeca3cb96b935386dfe4cdefa).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Aug 04 2025 at 02:09):

This is a breakage in RBMap/Lemmas, which I am temporarily commenting out in 630b71ad. Anyone (@Mario Carneiro?) who would like to fix this can please revert that commit first!

github mathlib4 bot (Aug 04 2025 at 02:10):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (310002d1dc5fc141f9b413c50a7ccaeb8dca1fbb)

github mathlib4 bot (Aug 04 2025 at 09:55):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d27f64901e4a89b68be9c451bf45aecccca38f22)

github mathlib4 bot (Aug 05 2025 at 09:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (c82a5abcfeb7c343cc85bc5ca35938f76546e0c2)

Mario Carneiro (Aug 05 2025 at 18:21):

Kim Morrison said:

This is a breakage in RBMap/Lemmas, which I am temporarily commenting out in 630b71ad. Anyone (Mario Carneiro?) who would like to fix this can please revert that commit first!

fixed

github mathlib4 bot (Aug 06 2025 at 09:54):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (88ef2f1a160659134f62f9edbaa10d318c4a6c1c)

github mathlib4 bot (Aug 07 2025 at 09:52):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a8aacd18dc8dc1c27b4bd180ea0c9615e16f7497).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Aug 07 2025 at 11:42):

Some fallout from lean#9759, I'm asking Sebastian for advice.

github mathlib4 bot (Aug 07 2025 at 11:50):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (1e51212a4c8d72c22de0c3b03b8909550b0ec9ff).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 07 2025 at 11:52):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c4277d9bca1c4d366ae1d976175ff6c008e56ac2).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 07 2025 at 12:17):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c4277d9bca1c4d366ae1d976175ff6c008e56ac2).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Aug 07 2025 at 12:23):

lean#9759 has made definitions in where clauses private. This will cause some disruption downstream.

There is a problem in Aesop, which will be resolved tomorrow by lean#9785. (So nightly-testing will remain failing until then; plus I'll be offline over the weekend.)

There is a problem in Batteries, which can either be resolved by batteries#1369 (deprecate List.fillNones, planning to simply remove the tail-recursive version on the next release), or by someone else adopting this part of the problem! For now I've commented out the broken code in 0de3188.

Robin Arnez (Aug 07 2025 at 13:01):

I feel like we shouldn't deprecate something for a reason that isn't better than "it broke"

Mario Carneiro (Aug 07 2025 at 13:02):

Kim Morrison said:

lean#9759 has made definitions in where clauses private. This will cause some disruption downstream.

by default? I hope that one can slap a public on them to fix this

Robin Arnez (Aug 07 2025 at 13:03):

Well, within the module system

Robin Arnez (Aug 07 2025 at 13:03):

I don't think there's a public override yet but I'd hope that will be introduced eventually

Mario Carneiro (Aug 07 2025 at 13:04):

not even; if private is being added by default then there had better be an opt out, and if it applies to non-modules then the opt out should also work on non-modules

Mario Carneiro (Aug 07 2025 at 13:05):

I don't think this can be delayed, it's essential backward compatibility support

Robin Arnez (Aug 07 2025 at 13:06):

It doesn't apply to non-modules, so I don't think there's much of a worry about backward compatibility unless you relied on where clauses in core

Robin Arnez (Aug 07 2025 at 13:07):

And you can do public section and #with_exporting (@[expose]?) to avoid this

Mario Carneiro (Aug 07 2025 at 13:08):

I'm going to fix https://github.com/leanprover-community/batteries/commit/0de31883486bf87c329a7f2872a333d47fc8b3c4 by open private. These two functions used to be in the same file, this mess was created by upstreaming

Mario Carneiro (Aug 07 2025 at 13:09):

or import all or whatever the new spelling is

Robin Arnez (Aug 07 2025 at 13:10):

Okay, although that won't work within the module system (and I don't believe import all works across module boundaries)

Mario Carneiro (Aug 07 2025 at 13:10):

it does, that's the whole point

Robin Arnez (Aug 07 2025 at 13:10):

Wait no I mean name root boundaries? Hmm let me try

Robin Arnez (Aug 07 2025 at 13:11):

Yeah, cannot use `import all` across module path roots

Robin Arnez (Aug 07 2025 at 13:12):

i.e. Init vs Batteries

Mario Carneiro (Aug 07 2025 at 13:12):

well, I have some choice words to say about that

Mario Carneiro (Aug 07 2025 at 13:13):

I guess I'm going to need to make a more aggressive open private now

Robin Arnez (Aug 07 2025 at 13:15):

That won't work though; because the private declarations aren't even in the environment then

Mario Carneiro (Aug 07 2025 at 13:16):

then I'll load the module file

Mario Carneiro (Aug 07 2025 at 13:16):

I don't want to write an automated copy paste but I will if I have to

Mario Carneiro (Aug 07 2025 at 13:19):

Robin Arnez said:

It doesn't apply to non-modules, so I don't think there's much of a worry about backward compatibility unless you relied on where clauses in core

my understanding is that some definitions from batteries (which used where) were upstreamed to core, and now are made private by this change, breaking batteries

Robin Arnez (Aug 07 2025 at 13:20):

You're right but I guess the question is whether batteries should use these in the first place

Mario Carneiro (Aug 07 2025 at 13:20):

I think the definitions need to be downstreamed again if this private business can't be fixed

Mario Carneiro (Aug 07 2025 at 13:21):

making where definitions private will break hundreds of proofs and definitions I have written

Mario Carneiro (Aug 07 2025 at 13:22):

the previous behavior was exactly what I intended when I wrote those definitions

Mario Carneiro (Aug 07 2025 at 13:22):

so I want an opt out of the new behavior

Mario Carneiro (Aug 07 2025 at 13:23):

and lots of definitions from core also need opt outs put on them because they will cause downstream breakage

Robin Arnez (Aug 07 2025 at 13:25):

My understanding is that what should rather be done instead is copy the definition of filterMapTR.go for this case (since where clauses are more or less considered to be implementation details)

Mario Carneiro (Aug 07 2025 at 13:25):

the thing is, for me "implementation detail" does not equal "private"

Mario Carneiro (Aug 07 2025 at 13:25):

private is much more aggressive and is almost unusable in proof contexts

Mario Carneiro (Aug 07 2025 at 13:26):

implementation details should be handled by scoping them and putting Internal in the namespace and the like

Mario Carneiro (Aug 07 2025 at 13:26):

basically all list functions should be public and have public implementations

Robin Arnez (Aug 07 2025 at 13:26):

Hmm @Sebastian Ullrich, what do you think about this?

Mario Carneiro (Aug 07 2025 at 13:28):

this also relates to the point I made a while back that batteries and mathlib will want to use public section and possibly @[expose] public section in their "standard header boilerplate"

Sebastian Ullrich (Aug 07 2025 at 13:29):

Proofs are not affected by this: where declarations in @[expose] definitions remain public, necessarily

Sebastian Ullrich (Aug 07 2025 at 13:30):

I haven't excluded an additional opt-out syntax but no application came up in core - every now-invalid access to a where decl indeed had a better solution

Mario Carneiro (Aug 07 2025 at 13:31):

I'm starting to dread the next lean4lean bump, this is absolutely going to hit cases where lean is thinking no one would want to prove the correctness of this meta function

Mario Carneiro (Aug 07 2025 at 13:31):

I need import all to work here

Robin Arnez (Aug 07 2025 at 13:33):

I guess you could choose not to adopt the module system and use open private as usual?

Mario Carneiro (Aug 07 2025 at 13:33):

it's unclear whether I can do that?

Mario Carneiro (Aug 07 2025 at 13:33):

I will if that is still an option

Sebastian Ullrich (Aug 07 2025 at 13:35):

I'm not aware of any relevant change to non-modules, I try to avoid introducing those as much as possible. Changes in elaboration of modules may of course still be visible to non-modules as in this case, that part can't be avoided

Mario Carneiro (Aug 07 2025 at 13:35):

right. But is Robin correct that in the new module world there is no way to implement open private?

Mario Carneiro (Aug 07 2025 at 13:37):

can I recommend import all!?

Sebastian Ullrich (Aug 07 2025 at 13:37):

Recommend in what sense?

Sebastian Ullrich (Aug 07 2025 at 13:37):

Oh I didn't see the !

Mario Carneiro (Aug 07 2025 at 13:38):

I assume there is no technical reason for the banning of import all on different name roots, this is just a social engineering thing

Sebastian Ullrich (Aug 07 2025 at 13:39):

A stronger import all may be problematic in ways I can't even foresee yet. E.g. we want to make use of this invariant in the code generator to get the growth of public native symbols under control

Mario Carneiro (Aug 07 2025 at 13:39):

another alternative would be to have an option in the lakefile, not sure if that information can get into the right places

Mario Carneiro (Aug 07 2025 at 13:39):

I don't think there can be any technical argument here considering that non-modules already have all the same issues

Mario Carneiro (Aug 07 2025 at 13:40):

sure you want to minimize the usage of this mechanism, that's different from making it impossible

Sebastian Ullrich (Aug 07 2025 at 13:40):

Non-modules will need to fall back to a less ideal compilation story (e.g. the current one), that's for sure

Mario Carneiro (Aug 07 2025 at 13:42):

I think having ways to achieve this with modules is important for the adoption story, since if avoiding modules means you can do things that can't be achieved otherwise, that's what people will do

Kim Morrison (Aug 07 2025 at 23:16):

Could we address the questions in batteries#1369 (propose deprecation of List.fillNones) directly?

Has this ever been used? Is it common in other languages' List APIs?

If the answers are yes to either, that's fine and good, but if there are not positive answers I would like to proceed with this to avoid pointless work ahead of the release.

github mathlib4 bot (Aug 08 2025 at 00:32):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (aaf34472de76dbfd3f5edfa479129c26fc0ace28).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 08 2025 at 03:28):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (f896bbbed218fb18099e9278b308612563f7337b).
You can git fetch; git checkout nightly-testing and push a fix.

Robin Arnez (Aug 08 2025 at 09:01):

I've traced the definition of fillNones back to https://github.com/leanprover-community/mathlib3/commit/d36af184d154f2e99f60fec5cd71bb3e53899d5c and it seems like it wasn't even used at its point of definition

Mario Carneiro (Aug 08 2025 at 09:02):

cc: @Jannis Limperg

github mathlib4 bot (Aug 08 2025 at 09:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (f896bbbed218fb18099e9278b308612563f7337b).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 08 2025 at 11:58):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (6b0204fdbde13b9a480e72b7e50ce946a05cd242)

Jannis Limperg (Aug 08 2025 at 17:59):

Very happy to have fillNones removed; it seems quite special-purpose.

github mathlib4 bot (Aug 10 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f0d2e0b5e9e8e3af81fa95c9795b68d6621c0a0c)

github mathlib4 bot (Aug 11 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (5315e5db4b93cfbb139249422d686785ab21b2a1)

github mathlib4 bot (Aug 12 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (1ec2b68c5684e29b541d649a7145996d88c4b222)

github mathlib4 bot (Aug 13 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (87dec50264a3aeab88eed62afd665678d220357c)

github mathlib4 bot (Aug 14 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b661461e96bbe8dc6e794700474fcdac724c8dc8)

github mathlib4 bot (Aug 16 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (62b147465fbdbb8e05c6c8a19e6695c80e34df79)

github mathlib4 bot (Aug 17 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (29660a8d23b3c3fc132cf86ac616e8879faf5f32)

github mathlib4 bot (Aug 18 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (91eaf643a48cd2df1e4137528b8b2ec4040bced4)

github mathlib4 bot (Aug 19 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 19 2025 at 12:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9e0e045c1075c42b0afc2b5fc7b1d06d565cecbf)

github mathlib4 bot (Aug 20 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 20 2025 at 12:09):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d3c3880b5053315a0283e885b6c3da181c08309c)

github mathlib4 bot (Aug 21 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3a7ee6b5d5159456492580d9cf7926251078159b)

github mathlib4 bot (Aug 22 2025 at 09:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Aug 22 2025 at 22:39):

oops: error: no such release: 'nightly-2025-08-22'

Kim Morrison (Aug 22 2025 at 22:40):

but: https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2025-08-22

Kim Morrison (Aug 22 2025 at 22:42):

The aarch64 binaries are missing. :-(

Kim Morrison (Aug 22 2025 at 22:44):

Weird: https://github.com/leanprover/lean4/actions/workflows/ci.yml?query=event%3Aschedule

Kim Morrison (Aug 22 2025 at 22:46):

The scheduled CI run failed because the tag already existed. I haven't so far found any trace of an early CI run that could have created it and uploaded a subset of the binaries.

github mathlib4 bot (Aug 23 2025 at 09:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 24 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 24 2025 at 09:59):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 24 2025 at 10:38):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (08ba1e7da2d17880598de231fdf2c75486b5ba2a)

github mathlib4 bot (Aug 25 2025 at 13:00):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 25 2025 at 23:33):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (16a3fbe93f5313e6e72b63bcbbfeb3e435c6f6f0)

github mathlib4 bot (Aug 26 2025 at 18:52):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 26 2025 at 19:58):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 27 2025 at 08:42):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (973c5a4396d070bc1030d596d9dc1375ba493aad)

github mathlib4 bot (Aug 27 2025 at 15:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 27 2025 at 22:14):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 27 2025 at 22:15):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Aug 27 2025 at 22:18):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Aug 27 2025 at 22:26):

@Joachim Breitner, I've had to add some additional exceptions to the Batteries docBlame linter following lean#9952, in bc56c14d on the Batteries nightly-testing branch. Could you please sanity check?

github mathlib4 bot (Aug 27 2025 at 22:26):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (bc56c14d53d868d605d232a97e9689ab4fa88369)

Joachim Breitner (Aug 28 2025 at 07:28):

Good catch, looks good.

At some point we should really provide an API in core for “is this an autogenerated and/or internal declaration”. I just don’t know how rich that API needs to be, short of the full powerset of

auto-generated
needs no documentation
please hide from docs
please hide from search results
please hide from auto-completion
please do not use in proof search/premise selection
…

github mathlib4 bot (Aug 29 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

Robin Arnez (Aug 29 2025 at 12:18):

batteries#1392

github mathlib4 bot (Aug 29 2025 at 12:19):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8f2c9cb2a06ebfe86e89a571cb7cbc4a372a446d)

github mathlib4 bot (Aug 29 2025 at 12:20):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

Robin Arnez (Aug 29 2025 at 12:21):

wtf

Robin Arnez (Aug 29 2025 at 12:37):

> The latest CI for Batteries' nightly-testing branch has succeeded!
> looks inside
> ci / Build (push) Failing after 1m

Kevin Buzzard (Aug 29 2025 at 13:38):

The link to nightly-testing branch above is just a generic link to the current head of the branch, so maybe the first of the two posts was reporting success for a different commit rather than the last one?

Robin Arnez (Aug 29 2025 at 13:40):

My guess is that the build success of batteries#1392 was mistaken for a build success on nightly-testing and then it just took the latest commit from nightly-testing as reference

Kevin Buzzard (Aug 29 2025 at 13:43):

yeah looking at the actual commit hashes now it's clear that something weird is going on. The message reporting a failure is apparently about the commit merging https://github.com/leanprover-community/batteries/pull/1283 which as far as I can see passed CI, and the message with the green check seems to refer to a commit which failed CI.

github mathlib4 bot (Aug 29 2025 at 16:44):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8f2c9cb2a06ebfe86e89a571cb7cbc4a372a446d)

Robin Arnez (Aug 29 2025 at 16:45):

okay something is seriously wrong

Robin Arnez (Aug 29 2025 at 16:46):

(with the commit hashes?)

Robin Arnez (Aug 29 2025 at 16:46):

github mathlib4 bot schrieb:

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (76408f09466811154e0e42329962de19f95d178b).
You can git fetch; git checkout nightly-testing and push a fix.

that's the latest commit on main, not nightly-testing

Kevin Buzzard (Aug 29 2025 at 17:52):

and the 8f2c9cb commit just above has now been posted twice. Hmm, actually that 76408f commit has been posted like 6 times!

github mathlib4 bot (Aug 30 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8236691920ed13377287d8c24c9fcc4f9b359477)

github mathlib4 bot (Aug 31 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9bcf8b228010593c6ee66f5b6a7465608639c6ef)

github mathlib4 bot (Sep 02 2025 at 13:01):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (6f1381fa30f0860ebc6c1c23eb773b558ce5ca29)

github mathlib4 bot (Sep 03 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (51e7ce2e8b017e48411b493232f39c2b7af97f48)

github mathlib4 bot (Sep 04 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f949f7afc2b4f73b2377b185c80c09eb92b228be)

github mathlib4 bot (Sep 05 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (70864aa2331af00ccd1eb4ca175c5a2f1f9641c1)

github mathlib4 bot (Sep 06 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (62fa88a579b754875b70a0b933b5997a393f3275)

github mathlib4 bot (Sep 07 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a67fc66cd1ebc0855dc064a4be727798771c0f89).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 08 2025 at 00:03):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9d75ace5931199084a56eb41697645158c3f1d72)

github mathlib4 bot (Sep 08 2025 at 13:01):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (148f6e74c93a0bc2a3a9b789fbd4dcb47667f787)

github mathlib4 bot (Sep 09 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (c69e53b6b55b28e5e9ed9a33c35dce1cbf37fff1)

github mathlib4 bot (Sep 10 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (21a46596aa055dcce212e03eae3f9224b75b9087)

github mathlib4 bot (Sep 11 2025 at 15:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (cd9ede0dda555daee5aa82b8b4ec7d663fd88d20).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 11 2025 at 22:27):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (cd9ede0dda555daee5aa82b8b4ec7d663fd88d20).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Sep 11 2025 at 22:27):

@David Thrane Christiansen, in lean#10307 the API for Lean.addDocString' changed. Could you please look at commit 3a0fd347 on Batteries nightly-testing and tell me what I'm actually meant to be doing here? I just passed a .missing for the new Syntax argument.

github mathlib4 bot (Sep 11 2025 at 22:28):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (183d9b7636ead80fcdc23056aa8453c07617fe43)

Robin Arnez (Sep 11 2025 at 22:59):

Kim Morrison schrieb:

David Thrane Christiansen, in lean#10307 the API for Lean.addDocString' changed. Could you please look at commit 3a0fd347 on Batteries nightly-testing and tell me what I'm actually meant to be doing here? I just passed a .missing for the new Syntax argument.

Just from looking at the code, here's how I think it works: The new syntax argument are the binders, which should be a null node of binderIdent <|> bracketedBinder and, if you're using addDeclDocOf, you're able to provide a boolean of whether the doc-string uses Verso syntax. That being said, the easiest thing to do is probably

if let some (doc, isVerso) := declMods.docString? then
  addDocStringOf isVerso declName (mkNullNode #[]) doc

If we want to be really fancy, we could also try to delab the binders from whatever were aliasing when isVerso is true (binders are only used for Verso doc-strings).

Kim Morrison (Sep 12 2025 at 00:14):

Thanks @Robin Arnez. I've pushed this now! (@David Thrane Christiansen, if you want to look that's fine but I think we'll survive if you're busy! :-)

github mathlib4 bot (Sep 12 2025 at 00:15):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (183d9b7636ead80fcdc23056aa8453c07617fe43)

David Thrane Christiansen (Sep 12 2025 at 06:25):

@Robin Arnez put in exactly the right suggestion :-)

The binder syntax is used for interactive features, to enable things like "find references" and "go to definition" inside of doc comments. Delaborated binders won't do any good here, because they don't have source locations, so there's no need to pass them if you don't actually have the original syntax of the constant's declaration.

The idea is that if I have:

/--
Creates the text of a proclamation about the value of {lean}`x`.
-/
def proclaim (x : Nat) : String := s!"it is {x}"

then putting the cursor on the x in the docs should cause the parameter binding to be highlighted. Similarly, "go to definition" on that x should jump to the function parameter binding.

I'm updating docstrings to make all this more clear.

github mathlib4 bot (Sep 12 2025 at 06:47):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (183d9b7636ead80fcdc23056aa8453c07617fe43)

github mathlib4 bot (Sep 12 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (d5aa91e17e5ff478bbc840a09cdd0a858cb80b4c)

github mathlib4 bot (Sep 13 2025 at 12:57):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a9a0cb7672b7134497c9d813e53999c9311f4037).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 14 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a9a0cb7672b7134497c9d813e53999c9311f4037).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 14 2025 at 22:34):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (d117e2c28cba42e974bc22568ac999492a34e812).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 14 2025 at 23:01):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (d117e2c28cba42e974bc22568ac999492a34e812).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 14 2025 at 23:05):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b83beda57cc07e6221075f83b99f14885903d261)

github mathlib4 bot (Sep 15 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (327a6eda1afd5779a9fc05a6f3bc9ee164ca48f0)

github mathlib4 bot (Sep 16 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (6a91cb69bf4d3d8b0bcf1c8e8c20ab1038662ca3)

github mathlib4 bot (Sep 17 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (4dc2d96ee6c969dfcde0b3179d831b6435aaa79f)

github mathlib4 bot (Sep 18 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (3881bc95874e5843b76886ea136f4722f1fa83cf).
You can git fetch; git checkout nightly-testing and push a fix.

Robin Arnez (Sep 18 2025 at 10:12):

We seem to have some problems with grind patterns. For example grind [Char.utf8Size_pos] previously resulted in the pattern Char.utf8Size _ and now results in the pattern 1 <= Char.utf8Size _ (which doesn't really make sense here)

Kim Morrison (Sep 18 2025 at 11:43):

Yes, Leo has just changed all the grind patterns. See #rss > Recent Commits to lean4:master @ 💬

Kim Morrison (Sep 18 2025 at 11:44):

We need to build with

-- Compare old and new
set_option backward.grind.checkInferPatternDiscrepancy true
-- Use old
set_option backward.grind.inferPattern true

to identify files where the behaviour has changed, then in those files set

set_option backward.grind.inferPattern false

and change the grind attribute to plain @[grind], which will now give a list of suggestions.

Kim Morrison (Sep 18 2025 at 11:45):

(Starting this in Batteries now.)

Kim Morrison (Sep 18 2025 at 11:51):

Changing the failing grind call to grind [!Char.utf8Size_pos] fixes it. This means: "use this lemma, picking minimal patterns". Probably it is actually fine to make this (and le_four) global grind patterns for utf8Size.

github mathlib4 bot (Sep 18 2025 at 11:54):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8c385cc768e96af7e42bd31980b0b8651367e02e)

github mathlib4 bot (Sep 19 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (3881bc95874e5843b76886ea136f4722f1fa83cf).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 20 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (3881bc95874e5843b76886ea136f4722f1fa83cf).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 20 2025 at 21:22):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (e91bd23a55766cfbe2a0bad429057e998b4ed370).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 21 2025 at 15:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (e91bd23a55766cfbe2a0bad429057e998b4ed370).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 21 2025 at 23:27):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (15a1cfc8b9e8191e67ebeaf5a6adf8abff3ab742)

github mathlib4 bot (Sep 22 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (c2ad556aae6f2371474db593a28cfa17c13de6d7)

github mathlib4 bot (Sep 23 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (e91bd23a55766cfbe2a0bad429057e998b4ed370).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 23 2025 at 11:16):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (2408c52a04baf68f616d79500dfcedbebea8e4ab)

github mathlib4 bot (Sep 24 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3d15ca1cb67e3d90e1e798eedee6e4e8df312dc0)

github mathlib4 bot (Sep 25 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (903b509acff8e83c0dd7820d164968e0cb941b97).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Sep 25 2025 at 10:40):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (2f914316e28b9568a42b68cba7982b4ae2682206)

github mathlib4 bot (Sep 26 2025 at 13:00):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (55c536c23a8883f56407e795fcf5681ae976ea34)

github mathlib4 bot (Sep 28 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8cfa2a012a3d3634d94511dc522cb5195fd3edaf)

github mathlib4 bot (Sep 29 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e07c1017880f46430eb114f0ca76844ac3078210)

github mathlib4 bot (Sep 30 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (11adfc4180b26c4e76776da82442b91ac00b0a07)

github mathlib4 bot (Oct 01 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8a9e7f9ce067fd2bd88a984884a236eb953bcab0)

github mathlib4 bot (Oct 02 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6f7d05f4955eb5af9799d828b697251bb2c9c0b8).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 02 2025 at 10:32):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3fe91d86245451f75cb7142b7cc0bdef71e89e2a)

github mathlib4 bot (Oct 03 2025 at 18:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6f7d05f4955eb5af9799d828b697251bb2c9c0b8).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 05 2025 at 14:33):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (4583377d39b5120d713e65de4f632ea3a545fdeb)

github mathlib4 bot (Oct 05 2025 at 15:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a28b25fbcb690b5fcc2403173a8b5ece6a076a3f)

github mathlib4 bot (Oct 06 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (933ffe84692c2e138daf121101ec6db2c281d495)

github mathlib4 bot (Oct 07 2025 at 13:01):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (915b7a51536f05133e407c5605029aa9e088d5c0)

github mathlib4 bot (Oct 08 2025 at 09:47):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (4702a8b7cb15829f95bb218d1d97eff1760bc10f).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 08 2025 at 14:03):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3e3ab44725d62e3d15b0dbd1b261cf187a26b33b)

github mathlib4 bot (Oct 09 2025 at 12:12):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a05c7c71ffa5dc15546103f81f63e381ae4730c6).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 09 2025 at 13:01):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a05c7c71ffa5dc15546103f81f63e381ae4730c6).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 09 2025 at 16:08):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (410fe5b362962f9a94ec33def57fdc1bbee21150)

github mathlib4 bot (Oct 10 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a05c7c71ffa5dc15546103f81f63e381ae4730c6).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 10 2025 at 10:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ee3b35157a0fd4910e7108df264c93b540986e88)

github mathlib4 bot (Oct 11 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (a05c7c71ffa5dc15546103f81f63e381ae4730c6).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 11 2025 at 12:28):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (05c384470acaf82ca38be66bfb1215c611c747ce)

github mathlib4 bot (Oct 12 2025 at 12:57):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (402aafd25cd468e1a84b43cdd6e67dc8c8694e77)

github mathlib4 bot (Oct 13 2025 at 13:02):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (aee0f1c21824c9f426a0efb3b8927d13c0be0c04)

github mathlib4 bot (Oct 15 2025 at 13:02):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (8da40b72fece29b7d3fe3d768bac4c8910ce9bee).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Oct 15 2025 at 22:43):

I'm mystified by both of these failures. Neither of the "missing" declarations Lean.Elab.Tactic.Ext.extCore and Lean.Elab.Tactic.tactic.customEliminators have been changed, but suddenly the identifiers aren't being found. What change occurred between nightly-2025-10-13 and nightly-2025-10-15?

Kim Morrison (Oct 15 2025 at 22:43):

Ah, lean#10699 explains both?

Kim Morrison (Oct 15 2025 at 22:44):

(@Joachim Breitner, probably changes like this need to be tested against Mathlib in future?)

Kim Morrison (Oct 15 2025 at 22:47):

@Sebastian Ullrich, this prompts a feature request: it's now quite hard when looking at a source file to determine if a declaration is public or private --- this is a nonlocal feature because of public section. Could we add this information to the hover, when hovering over the declaration name in the def itself?

Kim Morrison (Oct 15 2025 at 22:53):

Sanity check on lean#10799 appreciated.

Kim Morrison (Oct 15 2025 at 22:53):

As far as I understand we can't proceed with fixing nightly-testing until this is merged.

Joachim Breitner (Oct 16 2025 at 07:17):

Kim Morrison schrieb:

(Joachim Breitner, probably changes like this need to be tested against Mathlib in future?)

Ah, usually I do, may have slipped this time, sorry

github mathlib4 bot (Oct 16 2025 at 15:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (8da40b72fece29b7d3fe3d768bac4c8910ce9bee).
You can git fetch; git checkout nightly-testing and push a fix.

Sebastian Ullrich (Oct 16 2025 at 21:15):

Kim Morrison said:

Sebastian Ullrich, this prompts a feature request: it's now quite hard when looking at a source file to determine if a declaration is public or private --- this is a nonlocal feature because of public section. Could we add this information to the hover, when hovering over the declaration name in the def itself?

Personally I am using sticky scroll to solve this and similar issues. If we include this in the hover, the declaration kind, e.g. def, should likely also be included for consistency with e.g. #print?

github mathlib4 bot (Oct 16 2025 at 21:34):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (53aaff5d4ddb1aab179ccee49da9225a46a657f5)

github mathlib4 bot (Oct 17 2025 at 09:22):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (92ba52011c77558c50d7e60f2e7e6a087dd5bdd5)

github mathlib4 bot (Oct 18 2025 at 15:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9fa79119de67a1dd60f07932d8a53eccf4caddeb)

github mathlib4 bot (Oct 19 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (8da40b72fece29b7d3fe3d768bac4c8910ce9bee).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 20 2025 at 04:09):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (fdf3a1bb2b644e8e3b1a3a52ddd09d3d2a074d87)

github mathlib4 bot (Oct 20 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e9b1e6a1c70b8e52ff5ed46786e79e05c58bc618)

github mathlib4 bot (Oct 21 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (95fd856490564c67c291a0a7d766c1b1117905d8)

github mathlib4 bot (Oct 22 2025 at 02:41):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

Sebastian Ullrich (Oct 22 2025 at 08:18):

(needs to wait for next nightly to catch up with rc2)

github mathlib4 bot (Oct 22 2025 at 13:03):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 23 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 23 2025 at 10:54):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Oct 23 2025 at 10:58):

@Henrik Böving, this is in part broken by lean#10625. Is there some salvageable replacement for

instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EST _ _)
instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (EIO _)
instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)

instance : LawfulMonad (EST ε σ) := inferInstanceAs <| LawfulMonad (EStateM _ _)

Kim Morrison (Oct 23 2025 at 10:58):

If you're not interested in this aspect of the problem I'm happy to find someone else / delete stuff. :-)

Kim Morrison (Oct 23 2025 at 10:59):

@Markus Himmel, the other parts of the failure here are due to changes in String. I'm not finding an adaptation branch, however, is there something around? (I'm about to go to bed, so feel free to push anything / leave it to me to look at further tomorrow).

Henrik Böving (Oct 23 2025 at 11:03):

I would be somewhat troubled if people were using these to actually do proofs so I would say deleting them for now is fine. They are in principle very much fixable though yes.

Markus Himmel (Oct 23 2025 at 11:06):

Kim Morrison said:

Markus Himmel, the other parts of the failure here are due to changes in String. I'm not finding an adaptation branch, however, is there something around? (I'm about to go to bed, so feel free to push anything / leave it to me to look at further tomorrow).

This was due to my splitting Init.Data.String.Basic, I have added these lines in addition to the existing import all Init.Data.String.Basic:

import all Init.Data.String.Substring  -- for unfolding `Substring` functions
import all Init.Data.String.Iterator  -- for unfolding `Iterator` functions
import all Init.Data.String.Extra  -- for unfolding `Substring.toIterator`
import all Init.Data.String.TakeDrop  -- for unfolding `drop`

github mathlib4 bot (Oct 23 2025 at 11:07):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 23 2025 at 23:36):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Oct 24 2025 at 00:04):

Henrik Böving said:

I would be somewhat troubled if people were using these to actually do proofs so I would say deleting them for now is fine. They are in principle very much fixable though yes.

Okay, handed-off in https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/.60LawfulMonad.60.20instances.20for.20the.20core.20monad.20stack.2C.20broken/near/546784265.

github mathlib4 bot (Oct 24 2025 at 00:05):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Oct 24 2025 at 00:18):

We have an interesting problem in BatteriesTest/lint_empty.lean.

(@David Thrane Christiansen, you might be interested as you added this test ~2 years ago!)

This test checks that Batteries linters run on declarations in an empty environment (e.g. via IO.processCommands).

The test now errors with an `Unknown constant lcAny```. This starts on nightly-2025-10-23 (i.e. it's fine on nightly-2025-10-22), but I don't see anything in the log that is obviously related: https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2025-10-23

Anyone have ideas?

Sebastian Ullrich (Oct 24 2025 at 07:01):

I assume this is BaseIO as well but I don't think it is reasonable to attempt compilation on an empty environment and I'm not sure yet how that could have worked before (haven't looked at the code yet)

David Thrane Christiansen (Oct 24 2025 at 07:07):

I'm having a hard time remember the context in which elaboration (not compilation) in an empty env was needed in a downstream dependency of Batteries, but I think it was for doing the equivalent of prelude in a Verso code block. I think this is not something that's done anywhere anymore and it can be deleted (and if a user wants to do that for pedagogical reasons, we point them at subverso instead)

Henrik Böving (Oct 24 2025 at 07:08):

The compiler definitely expects to have the first three declarations of Init.Prelude available to itself. Even if you are not using core types these can occur out of thin air when compiling code

Sebastian Ullrich (Oct 24 2025 at 07:10):

Let's delete it then

github mathlib4 bot (Oct 24 2025 at 09:03):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 24 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

Sebastian Ullrich (Oct 24 2025 at 09:55):

@Eric Wieser https://github.com/leanprover-community/batteries/commit/979dcd044802cb9f198e99e8a0d55866adf9f8b4 appears to have introduced new failures?

Sebastian Ullrich (Oct 24 2025 at 10:04):

Reverted for now. @Markus Himmel I also fixed moved string import alls but there is one defeq failure left where I don't immediately see the problem/change

github mathlib4 bot (Oct 24 2025 at 10:05):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 24 2025 at 10:09):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 24 2025 at 10:10):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c44068fa1b40041e6df42bd67639b690eb2764ca).
You can git fetch; git checkout nightly-testing and push a fix.

Sebastian Ullrich (Oct 24 2025 at 10:11):

Ah, I didn't mean to push the import all Init.Prelude :)

github mathlib4 bot (Oct 24 2025 at 10:12):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a61819ab39d5bb5d889bd4795904f72cef7ebc42)

github mathlib4 bot (Oct 25 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (5219ff865e343e4176df85c1db45d0cdd3ddda91)

github mathlib4 bot (Oct 26 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (143682977bb0ededbb72cbefd8e5890e9fffd73c)

github mathlib4 bot (Oct 27 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (99b62029ea9c0b43c39281f6687ce3bfc6cd6bc3)

github mathlib4 bot (Oct 29 2025 at 02:15):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (e1303724b4b421693e72e817657f766ed6b9c0c9).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 29 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (e1303724b4b421693e72e817657f766ed6b9c0c9).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 29 2025 at 10:46):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e94d5e4b0500e3013afb79c44e42a36282c760c3)

github mathlib4 bot (Oct 30 2025 at 09:50):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c029ceb9956ef9d567fc034e5403ec829f8d0d87).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Oct 30 2025 at 10:58):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (2ff6418e915c384626f0566a3c5ad829c809391f)

github mathlib4 bot (Oct 31 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3a43cfc033d418625f1c54a6f2a5edefca462ab3)

github mathlib4 bot (Nov 01 2025 at 12:58):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (5da171049c81931a2110303c9d547f5ab2955b06).
You can git fetch; git checkout nightly-testing and push a fix.

Markus Himmel (Nov 01 2025 at 12:59):

It would be great if the bot(s) could merge the adaptations PR first and then run CI, not the other way around :D

github mathlib4 bot (Nov 01 2025 at 13:01):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a89d951ac85d717a0c2a78bc5a342728c97771bd)

Sebastian Ullrich (Nov 01 2025 at 13:02):

Markus Himmel said:

It would be great if the bot(s) could merge the adaptations PR first and then run CI, not the other way around :D

Yes, prior discussion @ #nightly-testing > bot not running CI

github mathlib4 bot (Nov 01 2025 at 13:03):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a89d951ac85d717a0c2a78bc5a342728c97771bd)

github mathlib4 bot (Nov 02 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (5da171049c81931a2110303c9d547f5ab2955b06).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 02 2025 at 10:11):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a747dd9d4cb480b3f063895e1c1a77bf49ec315d)

github mathlib4 bot (Nov 03 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (310499bf83bc734e3981dbddcf15799e4f6c06a0)

github mathlib4 bot (Nov 04 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (f5e039741e8092aeb366e10005c3fe9a68ad07bb)

github mathlib4 bot (Nov 05 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (44b6e6cb4dbeb35455721da14bf164d3f9883e4c)

github mathlib4 bot (Nov 06 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b1c105bb5490556ce9789fab7224e710eb67631b)

github mathlib4 bot (Nov 07 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (50d1f6a911cd591db1762e77f9771a4a679e96bb)

github mathlib4 bot (Nov 08 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (14522f6ff4107d41a0ebff11cc5d0831224ffe59)

github mathlib4 bot (Nov 10 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a11cdab9a6b9e7144267924b0bbd7d1c84fa264f)

github mathlib4 bot (Nov 11 2025 at 09:50):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (091ff2379c7f0998aba1dc031a578810d44b9f3f).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 11 2025 at 09:57):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (828bc7c72aac4efc1906c784bf86d229f2feb91a)

github mathlib4 bot (Nov 12 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (04c097bfebdb61c3697892ccc2bd757a1341627a)

github mathlib4 bot (Nov 13 2025 at 10:14):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ebdad22481215c741c2f6f7882d3cc2d3d8f46d6)

github mathlib4 bot (Nov 14 2025 at 13:01):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (39260e31b7b3f7f05643da95242463b462dc05f1).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 14 2025 at 14:24):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (0302374521960af49605c5b2a73718c90f1369e2)

github mathlib4 bot (Nov 15 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (c8cd1455de8c406797412a921eae787ec663ae51)

github mathlib4 bot (Nov 16 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8e479e9aa245cea4fd6262904f144b4e67458425)

github mathlib4 bot (Nov 17 2025 at 09:50):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (5c78955e8375f872c085514cb521216bac1bda17).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 18 2025 at 05:30):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Nov 18 2025 at 05:59):

nightly-testing is working, but the bot is not reporting this. :-(

Kim Morrison (Nov 18 2025 at 06:01):

chore: adaptations for nightly-2025-11-17 #1519

github mathlib4 bot (Nov 18 2025 at 06:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (e53b625cdcda396fb008ca99ea1ae49ddc24fdd7)

github mathlib4 bot (Nov 18 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (458f79255ec9b361a15ddd9ee08fd3829fdf643d)

github mathlib4 bot (Nov 19 2025 at 10:59):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c278d4e94fe43bc38da4966795dc0c72538e68ab).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 19 2025 at 11:02):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (06c225a07b296d892a6d329fb09f34e3712ec3ff)

github mathlib4 bot (Nov 20 2025 at 09:50):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (c278d4e94fe43bc38da4966795dc0c72538e68ab).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Nov 20 2025 at 11:02):

90e3bf68c comments out a failing proof about String in Batteries. @Mario Carneiro and/or @Markus Himmel, if either of you would like to restore this and/or tell me it's fine to deprecate on main?

github mathlib4 bot (Nov 20 2025 at 11:03):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (90e3bf68cbacac466317e2d1560a5b0d7d3aa6a0)

Markus Himmel (Nov 20 2025 at 12:16):

Kim Morrison said:

f either of you would like to restore this and/or tell me it's fine to deprecate on main?

Restored.

github mathlib4 bot (Nov 20 2025 at 12:17):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (90e3bf68cbacac466317e2d1560a5b0d7d3aa6a0)

github mathlib4 bot (Nov 21 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (1ed7b098fa61b38ed17db5ed4bb7087e01196e6a)

github mathlib4 bot (Nov 22 2025 at 09:49):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (afe9302d9243cee630b0be95322b38b90342ddbf).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 22 2025 at 12:33):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (30cfb2255996f3e6217a77fd940fde1f3e12ccc2).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Nov 23 2025 at 04:08):

38e6d3429 comments out more failing String lemmas, @Markus Himmel / @Mario Carneiro .

github mathlib4 bot (Nov 23 2025 at 04:10):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (38e6d3429b2953b7e72b514bcbb1beba51582297)

github mathlib4 bot (Nov 23 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (1038f333c6c93649181ab5aeea4bff76b4c0cc32)

github mathlib4 bot (Nov 24 2025 at 09:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (30cfb2255996f3e6217a77fd940fde1f3e12ccc2).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Nov 24 2025 at 10:37):

Merged lean-pr-testing-11276, which didn't happen automatically because of a conflict.

github mathlib4 bot (Nov 24 2025 at 10:39):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (7444211aa83390b018718c0300bdcf518b8cd5db)

github mathlib4 bot (Nov 25 2025 at 09:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (26884086fb66f99b56ed363c5e54bfcc70238599).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 25 2025 at 10:17):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (7ba90e320ee46ae77772b2b747af5511ceb2e577)

github mathlib4 bot (Nov 26 2025 at 13:04):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (26884086fb66f99b56ed363c5e54bfcc70238599).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Nov 27 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (7cb517611b099456c5a93de6da3196d216bf10c6)

github mathlib4 bot (Nov 28 2025 at 18:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (09aa5c2b9a0c7df284fd344b8b1e246d61127492)

github mathlib4 bot (Nov 29 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (a59a7e6c69af305b4a03acce5db2ec2588fb1336)

github mathlib4 bot (Nov 30 2025 at 09:50):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9dc7973629f2338d9d40f55a1c17f9ce59709941)

github mathlib4 bot (Dec 01 2025 at 13:06):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (2315ef514ef6de8a8a79fca3c1fdf146dca0ab77)

github mathlib4 bot (Dec 02 2025 at 09:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (943400f97c5eee1cacc151ed91c0545d83dc95c8)

github mathlib4 bot (Dec 03 2025 at 13:06):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (e1c1e06b9cbfc873b309695c9e9584de88ec22ac).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 04 2025 at 03:55):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (7d12840c9e4942d1a30345051517bc8b4f00dd38)

github mathlib4 bot (Dec 04 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (44fcf738c060fdda7cc1bbf57ed5f4ff3f2b48de)

github mathlib4 bot (Dec 05 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (0d1f1ab7e3e7d409bd496bc3449e658ac8c3119f)

github mathlib4 bot (Dec 06 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (194746cfa746ce64a09228e1ca0ea58aa2af90eb)

github mathlib4 bot (Dec 07 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (1333433fa4c36be7133c305c881e6e1f3c5f9ba3)

github mathlib4 bot (Dec 08 2025 at 09:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (f2aca6fc4a47c5b67fad08d3eda5e949d5b73ac0).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 08 2025 at 10:59):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (66153a0cad828f26f7e0e65db1057cd5a104b536)

github mathlib4 bot (Dec 09 2025 at 09:51):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (0d8c5b998cd549694a68e184bba24cc300ab2276)

github mathlib4 bot (Dec 09 2025 at 11:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (44cdfa76dc744fb0cd356457dcdcc5366ec647ac).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 09 2025 at 22:39):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (0d8c5b998cd549694a68e184bba24cc300ab2276)

github mathlib4 bot (Dec 10 2025 at 09:56):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (faaece101b4c82137c08f13af38e03ca58267d20)

github mathlib4 bot (Dec 11 2025 at 09:52):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (44cdfa76dc744fb0cd356457dcdcc5366ec647ac).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 11 2025 at 10:23):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (5fc8fc81c41a634786fb480c6e9bee9dbe93015d)

github mathlib4 bot (Dec 12 2025 at 09:51):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (44cdfa76dc744fb0cd356457dcdcc5366ec647ac).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 12 2025 at 11:39):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (ba7f3a667536b8e73bdce55acc0087b4f544cbea)

github mathlib4 bot (Dec 13 2025 at 09:37):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (24241822ef9d3e7f6a3bcc53ad136e12663db8f3).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 13 2025 at 09:44):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (3da88432f37fc72ab1cb207be080a2352a89ec45)

github mathlib4 bot (Dec 14 2025 at 08:55):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (cf021cb1888b678334b873e0d4544261898921f4)

github mathlib4 bot (Dec 15 2025 at 09:56):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (8c795d864da584c9fbd69e15a97aebbbfc8d5b7f)

github mathlib4 bot (Dec 16 2025 at 09:52):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (78129e1913fe4988ac238156ec5f223ec02d286c).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 16 2025 at 21:29):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (fc39f125cafc8b03a514ea2afb401940f56d7715)

github mathlib4 bot (Dec 17 2025 at 09:53):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (318cf31925d3887992d152d52d05de6d5fdf94b4)

github mathlib4 bot (Dec 18 2025 at 09:53):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6cae843edf5b3abc871c557614eaffdcb4492d89).
You can git fetch; git checkout nightly-testing and push a fix.

Kim Morrison (Dec 18 2025 at 10:02):

I commented out in 50902ea41 on nightly-testing some failing material on AsciiCasing. If someone is available to restore this, that would be great (i.e. revert that commit and apply a fix).

github mathlib4 bot (Dec 18 2025 at 10:03):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6cae843edf5b3abc871c557614eaffdcb4492d89).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 18 2025 at 10:11):

:cross_mark: The latest CI for Batteries' nightly-testing branch has failed (6cae843edf5b3abc871c557614eaffdcb4492d89).
You can git fetch; git checkout nightly-testing and push a fix.

github mathlib4 bot (Dec 18 2025 at 10:13):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (50902ea41ffbee1c69400d2e0e915719111ba53b)

github mathlib4 bot (Dec 19 2025 at 09:52):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (b113a64a5a54c86a799f7aa95c27342186ee49eb)

github mathlib4 bot (Dec 20 2025 at 09:49):

:check: The latest CI for Batteries' nightly-testing branch has succeeded! (9f7f933c2bb39ba927522e3ed43e0dc991d04e38)

Last updated: Dec 20 2025 at 21:32 UTC