Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: allow updating stage0 via workflow_dispatch #3052

Merged
merged 2 commits into from
Dec 14, 2023
Merged

chore: allow updating stage0 via workflow_dispatch #3052

merged 2 commits into from
Dec 14, 2023

Conversation

nomeata
Copy link
Contributor

@nomeata nomeata commented Dec 12, 2023

follow-up to #3042

@nomeata nomeata mentioned this pull request Dec 12, 2023
Merged
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 12, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-12 10:37:15)

@nomeata nomeata added the will-merge-soon …unless someone speaks up label Dec 12, 2023
kim-em
kim-em reviewed Dec 12, 2023
View reviewed changes
.github/workflows/update-stage0.yml Outdated
@@ -23,16 +24,17 @@ jobs:
- uses: actions/checkout@v3
with:
ssh-key: ${{secrets.STAGE0_SSH_KEY}}
- name: Check if update is needed
- run: echo "DOIT=yes" >> "$GITHUB_ENV"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not super excited that the flag is named DOIT here!

Copy link
Contributor Author

@nomeata nomeata Dec 13, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Happy to change, any suggestions?

(Is DOIT somehow culturally inappropriate in a way I didn't see, or otherwise not good?)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is should_update_stage0 better?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just unclear. (I have a vendetta against 'it'.)

@kim-em
Copy link
Collaborator

kim-em commented Dec 12, 2023

Could we have a paragraph somewhere (not quite sure the best place? dev guide in the manual?) explaining how to invoke this via workflow_dispatch manually?

@nomeata
Copy link
Contributor Author

nomeata commented Dec 13, 2023

Could we have a paragraph somewhere (not quite sure the best place? dev guide in the manual?) explaining how to invoke this via workflow_dispatch manually?

Good idea, will do. The bootstrapping section of the manual probably

@nomeata nomeata removed the will-merge-soon …unless someone speaks up label Dec 13, 2023
@nomeata nomeata marked this pull request as draft December 13, 2023 07:32
@nomeata nomeata marked this pull request as ready for review December 13, 2023 09:20
@nomeata nomeata added the awaiting-review Waiting for someone to review the PR label Dec 13, 2023
@nomeata
Copy link
Contributor Author

nomeata commented Dec 13, 2023

I changed the flag, and also rewrote the section on updating stage0 in the manual, PTAL

@kim-em kim-em added this pull request to the merge queue Dec 14, 2023
Merged via the queue into master with commit ce15b43 Dec 14, 2023
9 of 13 checks passed
@nomeata nomeata deleted the joachim/update-stage0-dispatch branch December 15, 2023 07:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em approved these changes

@Kha Kha Kha approved these changes

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@nomeata @leanprover-community-mathlib4-bot @kim-em @Kha