Skip to content

Serialize documentation deployment writes to gh-pages #4761

Description

@ChrisRackauckas-Claude

Failure

The current master documentation workflow failed after completing the documentation build because Documenter could not push its generated commit to gh-pages:

The job built and committed the generated documentation successfully (build based on 97aec8f) before the push was rejected. The gh-pages branch had been updated at 09:41:31 UTC by commit 431543a while this roughly two-hour workflow was running.

Cause

.github/workflows/Documentation.yml currently groups concurrency by workflow and source ref:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}

PR previews, master, and tag builds therefore run concurrently even though all eventually write to the same gh-pages branch. Documenter can then try to push a commit based on an older gh-pages state.

This is an external-state race and is not meaningfully reproducible as a single clean local build; the CI log demonstrates the two required concurrent branch states.

Suggested direction

Serialize only the deployment write to gh-pages, while allowing the expensive documentation builds to remain parallel. A global workflow-level concurrency group would avoid the race but would also serialize the full builds, so splitting build and deploy (with a shared deployment concurrency group) appears safer.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions