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)

Last updated: May 02 2025 at 03:31 UTC