Skip to content

Commit

Permalink
chore(ci): always push release to azure (#2321)
Browse files Browse the repository at this point in the history
PR #2048 changed the CI so that olean caches are not pushed to Azure if a later commit on the same branch occurs. The reasoning was that it was unlikely that anyone would fetch those caches. That's changed as of #2278, since `fetch_olean_cache.sh` now looks for caches from commits earlier in the history. This means that currently, we can observe the following wasteful sequence of events in several PRs (e.g. #2258):

1. commit A gets pushed to a certain branch and CI_A starts.
2. While CI_A is still running the `leanpkg build` step, commit B is pushed and CI_B starts.
3. CI_A finishes `leanpkg build` but doesn't upload its cache to Azure because of #2048 
4. Now commit C is pushed and can't use the results of CI_A
5. CI_B finishes `leanpkg build` but doesn't upload its cache
6. Commit D is pushed and can't use the results of CI_A or CI_B ...

(This can keep happening as long as the next commit arrives before the most recent CI uploads to Azure).

I also cleaned up some stuff that was left over from when we ran the build on both "pr" and "push" events.
  • Loading branch information
bryangingechen committed Apr 4, 2020
1 parent 63aa8b1 commit 8406896
Showing 1 changed file with 7 additions and 14 deletions.
21 changes: 7 additions & 14 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -66,22 +66,15 @@ jobs:
git config --unset http.https://github.com/.extraheader
- name: push release to azure
if: always() && github.repository == 'leanprover-community/mathlib' && github.event_name == 'push'
if: always() && github.repository == 'leanprover-community/mathlib'
run: |
branch=${GITHUB_REF#refs/heads/}
git fetch --depth=1 origin-bot $branch
remote_sha="$(git rev-parse origin-bot/$branch)"
if [ "${{ github.sha }}" == "$remote_sha" -o "${{ github.ref }}" == "refs/heads/master" ]; then
archive_name="$(git rev-parse HEAD).tar.gz"
tar czf "$archive_name" src
azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
python scripts/write_azure_table_entry.py "$lean_file_hash" "${{ github.sha }}" "${{ secrets.AZURE_TABLE_WRITE_TOKEN }}"
else
echo "archive is obsolete: branch has been updated"
fi
archive_name="$(git rev-parse HEAD).tar.gz"
tar czf "$archive_name" src
azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
python scripts/write_azure_table_entry.py "$lean_file_hash" "${{ github.sha }}" "${{ secrets.AZURE_TABLE_WRITE_TOKEN }}"
- name: push release to mathlib-nightly
if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master'
if: github.repository == 'leanprover-community/mathlib' && github.ref == 'refs/heads/master'
run: ./scripts/deploy_nightly.sh
env:
DEPLOY_NIGHTLY_GITHUB_TOKEN: ${{ secrets.DEPLOY_NIGHTLY_GITHUB_TOKEN }}
Expand All @@ -107,7 +100,7 @@ jobs:
git diff
- name: update nolints.txt
if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master'
if: github.repository == 'leanprover-community/mathlib' && github.ref == 'refs/heads/master'
run:
./scripts/update_nolints.sh
env:
Expand Down

0 comments on commit 8406896

Please sign in to comment.