Subtree Update Automation Fixes (#250)

Improvements to the workflow to update the subtree:
- Check for existing PRs before creating new ones
- Update the Kani version automatically
- Remove erroneous additional submodules
- Typo in toolchain file

Resolves #249

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Michael Tautschnig <[email protected]>

Author: 3 people

.github/workflows/update-subtree.yml

@@ -58,8 +58,27 @@ jobs:
         echo "NEXT_TOOLCHAIN_DATE=${NEXT_TOOLCHAIN_DATE}" >> $GITHUB_ENV
         echo "CURRENT_COMMIT_HASH=${CURRENT_COMMIT_HASH}" >> $GITHUB_ENV
         echo "NEXT_COMMIT_HASH=${NEXT_COMMIT_HASH}" >> $GITHUB_ENV
+        KANI_COMMIT_HASH=$(git -C kani-tmp rev-parse HEAD)
+        echo "KANI_COMMIT_HASH=${KANI_COMMIT_HASH}" >> $GITHUB_ENV
+
+    - name: Check for existing pull requests
+      run: |
+        cd verify-rust-std
+        if gh pr list --json title --jq '.[] | select(.title | startswith("Update subtree/library to")) | .title' | grep -q .; then
+          echo "SUBTREE_PR_EXISTS=yes" >> $GITHUB_ENV
+        else
+          echo "SUBTREE_PR_EXISTS=no" >> $GITHUB_ENV
+        fi
+        if gh pr list --json title --jq '.[] | select(.title | startswith("Merge subtree update for toolchain nightly-")) | .title' | grep -q .; then
+          echo "MERGE_PR_EXISTS=yes" >> $GITHUB_ENV
+        else
+          echo "MERGE_PR_EXISTS=no" >> $GITHUB_ENV
+        fi
+      env:
+        GH_TOKEN: ${{ github.token }}
 
     - name: Update subtree/library locally
+      if: ${{ env.SUBTREE_PR_EXISTS == 'no' }}
       run: |
         cd rust-tmp
 
@@ -77,6 +96,9 @@ jobs:
         git remote add rust-filtered ../rust-tmp/
         git fetch rust-filtered
         git checkout -b subtree/library rust-filtered/subtree/library
+        # The filter-subtree operation adds an extraneous `library/` folder containing the submodules
+        # (c.f. https://github.com/model-checking/verify-rust-std/issues/249), so remove that before committing.
+        rm -rf library
         SUBTREE_HEAD_MSG=$(git log --format=%s -n 1 origin/subtree/library)
         UPSTREAM_FROM=$(git log --grep="${SUBTREE_HEAD_MSG}" -n 1 --format=%H rust-filtered/subtree/library)
         UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)
@@ -89,22 +111,23 @@ jobs:
           echo "MERGE_CONFLICTS=maybe" >> $GITHUB_ENV
         fi
 
-    - name: Create Pull Request
-      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+    - name: Create Pull Request to update subtree/library
+      if: ${{ env.MERGE_CONFLICTS != 'noop' && env.SUBTREE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Update subtree/library to ${{ env.NEXT_TOOLCHAIN_DATE }}'
         body: |
           This is an automated PR to update the subtree/library branch to the changes
           from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
           to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
+          **Do not merge this PR using the merge queue. Instead, use the rebase strategy.**
         branch: update-subtree/library
         delete-branch: true
         base: subtree/library
         path: verify-rust-std
 
     - name: Merge subtree/library changes
-      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+      if: ${{ env.MERGE_CONFLICTS != 'noop' && env.MERGE_PR_EXISTS == 'no' }}
       run: |
         cd verify-rust-std
         git checkout main
@@ -119,12 +142,15 @@ jobs:
           echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV
         fi
 
-        sed -i "s/^channel = \"nightly-.*\"/channel = \"${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
+        sed -i "s/^channel = \"nightly-.*\"/channel = \"nightly-${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update toolchain to ${NEXT_TOOLCHAIN_DATE}" rust-toolchain.toml
-
+        # Update kani-version.toml with the new Kani commit hash
+        sed -i "s/commit = .*/commit = \"${KANI_COMMIT_HASH}\"/" tool_config/kani-version.toml
+        git -c user.name=gitbot -c user.email=git@bot \
+          commit -m "Update Kani version to ${KANI_COMMIT_HASH}" tool_config/kani-version.toml
     - name: Create Pull Request without conflicts
-      if: ${{ env.MERGE_CONFLICTS == 'no' }}
+      if: ${{ env.MERGE_CONFLICTS == 'no' && env.MERGE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
@@ -139,7 +165,7 @@ jobs:
         path: verify-rust-std
 
     - name: Create Pull Request with conflicts
-      if: ${{ env.MERGE_CONFLICTS == 'yes' }}
+      if: ${{ env.MERGE_CONFLICTS == 'yes' && env.MERGE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'