Lean PR testing via nightly-with-mathlib

Stream: nightly-testing

[Thomas Murrills]

Hopefully a topic like this is appropriate for this stream—my intention is that this topic could be used for any issues with the way nightly testing interacts with Lean PR testing. (If this is out of scope, please feel free to move it, though.)

[Thomas Murrills]

The issue that motivated me is: when nightly-testing is already broken, the bot labels lean4 PRs with breaks-mathlib, and includes a message saying that the PR breaks mathlib.

In the case that nightly-testing is already broken, would it be possible for the bot to

1. not label it breaks-mathlib (nor builds-mathlib)
2. use a different message clarifying the situation in the comment, e.g. "nightly-testing is currently broken"
3. re-run automatically when nightly-testing is fixed (maybe this last step already happens?)

(I'm guessing we still want to run CI in the first place, in case the lean4 PR is meant to be a patch that fixes issues in nightly-testing!)

[Kim Morrison]

@Thomas Murrills, if the automation is labelling anything with break-mathlib because of existing problems separate from the Lean PR, that is a bug and needs a report.

[Kim Morrison]

Note Lean PRs are never tested against nightly-testing directly.

[Kim Morrison]

Instead:

• whenever nightly-testing first goes green on a given nightly, we create a Mathlib tag nightly-testing-YYYY-MM-DD
• and update Lean's nightly-with-mathlib branch to point at the Lean nightly for that date
• if the base of a Lean PR is nightly-with-mathlib, then we generate a Mathlib branch lean-pr-testing-XXXX from the corresponding nightly-testing-YYYY-MM-DD
• however if the base is some other commit, we don't attempt to test against Mathlib and instead post a message to the Lean PR saying that you need to rebase on nightly-with-mathlib if you want Mathlib testing.

[Kim Morrison]

The combination of these rules means that any breaks-mathlib tag should be a real breakage caused by that PR.

[Thomas Murrills]

Ah, ok. This occurred on lean4#3698, which should be a very small change; some of the errors were even style linting errors. Could you please verify that this is erroneously labeled?

[Thomas Murrills]

(And, if so, where should I file the bug?)

[Kim Morrison]

Yup, something is definely wrong there. The Lean CI status messages clearly identify that this PR is based off nightly-2024-03-16, yet over on Mathlib nightly-testing-2024-03-16 doesn't exist.

[Kim Morrison]

Thus, according to the rules I said above, I thought this means that Mathlib CI simply shouldn't run.

[Kim Morrison]

Just making sure: you didn't manually create a lean-pr-testing-3698 branch at Mathlib?

The git log shows that leanprover-community-mathlib4-bot created the lean-pr-testing-3698 branch.

[Thomas Murrills]

(I see it’s struck through, but just to confirm: nope, it was automatic :) ) Oops, the git log message hadn’t come through. (Or my scroll state was locked? Zulip went a bit funky.)

[Kim Morrison]

It looks like https://github.com/leanprover/lean4/actions/runs/8310595327/job/22743278264 is the relevant CI job that did this.

[Kim Morrison]

The merge base of this PR coincides with the nightly release
... but Mathlib does not yet have a 'nightly-testing-2024-03-16' tag.
... and Std has a 'nightly-testing-2024-03-16' tag.

seems correct.

[Kim Morrison]

Ahha!

[Kim Morrison]

Logic error here:

            if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
              MESSAGE=""
            else
              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
            fi

            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"

            if [[ -n "$STD_REMOTE_TAGS" ]]; then
              echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
              MESSAGE=""
            else
              echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
              MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
            fi

[Kim Morrison]

The presence of the Std nightly-testing-2024-03-16 tag overrides the failure message about Mathlib not having a nightly-test-2024-03-16 tag.

[Kim Morrison]

I think this can be fixed just by moving the entire second if statement inside the positive branch of the first if.

[Thomas Murrills]

Is this logic also responsible for telling me what to try to rebase onto initially? (I just used the commits it suggested.) And is there something I could currently rebase onto which would cause CI to run?

[Kim Morrison]

Yes. If you can't rebase onto nightly-with-mathlib, then there is a bug.

[Kim Morrison]

We should only ever be updating Lean's nightly-with-mathlib branch to a nightly if there are green nightly-testing-YYYY-MM-DD branches for that nightly on both Std and Mathlib.

[Kim Morrison]

#3700 should fix this.

[Kim Morrison]

Scott Morrison said:

Yes. If you can't rebase onto nightly-with-mathlib, then there is a bug.

Now, is this also the case here? What did you rebase onto?

[Kim Morrison]

I think the advice message with SHAs in https://github.com/leanprover/lean4/pull/3698#issuecomment-2002134358 is likely wrong, too.

[Kim Morrison]

I'm not really sure why we are advising a rebase onto a SHA. Rebasing onto nightly-with-mathlib is the only thing that ever makes sense.

[Kim Morrison]

This was added in lean4#3417

[Kim Morrison]

@Joachim Breitner

[Thomas Murrills]

Right, I simply used the SHAs suggested, not nightly-with-mathlib!

[Kim Morrison]

Yes, it suggests rebasing onto NIGHTLY_SHA, which is the SHA of the most recent nightly release in your branch. That's just irrelevant, and should be nightly-with-mathlib.

[Kim Morrison]

I'll make this change, but wait until @Joachim Breitner can take a look to confirm I'm not missing something.

[Thomas Murrills]

Just for the record, what’s the easiest way to rebase onto nightly-with-mathlib from a fork? (I’m sure there must be a better way than copying the sha from github.com…)

[Kim Morrison]

lean4#3701

[Kim Morrison]

I would just git checkout nightly-with-mathlib to be honest.

[Kim Morrison]

Thanks very much for reporting these problems!

[Kim Morrison]

