Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 5 additions & 20 deletions .github/workflows/api-map.yml
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,6 @@ jobs:
generate:
runs-on: ubuntu-latest
timeout-minutes: 20
env:
HAS_MIRROR_PAT: ${{ secrets.MIRROR_PAT != '' }}
steps:
- name: Checkout
uses: actions/checkout@v4
Expand Down Expand Up @@ -67,21 +65,8 @@ jobs:
git push origin "HEAD:${GITHUB_REF_NAME}"
echo "committed=true" >> "$GITHUB_OUTPUT"

# See monthly-updates.yml for why this step exists: pushes made with the
# default GITHUB_TOKEN don't trigger mirror-to-personal.yml, so without
# this the API map would never reach the deployed (Vercel) site.
- name: Mirror to personal repo (Vercel)
if: steps.commit.outputs.committed == 'true' && env.HAS_MIRROR_PAT == 'true'
env:
MIRROR_PAT: ${{ secrets.MIRROR_PAT }}
run: |
git config --unset-all http.https://github.com/.extraheader || true
git config --global credential.helper store
echo "https://x-access-token:${MIRROR_PAT}@github.com" > ~/.git-credentials
git remote add mirror https://github.com/Gabrielebattimelli/Physlib-Website.git
# See monthly-updates.yml: mirror-to-personal.yml rewrites authorship
# and force-pushes this same mirror, so its history is never a
# fast-forward descendant of this repo's commits and a plain push
# here is rejected as non-fast-forward. The mirror is a deploy
# artifact, not shared history, so force is correct here too.
git push --force mirror "HEAD:refs/heads/${GITHUB_REF_NAME}"
# The site deploys via Gabrielebattimelli/Physlib-Website (Vercel).
# mirror-to-personal.yml keeps that mirror in sync, including for the
# commit just pushed above: it also runs on workflow_run for this
# workflow, which (unlike `push`) fires regardless of which token made
# the commit it's mirroring.
19 changes: 18 additions & 1 deletion .github/workflows/mirror-to-personal.yml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,18 @@ on:
push:
branches: ['**']
delete:
# The generator workflows (monthly-updates, api-map, references) commit
# and push with the default GITHUB_TOKEN, which GitHub deliberately does
# not trigger the `push` event above for, to avoid recursion. workflow_run
# isn't subject to that restriction, so this is how their commits reach
# the mirror instead of each of them reimplementing this same mirroring
# (and its authorship rewrite) by hand.
workflow_run:
workflows:
- Generate monthly update
- Generate API map
- Generate references
types: [completed]

# Force-pushes to the mirror must not race each other.
concurrency:
Expand All @@ -14,7 +26,12 @@ jobs:
mirror:
# The mirror receives .github/ too, so without this guard the mirror repo
# runs this workflow against itself and fails on the missing MIRROR_PAT.
if: github.repository == 'kernel-science/physlib-website'
# The conclusion check skips remirroring current main over a generator
# run that failed (or found nothing new to commit) - there's nothing new
# in that case, just the same state this workflow already mirrored.
if: |
github.repository == 'kernel-science/physlib-website' &&
(github.event_name != 'workflow_run' || github.event.workflow_run.conclusion == 'success')
runs-on: ubuntu-latest
steps:
# Vercel's Hobby plan refuses to build any commit whose *author* is not the
Expand Down
39 changes: 5 additions & 34 deletions .github/workflows/monthly-updates.yml
Original file line number Diff line number Diff line change
Expand Up @@ -36,12 +36,6 @@ jobs:
# A month whose clone hangs or whose compile pathologically loops would
# otherwise sit here for the 6-hour default.
timeout-minutes: 60
env:
# The `secrets` context is not available to a step's `if`, so the
# presence of the mirror credential is hoisted here as a plain boolean.
# Deliberately not the secret itself: this keeps it out of every step's
# environment.
HAS_MIRROR_PAT: ${{ secrets.MIRROR_PAT != '' }}
steps:
- name: Checkout
uses: actions/checkout@v4
Expand Down Expand Up @@ -135,31 +129,8 @@ jobs:
git push origin "HEAD:${GITHUB_REF_NAME}"
echo "committed=true" >> "$GITHUB_OUTPUT"

