max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: create a mathlib branch for each Lean PR (#2473)

Browse source 
* chore: create a mathlib branch for each Lean PR

* use existing branch if present
This commit is contained in:
Scott Morrison 2023-08-31 13:24:41 +10:00 • committed by GitHub
parent 0901e062eb
commit c4540f75b8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 39 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
.github/workflows/pr-release.yml vendored
View file

@ -69,3 +69,42 @@ jobs:
env:
# The token used here must have `workflow` privileges.
GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
# We next automatically create a Mathlib branch using this toolchain.
# Mathlib CI will be responsible for reporting back success or failure
# to the PR comments asynchronously.
- name: Cleanup workspace
run: |
sudo rm -rf *
# Checkout the mathlib4 repository with all branches
- name: Checkout mathlib4 repository
uses: actions/checkout@v2
with:
repository: leanprover-community/mathlib4
token: ${{ secrets.MATHLIB4_BOT }}
ref: master
fetch-depth: 0
- name: Check if branch exists
id: check_branch
run: |
EXISTS=$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)
echo "Branch exists: $EXISTS"
if [ "$EXISTS" = "0" ]; then
echo "Branch does not exist, creating it."
git checkout -b lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
git add lean-toolchain
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else
echo "Branch already exists, pushing an empty commit."
git checkout lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi
- name: Push changes
run: |
git config user.name "leanprover-community-mathlib4-bot"
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}