Zulip Chat Archive

Stream: nightly-testing

Topic: Mergeable lean testing PRs

github mathlib4 bot (Dec 10 2024 at 08:39):

We will need to merge the following branches into nightly-testing:

lean-pr-testing-6342 (lean4#6342) (diff with nightly-testing)

This can be done using the script scripts/merge-lean-testing-pr.sh, which takes 1 lean-PR number as argument.

Kim Morrison (Dec 10 2024 at 08:49):

@Johan Commelin, the script prints sed: 1: "lakefile.lean": extra characters at the end of l command, and still has lean-pr-testing-6242 in the lakefile.

Kim Morrison (Dec 10 2024 at 08:49):

(While we're at it, can the bot just post the script suggestions, with PR numbers, as a code block?)

Johan Commelin (Dec 10 2024 at 09:24):

@Kim Morrison Could it be that sed -i on Linux is different from MacOS?

Johan Commelin (Dec 10 2024 at 09:25):

#!/usr/bin/env bash

if [ "$#" -ne 1 ]; then
    echo "Usage: $0 <PR number>"
    exit 1
fi

PR_NUMBER=$1
BRANCH_NAME="lean-pr-testing-$PR_NUMBER"

git checkout nightly-testing
git pull

if ! git merge origin/$BRANCH_NAME; then
    echo "Merge conflicts detected. Resolving conflicts in favor of current version..."
    git checkout --ours lean-toolchain lakefile.lean lake-manifest.json
    git add lean-toolchain lakefile.lean lake-manifest.json
fi

# I CHANGED THE NEXT TWO LINES
sed "s/$BRANCH_NAME/nightly-testing/g" < lakefile.lean > lakefile.lean.new
mv lakefile.lean.new lakefile.lean
git add lakefile.lean

# Check for merge conflicts
if git ls-files -u | grep -q '^'; then
    echo "Merge conflicts detected. Please resolve conflicts manually."
    git status
    exit 1
fi

if ! lake update; then
    echo "Lake update failed. Please resolve conflicts manually."
    git status
    exit 1
fi

# Attempt to commit. This will fail if there are conflicts.
if git commit -m "merge $BRANCH_NAME"; then
    echo "Merge successful."
    exit 0
else
    echo "Merge failed. Please resolve conflicts manually."
    git status
    exit 1
fi

Johan Commelin (Dec 10 2024 at 09:25):

In this new version, I'm writing the output of sed to a new file, and moving that back to lakefile.lean.

Johan Commelin (Dec 10 2024 at 09:25):

Hopefully that is more robust.

Ruben Van de Velde (Dec 10 2024 at 09:35):

I believe macos infamously comes with BSD sed, with a surprising number of incompatibilities

Johan Commelin (Dec 10 2024 at 09:44):

#19857 should fix the sed and also make the zulip post more useful.

github mathlib4 bot (Dec 11 2024 at 08:36):

We will need to merge the following branches into nightly-testing:

lean-pr-testing-3696 (lean4#3696) (diff with nightly-testing)
lean-pr-testing-6341 (lean4#6341) (diff with nightly-testing)

This can be done using the script scripts/merge-lean-testing-pr.sh, which takes 1 lean-PR number as argument.

Kim Morrison (Dec 11 2024 at 09:59):

Johan Commelin said:

#19857 should fix the sed and also make the zulip post more useful.

Needs actionlint fixes.

Johan Commelin (Dec 11 2024 at 12:31):

Ghaaarhg. Should be fixed now.

Johan Commelin (Dec 11 2024 at 12:31):

Actionlint should get a reward for "most pedantic linter evah"

Kim Morrison (Dec 14 2024 at 10:29):

Hmm, this didn't mention lean#6123, which needs to be merged now.

Johan Commelin (Dec 14 2024 at 11:15):

Hmm, weird. I'll check the workflow run.

Johan Commelin (Dec 14 2024 at 12:21):

The 13-Dec workflow run failed because there was a branch containing a lean pr number in its name, without being a lean-pr-testing branch.

The 14-Dec workflow run failed for a reason I do not yet understand.

I've created #19958 as a WIP for fixing these. @Damiano Testa if you have a few minutes to look at the 14-Dec run, that would be great!

Damiano Testa (Dec 14 2024 at 13:23):

Taking a look right now!

Damiano Testa (Dec 14 2024 at 13:25):

I suspect is the backticks in

if [ -z "
  - lean-pr-testing-6123 (lean4#6123) ([diff with `nightly-testing`](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6123))" ]; then
    echo "branches_exist=false" >> "$GITHUB_ENV"
  else
    echo "branches_exist=true" >> "$GITHUB_ENV"
  fi

where it says diff with `nightly-testing`

Damiano Testa (Dec 14 2024 at 13:25):

The backticks are a way to get bash to parse a command, an old form of $((cmd)).

Damiano Testa (Dec 14 2024 at 13:26):

If you want to use them, they should be escaped, I think.

Johan Commelin (Dec 14 2024 at 13:26):

Hmm, or maybe we should use that as argument to if [ -z?

Damiano Testa (Dec 14 2024 at 13:26):

Then, the error

/home/runner/work/_temp/ec4ff2ad-a356-411c-8c3c-cda95e19fac8.sh: line 1: nightly-testing: command not found

is telling you that nightly-testing is not a command.

Johan Commelin (Dec 14 2024 at 13:28):

Sorry, I meant "should not"

Damiano Testa (Dec 14 2024 at 13:28):

On my version of bash, using \` seems to work.

Johan Commelin (Dec 14 2024 at 13:28):

Nice. Would you mind pushing a fix to the PR I posted upstairs?

Damiano Testa (Dec 14 2024 at 13:31):

Oh, I see that in the workflow they are already escaped, but then they are laundered through a github variable.

Damiano Testa (Dec 14 2024 at 13:32):

I think that this needs to be a little more structurally robust: I'll see if I can recreate the message when it is printed, passing only "clean" information through github environment variables.

Damiano Testa (Dec 14 2024 at 13:54):

I just pushed a possible fix: rather than "escaping more", I made the previous CI step also create the github environment variable, using the same bash variable that seemed to work for creating the message. Hopefully this sidesteps "escaping after github laundering", which seemed iffy.

Johan Commelin (Dec 14 2024 at 13:58):

That sounds like a good idea!

Johan Commelin (Dec 16 2024 at 09:08):

@Damiano Testa Somehow this didn't fix it...

Johan Commelin (Dec 16 2024 at 09:08):

https://github.com/leanprover-community/mathlib4/actions/runs/12348832176/job/34458412247#step:7:21

Johan Commelin (Dec 16 2024 at 09:08):

I'm not sure what we're doing wrong now

Damiano Testa (Dec 16 2024 at 09:09):

The error message is the same, so maybe my earlier diagnosis was incorrect.

Damiano Testa (Dec 16 2024 at 09:11):

It seems like there is an environment variable called branches_exist: true, which is good, though. So maybe we did progress last time.

Damiano Testa (Dec 16 2024 at 09:24):

I suspect that the issue is again with escaping backticks, so I tried something at #19991.

Johan Commelin (Dec 16 2024 at 09:27):

Thanks! That looks like it might be it!

Johan Commelin (Dec 16 2024 at 09:27):

It's in the right part of the CI workflow

Damiano Testa (Dec 16 2024 at 09:28):

I am not really sure whether this will fix it, since it is still backticks that go into github variables. However, I think that it is the shell that is complaining in CI and, on my computer, with the new bash escapes I see the backticks, while I get the error with the double quotes.

Damiano Testa (Dec 16 2024 at 09:29):

It is very unfortunate that backticks mean different things in the shell and on Zulip.

Damiano Testa (Dec 16 2024 at 09:31):

This action is triggered by a push to nightly-testing that touches the toolchain, right? Once the "fix" is in, is it possible to trigger the action to see that it works?

Johan Commelin (Dec 16 2024 at 09:48):

I'm not sure it is easy to trigger, without pushing a commit that touches the toolchain.

Damiano Testa (Dec 16 2024 at 09:48):

Is whitespace in the toolchain relevant?

Johan Commelin (Dec 16 2024 at 09:49):

For the record, these were the relevant branches in today's run:

lean-pr-testing-6379 (lean4#6379) (diff with nightly-testing)
lean-pr-testing-6390 (lean4#6390) (diff with nightly-testing)

Damiano Testa (Dec 16 2024 at 09:50):

Anyway, if it is hard to test, then we can have a similar exchange tomorrow! :smile:

Kim Morrison (Dec 21 2024 at 10:04):

The bot didn't report lean-pr-testing-6397, which should have been merged at nightly-2024-12-21.

Johan Commelin (Dec 21 2024 at 10:06):

:sad: I'll look into what went wrong.

Johan Commelin (Dec 21 2024 at 10:08):

I can confirm that 6397 is the only one that needs merging.

Johan Commelin (Dec 21 2024 at 10:08):

The bot still seems to choke on some quoting.

Johan Commelin (Dec 21 2024 at 10:11):

@Kim Morrison I really hope that #20152 fixes this.

Johan Commelin (Dec 21 2024 at 11:18):

#20153 is another attempt, really getting rid of the ` s

Johan Commelin (Dec 21 2024 at 14:44):

It is still broken, and I don't understand why :sad:

Error: Process completed with exit code 1.
Error: Unable to process file command 'output' successfully.
Error: Invalid value. Matching delimiter not found 'EOF'

Johan Commelin (Dec 21 2024 at 14:44):

https://github.com/leanprover-community/mathlib4/actions/runs/12446031681/job/34747987337#step:7:21

Bryan Gin-ge Chen (Dec 21 2024 at 15:19):

I can try and take a look later today.

Edward van de Meent (Dec 21 2024 at 16:54):

i'm having a look right now

Edward van de Meent (Dec 21 2024 at 17:35):

~~i know the issue! it's complaining that there is no EOF found: this is because this line uses the wrong kind of quotation marks!~~

Edward van de Meent (Dec 21 2024 at 18:31):

i think i've pretty much fixed it now. here's an example message:

Edward van de Meent (Dec 21 2024 at 18:31):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-1
scripts/merge-lean-testing-pr.sh 1   # lean-pr-testing-1
# # # # #
# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-2
scripts/merge-lean-testing-pr.sh 2   # lean-pr-testing-2
# # # # #
# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3489
scripts/merge-lean-testing-pr.sh 3489   # lean-pr-testing-3489
# # # # #

Edward van de Meent (Dec 21 2024 at 18:32):

i'm not sure the line with hashes makes this more readable, and removing them should be pretty easy... opinions?

Edward van de Meent (Dec 21 2024 at 18:32):

(im not sure what the purpose of them was to begin with)

Ruben Van de Velde (Dec 21 2024 at 18:46):

Added in #20153?

Johan Commelin (Dec 21 2024 at 18:47):

I added them to make it clear which Diff: and scripts/ lines belonged together. Happy to do something else there.

Johan Commelin (Dec 21 2024 at 18:48):

Also: thanks a lot for fixing it! What was the issue in the end?

Edward van de Meent (Dec 21 2024 at 19:11):

the way i understand it, the main issue was that the $BRANCHES variable was given a value that doesn't work well with for ... in $BRANCHES; do bla.

Johan Commelin (Dec 21 2024 at 19:13):

Do you have a PR that fixes that? I would be happy to merge it :grinning:

Ruben Van de Velde (Dec 21 2024 at 19:13):

May I suggest that shell scripting is the only language that's terrible in this way? :innocent:

Edward van de Meent (Dec 21 2024 at 19:16):

if all is well, #20163 should fix it

Edward van de Meent (Dec 21 2024 at 19:17):

darn actionlint

Edward van de Meent (Dec 21 2024 at 19:18):

there

Edward van de Meent (Dec 21 2024 at 21:08):

since the fix is now merged into master, it should start working again once master is merged into nightly-testing

Edward van de Meent (Dec 21 2024 at 21:09):

(or once the fix is cherry-picked onto nightly-testing. that may cause a merge conflict once master does get merged into the branch, though)

github mathlib4 bot (Dec 21 2024 at 21:19):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6397
scripts/merge-lean-testing-pr.sh 6397   # lean-pr-testing-6397

Johan Commelin (Dec 21 2024 at 21:24):

Finally, #20165 reverts a change, so that this workflow will only run when lean-toolchain changes. Otherwise the bot will be spammy. (But a spammy bot was useful for testing.)

github mathlib4 bot (Dec 21 2024 at 21:32):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6397
scripts/merge-lean-testing-pr.sh 6397   # lean-pr-testing-6397

Edward van de Meent (Dec 21 2024 at 21:32):

if we make sure that there are no PRs to merge, it also won't be spammy :upside_down:

github mathlib4 bot (Jan 01 2025 at 08:38):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6473
scripts/merge-lean-testing-pr.sh 6473   # lean-pr-testing-6473

github mathlib4 bot (Jan 14 2025 at 10:08):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6602
scripts/merge-lean-testing-pr.sh 6602   # lean-pr-testing-6602

github mathlib4 bot (Jan 16 2025 at 08:42):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6660
scripts/merge-lean-testing-pr.sh 6660   # lean-pr-testing-6660

github mathlib4 bot (Jan 27 2025 at 08:49):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6755
scripts/merge-lean-testing-pr.sh 6755   # lean-pr-testing-6755

Joachim Breitner (Jan 27 2025 at 10:06):

Ah, did that manually right now.

github mathlib4 bot (Jan 29 2025 at 11:54):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6800
scripts/merge-lean-testing-pr.sh 6800   # lean-pr-testing-6800

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6812
scripts/merge-lean-testing-pr.sh 6812   # lean-pr-testing-6812

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6826
scripts/merge-lean-testing-pr.sh 6826   # lean-pr-testing-6826

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

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6863
scripts/merge-lean-testing-pr.sh 6863   # lean-pr-testing-6863

github mathlib4 bot (Feb 04 2025 at 08:45):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6823
scripts/merge-lean-testing-pr.sh 6823   # lean-pr-testing-6823

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

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7013
scripts/merge-lean-testing-pr.sh 7013   # lean-pr-testing-7013

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

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7046
scripts/merge-lean-testing-pr.sh 7046   # lean-pr-testing-7046

github mathlib4 bot (Feb 14 2025 at 08:56):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7050
scripts/merge-lean-testing-pr.sh 7050   # lean-pr-testing-7050

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

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7059
scripts/merge-lean-testing-pr.sh 7059   # lean-pr-testing-7059

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7069
scripts/merge-lean-testing-pr.sh 7069   # lean-pr-testing-7069

Kim Morrison (Feb 17 2025 at 11:19):

(Also merged lean-pr-testing-7059 at Batteries and Aesop)

github mathlib4 bot (Feb 18 2025 at 08:56):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7103
scripts/merge-lean-testing-pr.sh 7103   # lean-pr-testing-7103

github mathlib4 bot (Feb 19 2025 at 08:45):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7082
scripts/merge-lean-testing-pr.sh 7082   # lean-pr-testing-7082

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7100
scripts/merge-lean-testing-pr.sh 7100   # lean-pr-testing-7100

Kim Morrison (Feb 19 2025 at 08:51):

branch#lean-pr-testing-7100 had quite a few merge conflicts, but I think I have them sorted.

github mathlib4 bot (Feb 24 2025 at 23:47):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7196
scripts/merge-lean-testing-pr.sh 7196   # lean-pr-testing-7196

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

This script seems to be working pretty reliably, so we should consider the following two updates:

Can we run it also on batteries and aesop?
Can we just let it run the suggestion automatically?

github mathlib4 bot (Mar 01 2025 at 08:45):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7259
scripts/merge-lean-testing-pr.sh 7259   # lean-pr-testing-7259

github mathlib4 bot (Mar 04 2025 at 08:59):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7075
scripts/merge-lean-testing-pr.sh 7075   # lean-pr-testing-7075

github mathlib4 bot (Mar 05 2025 at 08:52):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7075
scripts/merge-lean-testing-pr.sh 7075   # lean-pr-testing-7075

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7166
scripts/merge-lean-testing-pr.sh 7166   # lean-pr-testing-7166

Kim Morrison (Mar 06 2025 at 05:10):

I guess these two were done? @Johan Commelin, if you could emoji them when doing (or done) that would be great, so I can tell.

Damiano Testa (Mar 06 2025 at 05:27):

Would these get tagged as closed by the emoji automation, if the messages posted by the bot contained a PR number?

Johan Commelin (Mar 06 2025 at 05:50):

Nope, I had trouble running the script. So I'll now do them manually.

Johan Commelin (Mar 06 2025 at 05:56):

Now they are done.

github mathlib4 bot (Mar 06 2025 at 09:25):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7075
scripts/merge-lean-testing-pr.sh 7075   # lean-pr-testing-7075

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7166
scripts/merge-lean-testing-pr.sh 7166   # lean-pr-testing-7166

github mathlib4 bot (Mar 07 2025 at 08:52):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7261
scripts/merge-lean-testing-pr.sh 7261   # lean-pr-testing-7261

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7358
scripts/merge-lean-testing-pr.sh 7358   # lean-pr-testing-7358

Sebastian Ullrich (Mar 07 2025 at 09:53):

I thought I should give this workflow a try myself some time (and also I'm impatient). I encountered two minor issues:

the initial git pull should likely use --ff, it tried to initiate a rebase for me when running the two commands sequentially without a push in between
I almost forgot to commit the lake update result, shouldn't that be automated as well?

github mathlib4 bot (Mar 08 2025 at 08:59):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7378
scripts/merge-lean-testing-pr.sh 7378   # lean-pr-testing-7378

Johan Commelin (Mar 08 2025 at 09:30):

@Sebastian Ullrich #22709 adds the --ff-only.
About the lake update... isn't that running inside the if statement? So on the happy path, it is automated.
I agree that this script could try to be more helpful on the unhappy path...

Sebastian Ullrich (Mar 08 2025 at 09:33):

Ohh, it does a git commit afterwards but it does not pick up the lake update changes because the git add is before that

Johan Commelin (Mar 10 2025 at 05:18):

#22709 now also has a git add before the git commit.

github mathlib4 bot (Mar 12 2025 at 09:01):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7334
scripts/merge-lean-testing-pr.sh 7334   # lean-pr-testing-7334

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7435
scripts/merge-lean-testing-pr.sh 7435   # lean-pr-testing-7435

Kim Morrison (Mar 14 2025 at 02:38):

I'm going to be away over the weekend, and we have quite a number of lean-pr-testing-NNNN branches that will need merging into various repositories when the next nightly arrives:

lean-pr-testing-7447 needs to be merged into nightly-testing at Batteries, aesop, ProofWidgets (and set the toolchains back to the new nightly) (and then we'll need to tag v0.0.54-pre there, and have Mathlib's nightly-testing use it), and Mathlib
- Note that lean-pr-testing-7447 on Mathlib isn't building successfully, but I think it will come good on nightly-testing; the problems are from other PRs, fixed elsewhere.
lean-pr-testing-7445 needs to be merged into nightly-testing at Batteries and Mathlib (same caveat about Mathlib applies)
lean-pr-testing-7240 needs to be merged into nightly-testing at Batteries and Mathlib
lean-pr-testing-7451 needs to be merged into nightly-testing at Mathlib.
lean-pr-testing-7466 needs to be merged into nightly-testing at Batteries and Mathlib.

Good luck! :-)

github mathlib4 bot (Mar 14 2025 at 09:00):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7240
scripts/merge-lean-testing-pr.sh 7240   # lean-pr-testing-7240

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7445
scripts/merge-lean-testing-pr.sh 7445   # lean-pr-testing-7445

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7447
scripts/merge-lean-testing-pr.sh 7447   # lean-pr-testing-7447

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7451
scripts/merge-lean-testing-pr.sh 7451   # lean-pr-testing-7451

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7466
scripts/merge-lean-testing-pr.sh 7466   # lean-pr-testing-7466

Sebastian Ullrich (Mar 14 2025 at 09:27):

I've done all of these except for ProofWidgets for which I don't have push rights

Johan Commelin (Mar 14 2025 at 10:41):

I've done proofwidgets

Sebastian Ullrich (Mar 14 2025 at 12:30):

@Johan Commelin Is the tag still missing?

Johan Commelin (Mar 14 2025 at 12:32):

Whoops. Let me fix that.

Johan Commelin (Mar 14 2025 at 12:41):

@Sebastian Ullrich https://github.com/leanprover-community/ProofWidgets4/releases/tag/v0.0.54-pre

Sebastian Ullrich (Mar 14 2025 at 12:42):

Thanks! I updated nightly-testing

Johan Commelin (Mar 14 2025 at 12:42):

The mathlib one?

Sebastian Ullrich (Mar 14 2025 at 12:42):

yes

Johan Commelin (Mar 14 2025 at 12:43):

excellent, thanks!

github mathlib4 bot (Mar 15 2025 at 08:58):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7084
scripts/merge-lean-testing-pr.sh 7084   # lean-pr-testing-7084

github mathlib4 bot (Mar 16 2025 at 14:31):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7485
scripts/merge-lean-testing-pr.sh 7485   # lean-pr-testing-7485

github mathlib4 bot (Mar 17 2025 at 09:04):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7516
scripts/merge-lean-testing-pr.sh 7516   # lean-pr-testing-7516

Kim Morrison (Mar 17 2025 at 12:14):

Also needs merging at batteries and plausible.

github mathlib4 bot (Mar 18 2025 at 09:03):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7487
scripts/merge-lean-testing-pr.sh 7487   # lean-pr-testing-7487

github mathlib4 bot (Mar 19 2025 at 09:04):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7522
scripts/merge-lean-testing-pr.sh 7522   # lean-pr-testing-7522

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7558
scripts/merge-lean-testing-pr.sh 7558   # lean-pr-testing-7558

Kim Morrison (Mar 20 2025 at 22:28):

Hm, the bot did not report lean#5182.

Kim Morrison (Mar 21 2025 at 00:41):

lean-pr-testing-7544 will need merging tonight, at Batteries, Aesop, and Mathlib.

(I'll be offline, so if someone could take care of this that would be great!)

github mathlib4 bot (Mar 21 2025 at 10:39):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7519
scripts/merge-lean-testing-pr.sh 7519   # lean-pr-testing-7519

github mathlib4 bot (Mar 22 2025 at 09:00):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7614
scripts/merge-lean-testing-pr.sh 7614   # lean-pr-testing-7614

Kyle Miller (Mar 23 2025 at 18:27):

Kim Morrison said:

lean-pr-testing-7544 will need merging tonight, at Batteries, Aesop, and Mathlib.

It looks like this has been done, but I can't tell exactly. At least Batteries and Aesop build. Checking Mathlib.

Edit: Oh, lean4#7544 has not been merged yet. Reverting that merge to nightly-testing

github mathlib4 bot (Mar 24 2025 at 14:57):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7302
scripts/merge-lean-testing-pr.sh 7302   # lean-pr-testing-7302

Kyle Miller (Mar 24 2025 at 15:35):

Looks like 7544 is needed now. I'll merge.

Kyle Miller (Mar 24 2025 at 15:39):

I did Mathlib, but it looks like Aesop and Batteries need updates too.

Kyle Miller (Mar 24 2025 at 16:02):

lean4#7650 is missing a testing PR. Not too many things seem broken at least

Markus Himmel (Mar 24 2025 at 16:03):

Yes, see the discussion at #lean4 > argument order in`count_cons_of_ne` @ 💬

Kyle Miller (Mar 24 2025 at 16:14):

The change from Vector to Array caused Mathlib.Tactic.Order.updateGraphWithNlt to need !'s on some indexing. I wasn't sure if we wanted to leave an adaptation note — so I'm leaving a message here in case anyone wants to add one.

Kim Morrison (Mar 24 2025 at 23:40):

I've fixed.

github mathlib4 bot (Mar 26 2025 at 09:08):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7672
scripts/merge-lean-testing-pr.sh 7672   # lean-pr-testing-7672

github mathlib4 bot (Mar 27 2025 at 09:07):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7690
scripts/merge-lean-testing-pr.sh 7690   # lean-pr-testing-7690

Kim Morrison (Mar 27 2025 at 09:36):

Also at Batteries.

Kim Morrison (Mar 27 2025 at 11:08):

We will need to merge the branch pre-2025-03-28 when tomorrow's nightly lands, at Batteries, Aesop, and Mathlib. (We've reverted lean#7679, but because of stage0 issues we had to do this direct on master, so there isn't a lean-pr-testing-NNNN toolchain to try it out on.)

Kim Morrison (Mar 27 2025 at 11:09):

(So I've built locally and am using elan toolchain override like in the good old days.)

github mathlib4 bot (Mar 28 2025 at 09:25):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7692
scripts/merge-lean-testing-pr.sh 7692   # lean-pr-testing-7692

Johan Commelin (Mar 31 2025 at 07:21):

Let me advertise

scripts/merge-lean-testing-pr): push to github after successful merge #23265

github mathlib4 bot (Mar 31 2025 at 09:37):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7710
scripts/merge-lean-testing-pr.sh 7710   # lean-pr-testing-7710

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7717
scripts/merge-lean-testing-pr.sh 7717   # lean-pr-testing-7717

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7736
scripts/merge-lean-testing-pr.sh 7736   # lean-pr-testing-7736

Kim Morrison (Mar 31 2025 at 09:44):

I've merged these, but there were some merge conflicts from lean-pr-testing-7717 (cf lean#7717) which I'm not certain I got right.

Kim Morrison (Mar 31 2025 at 09:52):

I've also merged these three into Batteries.

github mathlib4 bot (Apr 01 2025 at 09:23):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7764
scripts/merge-lean-testing-pr.sh 7764   # lean-pr-testing-7764

github mathlib4 bot (Apr 02 2025 at 10:41):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7756
scripts/merge-lean-testing-pr.sh 7756   # lean-pr-testing-7756

github mathlib4 bot (Apr 03 2025 at 14:08):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6325
scripts/merge-lean-testing-pr.sh 6325   # lean-pr-testing-6325

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7774
scripts/merge-lean-testing-pr.sh 7774   # lean-pr-testing-7774

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7791
scripts/merge-lean-testing-pr.sh 7791   # lean-pr-testing-7791

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7797
scripts/merge-lean-testing-pr.sh 7797   # lean-pr-testing-7797

github mathlib4 bot (Apr 04 2025 at 09:05):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7812
scripts/merge-lean-testing-pr.sh 7812   # lean-pr-testing-7812

github mathlib4 bot (Apr 05 2025 at 09:24):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7499
scripts/merge-lean-testing-pr.sh 7499   # lean-pr-testing-7499

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7802
scripts/merge-lean-testing-pr.sh 7802   # lean-pr-testing-7802

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7816
scripts/merge-lean-testing-pr.sh 7816   # lean-pr-testing-7816

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7818
scripts/merge-lean-testing-pr.sh 7818   # lean-pr-testing-7818

Kim Morrison (Apr 06 2025 at 22:39):

Done for Batteries too.

Kim Morrison (Apr 06 2025 at 23:44):

Kim Morrison said:

This script seems to be working pretty reliably, so we should consider the following two updates:

Can we just let it run the suggestion automatically?

#23746 upgrades this script to try running automatically.

github mathlib4 bot (Apr 07 2025 at 09:12):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7474
scripts/merge-lean-testing-pr.sh 7474   # lean-pr-testing-7474

github mathlib4 bot (Apr 07 2025 at 16:32):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7812
scripts/merge-lean-testing-pr.sh 7812   # lean-pr-testing-7812

github mathlib4 bot (Apr 07 2025 at 19:03):

We will need to merge the following branches into nightly-testing:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7474
scripts/merge-lean-testing-pr.sh 7474   # lean-pr-testing-7474

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7499
scripts/merge-lean-testing-pr.sh 7499   # lean-pr-testing-7499

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7802
scripts/merge-lean-testing-pr.sh 7802   # lean-pr-testing-7802

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7816
scripts/merge-lean-testing-pr.sh 7816   # lean-pr-testing-7816

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7818
scripts/merge-lean-testing-pr.sh 7818   # lean-pr-testing-7818

Kim Morrison (Apr 08 2025 at 01:14):

These were all empty?

Johan Commelin (Apr 08 2025 at 06:10):

Weird...

Johan Commelin (Apr 08 2025 at 06:11):

I thought detection of empty merges worked quite reliably.

github mathlib4 bot (Apr 09 2025 at 10:48):

No branches were successfully merged.

:cross_mark: Failed merges:

The following branches need to be merged manually:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7851
scripts/merge-lean-testing-pr.sh 7851   # lean-pr-testing-7851

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7856
scripts/merge-lean-testing-pr.sh 7856   # lean-pr-testing-7856

Kim Morrison (Apr 09 2025 at 11:44):

These work fine locally, so we need to work out why the bot couldn't cope. Presumably it is just giving up when there is a merge conflict.

Johan Commelin (Apr 10 2025 at 04:11):

https://github.com/leanprover-community/mathlib4/actions/runs/14355252835/job/40243094946#step:7:77 is the relevant action log

Johan Commelin (Apr 10 2025 at 04:19):

script is failing because lake isn't found. Fix incoming

Johan Commelin (Apr 10 2025 at 04:25):

#23900 install elan in the workflow

Johan Commelin (Apr 10 2025 at 04:29):

Is this the correct thing to do nowadays? Or should we use lean-action? cc @Anne Baanen

Kim Morrison (Apr 10 2025 at 04:58):

We should be using lean-action eventually, but for now it's okay.

Kim Morrison (Apr 10 2025 at 06:42):

We will need to merge lean-pr-testing-7873 for lean#7873 into batteries, import-graph, as well as Mathlib, tonight.

Kim Morrison (Apr 10 2025 at 08:52):

Kim Morrison said:

We will need to merge lean-pr-testing-7873 for lean#7873 into batteries, import-graph, as well as Mathlib, tonight.

Done.

Anne Baanen (Apr 10 2025 at 08:53):

Johan Commelin said:

Is this the correct thing to do nowadays? Or should we use lean-action? cc Anne Baanen

Actually I just replaced all the elan-init scripts with lean-action. But I was going to touch this bit of CI anyway today :)

Johan Commelin (Apr 14 2025 at 09:32):

@Damiano Testa Still multiline problems, it seems. Do you think #24029 looks sensible?

Johan Commelin (Apr 14 2025 at 09:33):

Trying to address https://github.com/leanprover-community/mathlib4/actions/runs/14441337845/job/40491967612

Damiano Testa (Apr 14 2025 at 09:39):

I left a comment.

Damiano Testa (Apr 14 2025 at 09:46):

Wait, I think that the error was pointing out something different.

Damiano Testa (Apr 14 2025 at 09:49):

The error is complaining about

MESSAGE+=$(printf '- lean#%s ([diff](%s))\n' "$PR_NUMBER" "$GITHUB_DIFF")

bash is reading the printf as printf - lean... and thinks that - is introducing a flag to printf and it does not know what the empty flag is. Try with

MESSAGE+=$(printf -- '- lean#%s ([diff](%s))\n' "$PR_NUMBER" "$GITHUB_DIFF")

to let printf know that it should not be looking for printf-flags after the --.

Johan Commelin (Apr 14 2025 at 09:56):

Ooh! Aha.

Johan Commelin (Apr 14 2025 at 10:57):

The good news is that this bot tried to post:

:check: Successfully merged lean-pr-testing-7870
:check: Successfully merged lean-pr-testing-7897

Otoh, the merge looks empty, which is not good.

Damiano Testa (Apr 14 2025 at 10:58):

At least the "trivial" multiline issues look resolved! :octopus:

Johan Commelin (Apr 14 2025 at 11:02):

It didn't run again, yet, right?

Damiano Testa (Apr 14 2025 at 11:04):

Ah, I interpreted your message as saying that it did run again!

Damiano Testa (Apr 14 2025 at 11:05):

Btw, if you make the action on: workflow_dispatch:

on:
  ...
  workflow_dispatch:

then you can trigger it manually, which may be good for testing.

github mathlib4 bot (Apr 16 2025 at 08:39):

:check: Successfully merged branches:

lean#7933 (diff)- lean#7975 (diff)
All branches were successfully merged! :tada:

Damiano Testa (Apr 16 2025 at 08:42):

The diff links are not too informative and the lean#nnnn links should maybe point to https://github.com/leanprover-community/mathlib4/compare/lean-pr-testing-nnnn?

Johan Commelin (Apr 16 2025 at 11:09):

Wouldn't that compare them with master? Which will probably show a gigantic diff.

Damiano Testa (Apr 16 2025 at 11:10):

Ah, you are right! But is it meaningful that those diffs above is empty? Could it be something else, once they are merged?

Kim Morrison (Apr 16 2025 at 22:18):

Yes, they should be a diff against the most recent nightly-testing-YYYY-MM-DD tag in their history. That is where they departed from nightly-testing.

github mathlib4 bot (Apr 17 2025 at 09:22):

:check: Successfully merged branches:

lean#7855 (diff)- lean#7983 (diff)

:cross_mark: Failed merges:

The following branches need to be merged manually:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-7971scripts/merge-lean-testing-pr.sh 7971   # lean-pr-testing-7971```

github mathlib4 bot (Apr 22 2025 at 08:46):

No branches were successfully merged.

:cross_mark: Failed merges:

The following branches need to be merged manually:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-6432scripts/merge-lean-testing-pr.sh 6432   # lean-pr-testing-6432```

Kim Morrison (Apr 22 2025 at 20:03):

The bot failed to notice that lean-pr-testing-8021 needed merging.

github mathlib4 bot (Apr 26 2025 at 09:33):

:check: Successfully merged branches:

lean#8000 (diff)
All branches were successfully merged! :tada:

Kim Morrison (Apr 26 2025 at 12:52):

We really need to make this run on Batteries too, I'm doing this manually still.

github mathlib4 bot (Apr 29 2025 at 09:14):

:check: Successfully merged branches:

lean#8144 (diff)
All branches were successfully merged! :tada:

github mathlib4 bot (Apr 30 2025 at 09:17):

No branches were successfully merged.

:cross_mark: Failed merges:

The following branches need to be merged manually:

# Diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-8161scripts/merge-lean-testing-pr.sh 8161   # lean-pr-testing-8161```

Kim Morrison (Apr 30 2025 at 09:25):

Done manually.

Kim Morrison (Apr 30 2025 at 09:29):

and hopefully #24468 will fix the formatting of the messages posted by this bot

Last updated: May 02 2025 at 03:31 UTC