Subtree Update #1
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
| name: Kani Metrics Update | |
| on: | |
| schedule: | |
| - cron: '0 14 * * *' # Run at 14:00 UTC every day | |
| workflow_dispatch: | |
| defaults: | |
| run: | |
| shell: bash | |
| jobs: | |
| update-subtree-library: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout Repository | |
| uses: actions/checkout@v4 | |
| - name: Fetch Kani toolchain version | |
| run: | | |
| mkdir kani-tmp | |
| cd kani-tmp | |
| git init | |
| git remote add origin https://github.com/model-checking/kani | |
| git fetch --depth 1 origin main | |
| git checkout main | |
| TOOLCHAIN_DATE=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' rust-toolchain.toml) | |
| COMMIT_HASH=$(curl https://static.rust-lang.org/dist/$TOOLCHAIN_DATE/channel-rust-nightly-git-commit-hash.txt) | |
| if [ -z "$COMMIT_HASH" ]; then | |
| echo "Could not find commit hash on static.rust-lang.org" | |
| exit 1 | |
| fi | |
| echo "Kani toolchain date: ${TOOLCHAIN_DATE}" | |
| echo "TOOLCHAIN_DATE=${TOOLCHAIN_DATE}" >> $GITHUB_ENV | |
| echo "Kani toolchain hash: ${COMMIT_HASH}" | |
| echo "COMMIT_HASH=${COMMIT_HASH}" >> $GITHUB_ENV | |
| cd .. | |
| rm -r kani-tmp | |
| - name: Update subtree/library locally | |
| run: | | |
| git remote add upstream https://github.com/rust-lang/rust | |
| git fetch upstream | |
| # Ensure "upstream/master" branch contains the target commit | |
| if ! git show ${COMMIT_HASH} --oneline --no-patch; then | |
| echo "Rust commit ${COMMIT_HASH} cannot be found." | |
| exit 1 | |
| fi | |
| # subtree/library has the subtree-split variant of a commit that previously | |
| # went into upstream/master. Running `git subtree split` on top of the | |
| # original commit is much faster (my experiment when working on 280k+ | |
| # commits: 113 seconds vs 613 seconds) than using the HEAD commit from | |
| # subtree/library as base. | |
| SUBTREE_HEAD=$(git log --format=%s -n 1 origin/subtree/library) | |
| echo "SUBTREE_HEAD: ${SUBTREE_HEAD}" | |
| UPSTREAM_ONTO=$(git log --grep="$SUBTREE_HEAD" -n 1 --format=%H upstream/master) | |
| echo "UPSTREAM_ONTO: ${UPSTREAM_ONTO}" | |
| git checkout ${COMMIT_HASH} | |
| git subtree split --prefix=library --onto $UPSTREAM_ONTO -b subtree/library | |
| - name: Create Pull Request | |
| uses: peter-evans/create-pull-request@v7 | |
| with: | |
| title: 'Update subtree/library' | |
| body: | | |
| This is an automated PR to update the subtree/library branch to the changes | |
| up to and including ${{ env.COMMIT_HASH }} of ${{ env.TOOLCHAIN_DATE }}. | |
| branch: update-subtree/library | |
| delete-branch: true | |
| base: subtree/library | |
| - name: Merge subtree/library changes | |
| run: | | |
| SYNC_BRANCH="sync-$TOOLCHAIN_DATE" | |
| git checkout -t -b ${SYNC_BRANCH} origin/main | |
| git submodule update --init | |
| # This command may fail, which will require human intervention. | |
| if ! git subtree merge --prefix=library subtree/library --squash; then | |
| echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV | |
| git commit -a -m "Merge from $COMMIT_HASH with conflicts" | |
| else | |
| echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV | |
| fi | |
| sed -i "s/^channel = \"nightly-.*\"/channel = \"${TOOLCHAIN_DATE}\"/" rust-toolchain.toml | |
| git commit "Update toolchain to ${TOOLCHAIN_DATE}" rust-toolchain.toml | |
| - name: Create Pull Request without conflicts | |
| if: ${{ env.MERGE_CONFLICTS == 'no' }} | |
| uses: peter-evans/create-pull-request@v7 | |
| with: | |
| title: 'Merge subtree update' | |
| body: | | |
| This is an automated PR to merge library subtree updates | |
| up to and including ${{ env.COMMIT_HASH }} of ${{ env.TOOLCHAIN_DATE }} | |
| into main. This is a clean merge, no conflicts were detected. | |
| delete-branch: true | |
| - name: Create Pull Request with conflicts | |
| if: ${{ env.MERGE_CONFLICTS == 'yes' }} | |
| uses: peter-evans/create-pull-request@v7 | |
| with: | |
| title: 'Merge subtree update' | |
| body: | | |
| This is an automated PR to merge library subtree updates | |
| up to and including ${{ env.COMMIT_HASH }} of ${{ env.TOOLCHAIN_DATE }} | |
| into main. `git merge` resulted in conflicts, which require manual resolution. | |
| Files were commited with merge conflict markers. | |
| delete-branch: true |