-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(ci): avoid push to Azure if branch has been updated #2048
Conversation
+1 from me |
I have no idea why this is failing? The new test works when it's performed before the build stage, but not after. See the difference between the last two commits. |
@robertylewis Do you remember the magic number of 60 minutes? I think you need to use the credentials for @leanprover-community-bot. |
I think I blocked it out of my memory... |
GitHub is struggling right now but I think the fixes made it here. |
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.
…community#2048) * avoid push to Azure if branch has been updated * changes to git config in deploy_nightly.sh break git fetch * I don't understand why this is different than on my own repo * artifact upload breaks fetch, I guess? * factor out git config * fix env variable * adjustments * removed repo check Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
PR leanprover-community#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 leanprover-community#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. leanprover-community#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 leanprover-community#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.
…community#2048) * avoid push to Azure if branch has been updated * changes to git config in deploy_nightly.sh break git fetch * I don't understand why this is different than on my own repo * artifact upload breaks fetch, I guess? * factor out git config * fix env variable * adjustments * removed repo check Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
PR leanprover-community#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 leanprover-community#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. leanprover-community#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 leanprover-community#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.
PR leanprover-community#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 leanprover-community#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. leanprover-community#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 leanprover-community#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.
On non-master builds, it seems unnecessary to push an olean archive if another commit is added to the branch before the build finishes.
A common situation in an open PR is to add a sequence of commits very quickly, e.g. accepting review suggestions. It seems very unlikely anyone would check out one of the commits in the middle.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list