PR release failure

Stream: lean4

[Mario Carneiro]

@Scott Morrison do you recognize the error in this CI run? https://github.com/leanprover/lean4/actions/runs/8550153060/job/23426661125

Check merge-base and nightly-testing-YYYY-MM-DD
...
fatal: ambiguous argument 'nightly-with-mathlib': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'

[Kim Morrison]

No, I don't see what's going on. It looks like nightly-with-mathlib currently agrees with nightly (which is correct as Mathlib's nightly-testing just succeeded).

[Sebastian Ullrich]

Which line is supposed to fetch nightly-with-mathlib? I only see fetches of master and the PR head

[Mauricio Collares]

Probably nightly-with-mathlib in https://github.com/leanprover/lean4/actions/runs/8550153060/workflow#L152 should be origin/nightly-with-mathlib?

[Mauricio Collares]

Not sure, because there is a git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit} call which seems to work OK

[Mauricio Collares]

Ah, I guess that's Sebastian's point, nothing fetches nightly-with-mathlib so even origin/nightly-with-mathlib may not work if it's not an ancestor of master or steps.workflow-info.outputs.sourceHeadSha. Sorry for the noise!

[Kim Morrison]

Hopefully fixed in lean4#3834

[Mario Carneiro]

@Kim Morrison I'm still getting this error on all of my PRs on lean4 repo. Latest failure (for a docs change): https://github.com/leanprover/lean4/actions/runs/8691071106/job/23832417854

[Kim Morrison]

Let's see if it works after lean4#3923.

[Joachim Breitner]

This duplicates https://github.com/leanprover/lean4/pull/3914, I guess I should ping you more explicitly when suggesting fixes. (Or just merge more boldly, I admit I forgot about it at the end of the day). Closing mine.

[Kim Morrison]

Sorry, my github inbox overflowed a week or two ago, and I really need to get it back under control. :-(