Repository navigation
Let a newer Deploy Docs run cancel the one in progress #3633
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -26,7 +26,12 @@ on: | |
|
|
||
| concurrency: | ||
| group: deploy-docs | ||
| cancel-in-progress: false | ||
| # Newest run wins. build-docs.sh builds the tips of main and v1.x, not the | ||
| # triggering commit, so a newer run publishes everything an older one would, | ||
| # and Pages takes the site as one artifact, so a cancelled run leaves the live | ||
| # site as it was. With `false`, a run that never gets a runner holds the group | ||
| # and every later deploy waits behind it. | ||
| cancel-in-progress: true | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 🟡 (optional) Docs readers get a site that stays stale through every merge burst, where the base branch published after each run. .github/workflows/deploy-docs.yml:34 cancels the running deploy on every push to main matching the paths filter, which includes src/mcp/**. The build runs scripts/build-docs.sh: two branch builds plus 12 language sites, so a run lasts longer than the gap between merges in this repo (git log shows merges at 13:45, 13:50, 13:51 and 14:17, 14:24, 14:32 on 2026-10-02). Fix: keep cancel-in-progress: false and bound the stuck-queue case another way (a job-level timeout-minutes, or cancel only runs still queued), so a deploy that has started always finishes. Why this was flaggedgit log on this checkout shows 17 merges on 2026-10-02, with clusters three merges in six minutes (13:45:32, 13:50:29, 13:51:05) and three in fifteen minutes (14:17, 14:24, 14:32); nearly all touch src/mcp/** or docs/, which are in the push paths filter at .github/workflows/deploy-docs.yml:9-24. Each run executes scripts/build-docs.sh, which fetches and builds main via scripts/docs/build.sh (uv sync, zensical strict build, then one zensical build per language for 12 languages per i18n/languages.yml) and then v1.x via a second uv sync and mkdocs build. That is well over the five-minute merge gaps observed. With .github/workflows/deploy-docs.yml:34 set to true, every merge in such a cluster cancels the run in progress, so no deployment completes until the cluster ends; on the base branch each queued run waited and the site advanced after every build. Every reader of the published docs sees content lagging by the length of the burst, and each cancelled run burns a full runner build. Remedy: leave the in-progress run alone and address the stuck-queued-runner incident with a job timeout or by cancelling only queued runs. Verification: |
||
|
|
||
| jobs: | ||
| deploy-docs: | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P2: This cancels runs even after
Deploy to GitHub Pageshas started, but cancellation does not roll back a deployment request already submitted bydeploy-pages; an older artifact can therefore become live after a newer run starts. Separate the cancelable build from deployment and serialize the deployment phase, or otherwise prevent cancellation once publication begins.Prompt for AI agents