There is an obvious tension in our current setup

• the more we can test changes to Lean against Mathlib before they land, the easier it is to keep Mathlib up to date (and then this in turn makes it easier to test changes, because nightly-with-mathlib is fresh!)
• but testing against Mathlib adds a lot of friction to Lean development

[Thomas Murrills]

Hmm, if I git checkout nightly-with-mathlib, I get that the pathspec did not match any file(s) known to git. (Also, would this be something I do before every rebase-onto?)

[Kim Morrison]

Hmm...

% git checkout nightly-with-mathlib
Switched to branch 'nightly-with-mathlib'
Your branch is up to date with 'origin/nightly-with-mathlib'.

[Thomas Murrills]

Scott Morrison said:

Thanks very much for reporting these problems!

Thanks very much for being so responsive about them! :)

[Thomas Murrills]

Is that on a fork?

[Kim Morrison]

I don't think you should have to do this multiple times. Once you have a tracking branch for nightly-with-mathlib, I think it should be sufficient to git fetch && git rebase -i origin/nightly-with-mathlib.

[Kim Morrison]

(And in my experience VSCode is running git fetch often enough that it isn't needed.)

[Thomas Murrills]

Oh, do I have to make nightly-with-testing in my fork as well (or something like that)?

[Thomas Murrills]

Hmm, it looks like my fork is origin, while the lean4 repo is upstream. But I can’t seem to checkout or rebase onto upstream/nightly-with-mathlib:

[Thomas Murrills]

lean4 ▸ git rebase upstream/nightly-with-mathlib
fatal: invalid upstream 'upstream/nightly-with-mathlib'
lean4 ▸ git checkout upstream/nightly-with-mathlib
error: pathspec 'upstream/nightly-with-mathlib' did not match any file(s) known to git

[Thomas Murrills]

The nice thing about SHA's is that everyone can agree on them, and they're always accessible :) (The not-so-nice thing is that the instructions become outdated if nightly-with-mathlib progresses.)

[Thomas Murrills]

Ok, it looks like I have to manually fetch upstream—VS code doesn’t keep that updated by default.

[Thomas Murrills]

Though now I get:

lean4 ▸ git rebase 0b01ceb3bb3334fd6c2f3b24996646046722c62a --onto nightly-with-testing
fatal: Does not point to a valid commit 'nightly-with-testing'

(for whatever variation of nightly-with-testing ( upstream/, origin/) I try) Ok, that's because my brain turns mathlib into testing. :)

[Thomas Murrills]

Ok, all good!

[Thomas Murrills]

Thanks for all the help—I've now rebased lean4#3698 onto nightly-with-mathlib. I guess we'll see what happens!

[Thomas Murrills]

Re: lean4#3701, is origin/nightly-with-mathlib always the right thing to suggest, especially if origin is usually the fork? Does that depend on keeping the branch on the fork in sync with upstream?

[Kim Morrison]

It hadn't occurred to me that people didn't always use origin for the original repository. :-)

[Kim Morrison]

So yes, it is wrong.

[Kim Morrison]

This seems hard to give a reliable suggestion for without using a SHA...

git fetch https://github.com/leanprover/lean4.git nightly-with-mathlib
git rebase FETCH_HEAD

would work?

[Mario Carneiro]

Scott Morrison said:

It hadn't occurred to me that people didn't always use origin for the original repository. :-)

I think github recommends you use origin for your personal fork and upstream for the main repo

[Thomas Murrills]

I'd like to report a minor bug in the message produced by the PR testing automation: in lean4#3973, the message says

Mathlib branch lean-pr-testing-3973 built against this PR, but linting failed. (2024-04-23 01:08:08) View Log

However, it seems that it both failed to build and failed to lint. (Maybe Mathlib CI used to only lint if the build had succeeded, so a failed lint was at least an indication of a successful build?)

[Kim Morrison]

Thanks, I thought I'd fixed that one, will look again. The underlying problem is that Mathlib now runs lint even when the build fails, and the reporting logic has not caught up yet.

[Thomas Murrills]

I'm reviving an old PR (lean4#3973), and the associated batteries branch (lean-pr-testing-3973) seems to have grown stale. I think it needs to be reset to nightly-testing (up to toolchain); or perhaps nightly-testing-YYYY-MM-DD, or some other branch. I'm not exactly sure what should happen here.

[Kyle Miller]

What I normally do is delete the lean-pr-testing-NNNN branches on batteries and mathlib

[Kyle Miller]

They get regenerated the next time you push to your lean branch

[Thomas Murrills]

Ah, nice—letting the automation take over seems like the right thing :)

[Thomas Murrills]

Unfortunately, I don’t have write access to batteries. Could you (or someone with write access) please delete that branch for me?

[Thomas Murrills]

Also, a general question for this topic: to save me and others from having to ask in the future, and to allow me and others to create batteries adaptations when necessary—would it be possible to automatically give lean4 PR authors branch permissions for the associated PR testing branches on batteries?

[Kim Morrison]

That sounds a great idea, but I don't know how to set up permissions like that. If anyone does, I'm happy to implement.

[Kim Morrison]

I've run git branch -D --remote origin/lean-pr-testing-3973.

[Thomas Murrills]

Thanks! :)

[Thomas Murrills]

Hmm, I'm still seeing it for some reason.

[Kyle Miller]

Deleted!

[Thomas Murrills]

Thanks! :grinning_face_with_smiling_eyes:

[Thomas Murrills]

Kim Morrison said:

That sounds a great idea, but I don't know how to set up permissions like that. If anyone does, I'm happy to implement.

As a first step, I found this in the github REST api; if it does what I think, it might not be too terrible. :) (It's possible that it only affects users who already have some other kind of unstated repo permissions, though; I'm not sure.)