File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 1414 - name : checkout
1515 uses : actions/checkout@v6
1616 with :
17+ ref : nightly-testing
1718 fetch-depth : 0
1819
1920 - name : install jq
2223 - name : get toolchain tags
2324 id : toolchain-tag
2425 run : |
25- REPO_TAG=$(sed 's/.*://1' lean-toolchain | tr -d '\n')
26+ REPO_TAG=$(git show main:lean-toolchain | cut -d':' -f2 | tr -d '\n')
2627 LEAN_TAG=$(curl -s "https://api.github.com/repos/leanprover/lean4/releases" | jq -r '.[0].tag_name' | tr -d '\n')
2728 echo "repo_tag=$REPO_TAG" >> $GITHUB_OUTPUT
2829 echo "lean_tag=$LEAN_TAG" >> $GITHUB_OUTPUT
3233 if : ${{ steps.toolchain-tag.outputs.lean_tag != steps.toolchain-tag.outputs.repo_tag }}
3334 run : |
3435 git config user.name "${{ github.actor }}"
35- git config user.email "${{ github.actor_id}}+${{ github.actor }}@users.noreply.github.com"
36- git merge -X theirs origin/nightly-testing
36+ git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
3737 echo "leanprover/lean4:${{ steps.toolchain-tag.outputs.lean_tag }}" > lean-toolchain
3838
3939 - name : create pull request
4242 token : ${{ secrets.UNICODE_BASIC_TOKEN }}
4343 commit-message : " chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"
4444 branch : update-toolchain-${{ steps.toolchain-tag.outputs.lean_tag }}
45+ base : main
4546 delete-branch : true
4647 title : " chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"
You can’t perform that action at this time.
0 commit comments