chore: merge main into nightly-testing

Author: fgdorais

.github/workflows/push-to-nightly.yml

@@ -18,14 +18,11 @@ jobs:
           fetch-depth: 0
           token: ${{ secrets.UNICODE_BASIC_TOKEN }}
 
-      - name: set user
+      - name: merge main
         run: |
           git config user.name "${{ github.actor }}"
           git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
-
-      - name: merge main
-        run: |
           git merge origin/main --no-commit --strategy-option ours --allow-unrelated-histories
           git restore --staged lean-toolchain lake-manifest.json
-          git commit -m "chore: merge main into nightly-testing"
+          git commit --allow-empty -m "chore: merge main into nightly-testing"
           git push origin nightly-testing

.github/workflows/update-nightly-toolchain.yml

@@ -24,15 +24,18 @@ jobs:
           git config user.name "${{ github.actor }}"
           git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
 
-      - name: update lean-toolchain
+      - name: get toochain tags
         id: toolchain-tag
         run: |
           LEAN_TAG=$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')
+          REPO_TAG=$(cut -d ':' -f2 lean-toolchain | tr -d '\n')
           echo "lean_tag=$LEAN_TAG" >> $GITHUB_OUTPUT
-          echo "leanprover/lean4:$LEAN_TAG" > lean-toolchain
-          git add lean-toolchain
+          echo "repo_tag=$REPO_TAG" >> $GITHUB_OUTPUT
 
       - name: commit and push
+        if: ${{ steps.toolchain-tag.outputs.lean_tag != steps.toolchain-tag.outputs.repo_tag }}
         run: |
+          echo "leanprover/lean4:${{ steps.toolchain-tag.outputs.lean_tag }}" > lean-toolchain
+          git add lean-toolchain
           git commit -m "chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"
           git push origin nightly-testing

.github/workflows/update-toolchain.yml

@@ -37,6 +37,7 @@ jobs:
           echo "leanprover/lean4:${{ steps.toolchain-tag.outputs.lean_tag }}" > lean-toolchain
 
       - name: create pull request
+        if: ${{ steps.toolchain-tag.outputs.lean_tag != steps.toolchain-tag.outputs.repo_tag }}
         uses: peter-evans/create-pull-request@v8
         with:
           token: ${{ secrets.UNICODE_BASIC_TOKEN }}