# The site deploys via Gabrielebattimelli/Physlib-Website (Vercel), which
# mirror-to-personal.yml normally keeps in sync on push. That workflow
# will NOT fire for the commit above: GitHub deliberately does not trigger
# workflows for pushes made with the default GITHUB_TOKEN, to avoid
# recursion. Without this step the report lands on main and never reaches
# the live site. So mirror it here, using the same secret and target as
# mirror-to-personal.yml.
#
# Guarded on the secret being present: without it this fails with an
# opaque git credential error, and it fails *after* the report has
# already been committed and pushed to this repo, which reads as "the
# run broke" rather than "the mirror isn't configured".
- name: Mirror to personal repo (Vercel)
if: steps.commit.outputs.committed == 'true' && env.HAS_MIRROR_PAT == 'true'
env:
MIRROR_PAT: ${{ secrets.MIRROR_PAT }}
run: |
git config --unset-all http.https://github.com/.extraheader || true
git config --global credential.helper store
echo "https://x-access-token:${MIRROR_PAT}@github.com" > ~/.git-credentials
git remote add mirror https://github.com/Gabrielebattimelli/Physlib-Website.git
# mirror-to-personal.yml keeps this same mirror in sync by rewriting
# every commit's authorship (filter-branch) and force-pushing the
# result, so the mirror's history is never a fast-forward descendant
# of this repo's real commits - a plain push is rejected as
# non-fast-forward on every run after the first. The mirror is a
# deploy artifact, not shared history, so force is correct here too.
git push --force mirror "HEAD:refs/heads/${GITHUB_REF_NAME}"
# The site deploys via Gabrielebattimelli/Physlib-Website (Vercel).
# mirror-to-personal.yml keeps that mirror in sync, including for the
# commit just pushed above: it also runs on workflow_run for this
# workflow, which (unlike `push`) fires regardless of which token made
# the commit it's mirroring.
25 changes: 5 additions & 20 deletions .github/workflows/references.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,6 @@ jobs:
generate:
runs-on: ubuntu-latest
timeout-minutes: 20
env:
HAS_MIRROR_PAT: ${{ secrets.MIRROR_PAT != '' }}
steps:
- name: Checkout
uses: actions/checkout@v4
Expand Down Expand Up @@ -64,21 +62,8 @@ jobs:
git push origin "HEAD:${GITHUB_REF_NAME}"
echo "committed=true" >> "$GITHUB_OUTPUT"

# See monthly-updates.yml for why this step exists: pushes made with the
# default GITHUB_TOKEN don't trigger mirror-to-personal.yml, so without
# this the references page would never reach the deployed (Vercel) site.
- name: Mirror to personal repo (Vercel)
if: steps.commit.outputs.committed == 'true' && env.HAS_MIRROR_PAT == 'true'
env:
MIRROR_PAT: ${{ secrets.MIRROR_PAT }}
run: |
git config --unset-all http.https://github.com/.extraheader || true
git config --global credential.helper store
echo "https://x-access-token:${MIRROR_PAT}@github.com" > ~/.git-credentials
git remote add mirror https://github.com/Gabrielebattimelli/Physlib-Website.git
# See monthly-updates.yml: mirror-to-personal.yml rewrites authorship
# and force-pushes this same mirror, so its history is never a
# fast-forward descendant of this repo's commits and a plain push
# here is rejected as non-fast-forward. The mirror is a deploy
# artifact, not shared history, so force is correct here too.
git push --force mirror "HEAD:refs/heads/${GITHUB_REF_NAME}"
# The site deploys via Gabrielebattimelli/Physlib-Website (Vercel).
# mirror-to-personal.yml keeps that mirror in sync, including for the
# commit just pushed above: it also runs on workflow_run for this
# workflow, which (unlike `push`) fires regardless of which token made
# the commit it's mirroring.