moving to a fork

Stream: nightly-testing

[Kim Morrison]

I've got started this morning on moving our nightly-testing infrastructure to a fork. (So that we can give out write access to people involved in keeping it alive!)

So far:

• I've created a fork https://github.com/leanprover-community/mathlib4-nightly-testing, and copied across nightly-testing (which is set as the default branch -- there is no master on this fork, to avoid confusion), all the lean-pr-testing-NNNN branches, and all the batteries-pr-testing-NNNN branches.
• lean#8933 changes the Lean4 side of CI, so that future lean-pr-testing-NNNN branches will be created on this fork.

Ongoing:

• change everything on the mathlib4 and batteries side of things
• see what is broken, fix it
• give write access on this fork
• eventually, remove the migrated branches from the main repository.

Note that I intend that the bump/v4.X.0 branches will continue to live on the main repository: no one needs write access to these except a few maintainers.

[Kim Morrison]

(I'm recording progress on updating repository secrets and bot access in the CI admins private channel.)

[Kim Morrison]

Slight update to the plan --- the reviewed bump/v4.X.0 branches, as well as the unreviewed PR branches bump/nightly-YYYY-MM-DD will also live on the new fork, rather than the main repo.

[Kim Morrison]

Okay, #26286 is my attempt at reconfiguring all the CI infrastructure to work from the new fork.

[Kim Morrison]

I have tested nothing, this is all speculative. Review appreciated, but I'd also like to start trying it out in production asap.

[Kim Morrison]

I have created an team https://github.com/orgs/leanprover-community/teams/nightly-testing, to which we should add trusted people who need write access to the new fork.

[Kim Morrison]

I'm also transitively giving members of lean-fro write access, as they often need to be able to update lean-pr-testing-NNNN branches.

[Kim Morrison]

I am now pausing on this job, awaiting someone to give a +1 for merging the two PRs above, so we can start testing for real.

[Kim Morrison]

Oh, one more: batteries#1287

[Kyle Miller]

Does https://github.com/leanprover-community/mathlib4-nightly-testing have a cache yet? If it does, how do I configure things to use it?

All I've done is create a new remote for this repo and then make my nightly-testing branch track it.

[Kim Morrison]

That should suffice. (But presumably things are still broken.) What are you seeing?

[Kim Morrison]

To avoid confusion, I am about to delete the nightly-testing branch on our main repo, so everything has to work with the nightly-testing fork or fail.

[Kim Morrison]

Yeah, for me it is only looking for the oleans on leanprover-community/mathlib4 and kim-em/mathlib4

[Kim Morrison]

I think there is a hardcoded place in Cache where we tell it how to deal with nightly-testing, and this is now wrong.

[Kyle Miller]

Kim Morrison said:

What are you seeing?

Mathlib repository: leanprover-community/mathlib4
Attempting to download 6876 file(s) from leanprover-community/mathlib4 cache
Downloaded: 0 file(s) [attempted 6876/6876 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means [...]

[Kim Morrison]

Fixing now.

[Kim Morrison]

At least, the download logic. I think the oleans aren't being pushed at all anyway. :-(

[Kim Morrison]

#26334 feat: cache uses the nightly-testing cache when relevant

[Kim Morrison]

This at least causes cache to look for oleans in the right place. Why they are not there remains to be seen. :-)

[Joachim Breitner]

In https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/15853386008/job/44692443836 I fixed nighty-testing. The build step does

Attempting to upload 6876 file(s) to leanprover-community/mathlib4-nightly-testing cache

but the Post-build-step tries

Attempting to download 6876 file(s) from leanprover-community/mathlib4 cache

and then

Attempting to download 6876 file(s) from leanprover-community/mathlib4-nightly-testing cache

but both with (0% success).

---

Hmm, I thought I had something to add, but that wasn’t worth adding.

I wonder if it’s maybe a difference in trace keys. But the existing logs don’t seem to convey which key the cache is looking for.

[Johan Commelin]

We'll need to update https://leanprover-community.github.io/contribute/tags_and_branches.html once this stabilizes.

[Robin Arnez]

Wow that's outdated (Std4?)

[Kyle Miller]

How do we do mathlib benchmarks for Lean 4 PRs now? I (accidentally) created a PR for mathlib4-nightly-testing (https://github.com/leanprover-community/mathlib4-nightly-testing/pull/1) but the speed center appears not to be listening to !bench there.

If I created a similar PR for mathlib4, what do I need to do to be sure that the speed center will compare the effects of just the change in Lean? I worry that it will give me a comparison between some random old version of mathlib and my changes.

[Joachim Breitner]

If in doubt, create PRs in mathlib4 for both commits you want to compare, and run !bench on both, and then select the runs for comparison. A bit tedious, I agree.