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.

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

feat: convenience workflow for update major release tag #28

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 39 additions & 0 deletions .github/workflows/update-major-tag.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
name: Update major version tag
run-name: Set ${{ github.event.inputs.major_version }} to point to ${{ github.event.inputs.target }}

# Each time there is a minor release, this workflow can be manually run in order to update the major release tag to point to the latest release.
# Can also be used for rollback if the latest release is found to have problems.

on:
workflow_dispatch:
inputs:
target:
description: The tag or reference to use
required: true
major_version:
type: choice
description: The major version to update
options:
- v1-alpha
- v1
# add items to this list when new major releases are released

jobs:
tag:
runs-on: ubuntu-latest
permissions:
contents: write # required to commit to the repo
steps:
- uses: actions/checkout@v4
with:
fetch-depth: 0
- name: Git config
run: |
git config user.name "github-actions[bot]"
git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
Copy link
Collaborator

@austinletson austinletson May 18, 2024

Choose a reason for hiding this comment

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

Do you have a link to a doc which explains how this github actions bot user works?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I wish there was something in the docs about this! I failed to find anything relevant. The best I can suggest is the conversation on this PR for actions/checkout.

I suspect we can set anything as the git user and the tagging still works, I believe the choice is just to get the correct image when commits are view on gh webpages.

- name: Tag new target
run: git tag -f ${{ github.event.inputs.major_version }} ${{ github.event.inputs.target }}
- name: Push new tag
run: git push origin ${{ github.event.inputs.major_version }} --force

# bot user details: https://api.github.com/users/github-actions%5Bbot%5D
2 changes: 1 addition & 1 deletion RELEASING.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ For more information about releasing GitHub actions see the [Using tags for rele
- Test `lean-action` by pointing an existing test repository to the new version with `uses: leanprover/lean-action@v{RELEASE_VERSION}`.
- Make any minor commits related to the release on the release branch.
- Once the release has been validated, create a new release with release notes copied from the `## Unreleased` section of `CHANGELOG.md` and a git tag `v{RELEASE_VERSION}` (e.g `v2.7.1`).
- In the case of a minor or patch version, move the major version tag to the latest version
- In the case of a minor or patch version, move the major version tag to the latest version. This can be done by manually running the "Update major version tag" workflow.
- Update `CHANGELOG.md` with a new section with the release name and date directly below the `## Unreleased` header, e.g., `## v2.7.1 - 2024-12-21` .
- If you made updates to the release notes in the GitHub release, add them to `CHANGELOG.md`.
- If there are additional commits on the release branch, merge the release branch back into `main`.
Expand Down
Loading