Zulip Chat Archive

Stream: nightly-testing

Topic: Std status updates

github mathlib4 bot (Mar 15 2024 at 09:15):

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

Ruben Van de Velde (Mar 15 2024 at 09:17):

Several cases of error: unknown identifier 'resolveGlobalConstNoOverloadWithInfo' which should now be realizeGlobalConstNoOverloadWithInfo

github mathlib4 bot (Mar 15 2024 at 09:35):

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

Kim Morrison (Mar 15 2024 at 09:38):

Investigating this one now. (Or rather Sebastian is. :-)

github mathlib4 bot (Mar 15 2024 at 09:48):

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

Kim Morrison (Mar 15 2024 at 09:51):

Lots of unnecessary haves, because the termination checker keeps getting better :tada:

That was optimistic. Actually, it is lots of incorrect unusedHaveSuffices linter reports, on auto-generated simp auxiliaries.

Kim Morrison (Mar 15 2024 at 09:58):

Std.Tactic.Lint.isAutoDecl needs updating after lean4#3675

github mathlib4 bot (Mar 18 2024 at 07:47):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 18 2024 at 09:17):

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

github mathlib4 bot (Mar 18 2024 at 11:18):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

Kim Morrison (Mar 18 2024 at 11:51):

std4#700 is the bump PR for nightly-2024-03-18 for Std.

github mathlib4 bot (Mar 19 2024 at 09:16):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 19 2024 at 23:33):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 20 2024 at 00:42):

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

Kim Morrison (Mar 20 2024 at 00:47):

Caused by the merge of std4#489. First failure is easy to resolve by reordering lemmas.

Kim Morrison (Mar 20 2024 at 00:50):

Other failures from the new termination_by syntax, and needing some import adjustments.

github mathlib4 bot (Mar 20 2024 at 00:53):

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

Kim Morrison (Mar 20 2024 at 00:54):

std#703 is the bump PR for nightly-2024-03-19

github mathlib4 bot (Mar 20 2024 at 01:10):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 20 2024 at 01:13):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 21 2024 at 04:52):

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

github mathlib4 bot (Mar 21 2024 at 07:50):

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

github mathlib4 bot (Mar 21 2024 at 09:16):

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

github mathlib4 bot (Mar 21 2024 at 22:43):

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

github mathlib4 bot (Mar 21 2024 at 22:43):

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

github mathlib4 bot (Mar 22 2024 at 00:23):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 22 2024 at 00:36):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 22 2024 at 01:09):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 22 2024 at 01:56):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

Kim Morrison (Mar 22 2024 at 02:01):

Hmmm, bad bot, you seem to be repeating yourself.

Kim Morrison (Mar 22 2024 at 02:03):

https://github.com/leanprover/std4/pull/709

github mathlib4 bot (Mar 22 2024 at 02:10):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

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

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

Kim Morrison (Mar 22 2024 at 09:09):

Just requires merging lean-pr-testing-3589 for lean#3589

github mathlib4 bot (Mar 22 2024 at 09:10):

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

github mathlib4 bot (Mar 22 2024 at 09:17):

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

github mathlib4 bot (Mar 22 2024 at 09:20):

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

github mathlib4 bot (Mar 22 2024 at 10:43):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 23 2024 at 09:16):

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

github mathlib4 bot (Mar 23 2024 at 22:16):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

Kim Morrison (Mar 27 2024 at 23:47):

I will be away over the weekend and unable to fix this, but we should expect a failure here in about 8 hours from some upstreaming in lean4#3785. Fixing it should just involve deleting the /-! ## Tail recursive implementations for definitions from core -/ section in Std.Data.List.Basic.

If someone is able to do that, push to nightly-testing, and then lake update std on Mathlib's nightly-testing, that would be great.

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

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

github mathlib4 bot (Mar 28 2024 at 23:26):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Mar 29 2024 at 09:15):

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

github mathlib4 bot (Mar 29 2024 at 22:20):

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

github mathlib4 bot (Mar 29 2024 at 22:21):

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

github mathlib4 bot (Mar 30 2024 at 09:14):

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

github mathlib4 bot (Apr 01 2024 at 09:18):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 02 2024 at 09:17):

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

github mathlib4 bot (Apr 02 2024 at 09:27):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 05 2024 at 09:16):

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

github mathlib4 bot (Apr 05 2024 at 17:12):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 13 2024 at 09:31):

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

github mathlib4 bot (Apr 13 2024 at 11:43):

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

github mathlib4 bot (Apr 13 2024 at 11:43):

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

github mathlib4 bot (Apr 14 2024 at 01:14):

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

github mathlib4 bot (Apr 14 2024 at 11:23):

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

github mathlib4 bot (Apr 14 2024 at 18:22):

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

github mathlib4 bot (Apr 14 2024 at 18:32):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 15 2024 at 06:16):

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

Kim Morrison (Apr 15 2024 at 06:20):

Just needed a renamed after std4#734 landed.

github mathlib4 bot (Apr 15 2024 at 06:23):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

Kyle Miller (Apr 15 2024 at 06:23):

