chore: CI creates lean-pr-testing-NNNN branches at Std too #3200
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
nomeata
reviewed
Jan 19, 2024
nomeata
reviewed
Jan 19, 2024
nomeata
approved these changes
Jan 19, 2024
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 22, 2024
leanprover-community-mathlib4-bot
added
the
builds-mathlib
nomeata
reviewed
Jan 22, 2024
Comment on lines
-251
to
+321
| git checkout "$BASE" | ||
|
|
||
| EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)" | ||
| echo "Branch exists: $EXISTS" | ||
| if [ "$EXISTS" = "0" ]; then | ||
| echo "Branch does not exist, creating it." | ||
| git checkout -b lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | ||
| git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" |
There was a problem hiding this comment.
Hmm turns out
git switch -c foo base
works if base is a local tag, but not if it is a (remote) branch.
The old code (git checkout base) would work for a (remote) branch, but not for a tag. Kinda annoying.
There was a problem hiding this comment.
Maybe we need to parse this output to go onto a common path in both cases
$ git ls-remote --heads --tags --exit-code https://github.com/leanprover-community/mathlib4 nightly-testing-2024-01-22
7d803278d1b5978fccc14f992d9ffb692077ed93 refs/heads/nightly-testing-2024-01-22
$ git ls-remote --heads --tags --exit-code https://github.com/leanprover/std4 nightly-testing-2024-01-22
c15b5a8f04e84bc7aab8b1062a4a80de3046865f refs/tags/nightly-testing-2024-01-22
Alternatively, we can once manually convert all nightly-testing-YYYY-MM-DD branches to tags on mathlib4. Maybe easier.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Currently we create
lean-pr-testing-NNNNbranches at Mathlib automatically for each Lean PR.We don't automatically create one at Std; mostly simply because Std fails less often, so it has been okay to do this manually as needed. It is conceptually simpler, however, if this is done uniformly.
This PR:
nightly-testing-YYYY-MM-DDtag exists at Std (like it already doesn't proceed if that tag is missing at Mathlib)lean-pr-testing-NNNNbranches at Stdlean-pr-testing-NNNNbranches at Mathlib, updates the Std dependency to use thelean-pr-testing-NNNNbranch at StdNote that because most users do not have write access at Std, in order to make updates to
lean-pr-testing-NNNNbranches there they will need to make PRs. These will be merged with a very low bar, and feel free to ping me for assistance on this. If this is annoying we will automate. Also, frequent contributors to Lean may ask @digama0 or @joehendrix for write access in order to easily work on these branches.This PR requires that we have a secret here with write access at Std. I'm arranging that on zulip.
I will update the documentation at https://leanprover-community.github.io/contribute/tags_and_branches.html to reflect these changes when they are merged.