From dc98e2d6610cca3124430ac67749ad33d651beb1 Mon Sep 17 00:00:00 2001
From: Olivier Cots <olivier.cots@irit.fr>
Date: Thu, 15 Oct 2026 16:41:48 +0200
Subject: [PATCH] ci(docs): previews on request ('documentation push preview'),
 cleaned up on close

- 'run documentation' is the only trigger; 'documentation push preview'
  also deploys the PR preview (DOCUMENTER_PUSH_PREVIEW read in make.jl).
- DocPreviewCleanup.yml removes previews of closed PRs from gh-pages
  (control-toolbox/CTActions#94).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .github/workflows/DocPreviewCleanup.yml | 20 +++++++++++++++++++
 .github/workflows/Documentation.yml     | 26 ++++++++++++++-----------
 docs/make.jl                            |  6 +++++-
 3 files changed, 40 insertions(+), 12 deletions(-)
 create mode 100644 .github/workflows/DocPreviewCleanup.yml

diff --git a/.github/workflows/DocPreviewCleanup.yml b/.github/workflows/DocPreviewCleanup.yml
new file mode 100644
index 000000000..45fa38571
--- /dev/null
+++ b/.github/workflows/DocPreviewCleanup.yml
@@ -0,0 +1,20 @@
+name: Documentation preview cleanup
+
+# Removes from gh-pages the documentation previews of closed pull requests
+# (CTActions documentation-preview-cleanup.yml, see its docs/WORKFLOWS.md §3.1).
+
+on:
+  pull_request:
+    types: [closed]
+  workflow_dispatch:
+
+jobs:
+  call:
+    # A PR from a fork gets a read-only token, and its build never deployed a preview.
+    if: >
+      github.event_name == 'workflow_dispatch' ||
+      github.event.pull_request.head.repo.full_name == github.repository
+    permissions:
+      contents: write
+      pull-requests: read
+    uses: control-toolbox/CTActions/.github/workflows/documentation-preview-cleanup.yml@main
diff --git a/.github/workflows/Documentation.yml b/.github/workflows/Documentation.yml
index 1c2a284c1..84bde499b 100644
--- a/.github/workflows/Documentation.yml
+++ b/.github/workflows/Documentation.yml
@@ -13,24 +13,28 @@ on:
 # can take up to `gpu_timeout_minutes`. Without this, two pushes to `main` in quick
 # succession could leave an older run's GPU pass finishing — and redeploying — after a
 # newer run's CPU build has already published, showing older content over newer.
-# `cancel-in-progress` cancels the whole older run, its queued/running GPU job
-# included. Tags carry distinct refs (the tag name, not `main`), so a release build is
-# never cancelled by an unrelated push to `main`, and vice versa.
+# Push and tag runs queue (GitHub keeps only the newest pending one), so the GPU pass
+# on the self-hosted runner is never killed and the newest content deploys last; PR runs
+# are GitHub-hosted only and are cancelled. Tags carry distinct refs (the tag name, not
+# `main`), so a release build never waits for an unrelated push to `main`.
 concurrency:
   group: documentation-${{ github.ref }}
-  cancel-in-progress: true
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
 
 jobs:
   call:
-    # A 'labeled' event fires once per label added, and re-evaluates against the PR's
-    # *current* full label set — so adding several labels in a row would otherwise
-    # re-run this job on every subsequent label add. Only react to 'labeled' when it's
-    # this specific label; for other trigger types (opened/synchronize/reopened), fall
-    # back to checking the current label set as before.
+    # On a PR, `run documentation` is the only trigger. `documentation push preview` is a
+    # modifier: with `run documentation` present, the build also deploys its preview
+    # (CTActions sets DOCUMENTER_PUSH_PREVIEW from it); on its own it does nothing. Adding
+    # it to a PR that already has `run documentation` re-runs the build with the preview.
+    # A 'labeled' event fires once per label added, so it reacts only to these two labels;
+    # synchronize/reopened check the current label set.
     if: >
       github.event_name != 'pull_request' ||
-      (github.event.action == 'labeled' && github.event.label.name == 'run documentation') ||
-      (github.event.action != 'labeled' && contains(github.event.pull_request.labels.*.name, 'run documentation'))
+      (contains(github.event.pull_request.labels.*.name, 'run documentation') &&
+        (github.event.action != 'labeled' ||
+         github.event.label.name == 'run documentation' ||
+         github.event.label.name == 'documentation push preview'))
     uses: control-toolbox/CTActions/.github/workflows/documentation.yml@main
     with:
       use_ct_registry: true
diff --git a/docs/make.jl b/docs/make.jl
index 2a669e8cc..11dd2b7c7 100644
--- a/docs/make.jl
+++ b/docs/make.jl
@@ -358,8 +358,12 @@ end
 # ═══════════════════════════════════════════════════════════════════════════════
 bases_file = joinpath(@__DIR__, "build", "bases.txt")
 if isfile(bases_file)
+    # PR previews are opt-in: CTActions sets DOCUMENTER_PUSH_PREVIEW to "true" only on a
+    # PR carrying the `documentation push preview` label.
     DocumenterVitepress.deploydocs(;
-        repo=repo_url * ".git", devbranch="main", push_preview=true
+        repo=repo_url * ".git",
+        devbranch="main",
+        push_preview=get(ENV, "DOCUMENTER_PUSH_PREVIEW", "false") == "true",
     )
 else
     @info "Skipping deployment: no bases were built (prerelease with existing higher stable release)."