Ah, you beat me to it (std4#742)

Kim Morrison (Apr 15 2024 at 06:27):

The speed advantage of pushing direct to nightly-testing. :-)

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

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 17 2024 at 04:17):

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

github mathlib4 bot (Apr 17 2024 at 04:19):

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

github mathlib4 bot (Apr 17 2024 at 04:21):

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

github mathlib4 bot (Apr 17 2024 at 04:26):

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

github mathlib4 bot (Apr 17 2024 at 07:01):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 17 2024 at 14:12):

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

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

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 18 2024 at 01:46):

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

github mathlib4 bot (Apr 18 2024 at 02:15):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 19 2024 at 09:06):

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

github mathlib4 bot (Apr 20 2024 at 07:23):

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

github mathlib4 bot (Apr 20 2024 at 07:39):

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

github mathlib4 bot (Apr 20 2024 at 07:40):

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

github mathlib4 bot (Apr 20 2024 at 07:41):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

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

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

Kim Morrison (Apr 21 2024 at 23:53):

This was lean#3960.

github mathlib4 bot (Apr 21 2024 at 23:53):

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

Kim Morrison (Apr 21 2024 at 23:54):

And one more rfl.

github mathlib4 bot (Apr 21 2024 at 23:56):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 22 2024 at 10:42):

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

github mathlib4 bot (Apr 22 2024 at 10:53):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

Kim Morrison (Apr 23 2024 at 01:00):

I've just created std4#761, bringing Std's bump/v4.8.0 branch up from nightly-2024-04-01 to nightly-2024-04-22. It doesn't look too bad.

github mathlib4 bot (Apr 23 2024 at 01:04):

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

github mathlib4 bot (Apr 23 2024 at 01:11):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

github mathlib4 bot (Apr 24 2024 at 03:36):

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

github mathlib4 bot (Apr 24 2024 at 03:38):

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

github mathlib4 bot (Apr 24 2024 at 03:41):

:check: The latest CI for Std's branch#nightly-testing has succeeded!

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

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

github mathlib4 bot (Apr 25 2024 at 16:31):

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

Kim Morrison (Apr 27 2024 at 09:11):

I'm back, and will start looking at Std!

Ruben Van de Velde (Apr 27 2024 at 09:14):

Thanks!

github mathlib4 bot (Apr 27 2024 at 09:17):

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

github mathlib4 bot (Apr 27 2024 at 09:18):

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

Kim Morrison (Apr 27 2024 at 09:27):

test/congr.lean is failing. So far I don't see what is wrong. It looks like it has been failing for a while, however: succeeds on nightly-testing-2024-04-20, but not on 21, 22, 23 (24 didn't exist).

Kim Morrison (Apr 27 2024 at 09:27):

This is a bit worrying: how did the success shown above on April 24 happen?

Kim Morrison (Apr 27 2024 at 09:28):

Oh weird, now it is failing on 20 as well.

Ruben Van de Velde (Apr 27 2024 at 09:33):

Strange, the message from the 24th seems to have been triggered off https://github.com/leanprover/std4/commit/4a54f26203f47428c389297a2448d6348bb97484, which shouldn't have been the head of nightly-testing

Kim Morrison (Apr 27 2024 at 09:35):

Okay, I don't what is happening here. Now all the nightly-testing-2024-04-XXs succeed in test/congr.lean locally...

Kim Morrison (Apr 27 2024 at 09:35):

It's just nightly-testing where it fails.

Kim Morrison (Apr 27 2024 at 09:35):

So likely lean4#3977 is the culprit.

Kim Morrison (Apr 27 2024 at 09:43):

Ah not that at all.

Kim Morrison (Apr 27 2024 at 09:44):

test/congr.lean has always failed if List.ext was imported ---- but up until now it hasn't been. Now that List.ext is in core, this breaks the test file.

Kim Morrison (Apr 27 2024 at 09:46):

I am just adding:

-- Adaptation note: the next two examples have always failed if List.ext was in scope,
-- but until nightly-2024-04-24 (when List.ext was upstreamed), it wasn't in scope.
-- For now these are commented out,
-- but if anyone would like to replace these tests that would be great!

github mathlib4 bot (Apr 27 2024 at 09:48):

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

github mathlib4 bot (Apr 29 2024 at 08:10):

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

github mathlib4 bot (Apr 29 2024 at 08:12):

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

github mathlib4 bot (Apr 30 2024 at 23:20):

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

github mathlib4 bot (Apr 30 2024 at 23:22):

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

github mathlib4 bot (Apr 30 2024 at 23:47):

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

github mathlib4 bot (May 01 2024 at 03:16):

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

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

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

github mathlib4 bot (May 01 2024 at 10:00):

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

github mathlib4 bot (May 03 2024 at 04:39):

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

github mathlib4 bot (May 03 2024 at 04:44):

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

github mathlib4 bot (May 06 2024 at 09:06):

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

github mathlib4 bot (May 06 2024 at 11:08):

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

github mathlib4 bot (May 06 2024 at 11:11):

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

Last updated: May 02 2025 at 03:31 UTC