Extend workflow to include merge attempt

.github/workflows/update-subtree.yml

@@ -65,11 +65,50 @@ jobs:
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7
       with:
-        commit-message: Update Kani metrics
         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