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
7 changes: 6 additions & 1 deletion .github/workflows/api-map.yml
Original file line number Diff line number Diff line change
Expand Up @@ -79,4 +79,9 @@ jobs:
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
git push mirror "HEAD:refs/heads/${GITHUB_REF_NAME}"
# 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}"
8 changes: 7 additions & 1 deletion .github/workflows/monthly-updates.yml
Original file line number Diff line number Diff line change
Expand Up @@ -156,4 +156,10 @@ jobs:
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
git push mirror "HEAD:refs/heads/${GITHUB_REF_NAME}"
# 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}"
84 changes: 84 additions & 0 deletions .github/workflows/references.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
name: Generate references

on:
schedule:
# Weekly refresh, same cadence as api-map.yml โ€” docs/references.bib and
# the per-file citation comments it tracks change about as rarely as
# API-map.yaml does. Offset five minutes from api-map.yml's run so the
# two don't start in the same minute.
- cron: "25 4 * * 1"
workflow_dispatch: {}

permissions:
contents: write

# Two runs committing to the same branch would race on push.
concurrency:
group: references
cancel-in-progress: false

jobs:
generate:
runs-on: ubuntu-latest
timeout-minutes: 20
env:
HAS_MIRROR_PAT: ${{ secrets.MIRROR_PAT != '' }}
steps:
- name: Checkout
uses: actions/checkout@v4
with:
persist-credentials: true
fetch-depth: 0

- name: Set up Node.js
uses: actions/setup-node@v4
with:
node-version: "20"

# Shared with the api-map and monthly-updates generators, which also
# read this repo.
- name: Cache physlib clone
uses: actions/cache@v4
with:
path: web2/.cache/physlib.git
key: physlib-clone-${{ github.run_id }}
restore-keys: physlib-clone-

- name: Run generator
working-directory: web2
run: node scripts/generate-references.js

- name: Commit & push updated references
id: commit
run: |
git config user.name "github-actions[bot]"
git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
git add web2/data/References.json
if git diff --cached --quiet; then
echo "No reference changes to commit."
echo "committed=false" >> "$GITHUB_OUTPUT"
exit 0
fi
git commit -m "chore(references): auto-generated update"
git pull --rebase --autostash origin "${GITHUB_REF_NAME}"
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}"
6 changes: 3 additions & 3 deletions web2/scripts/generate-monthly-updates.js
Original file line number Diff line number Diff line change
Expand Up @@ -965,7 +965,7 @@ const MISSING_GLYPH_MATH = [
["โŸช", "\\langle\\!\\langle"], ["โŸซ", "\\rangle\\!\\rangle"],
["โŸถ", "\\longrightarrow"], ["โŸน", "\\Longrightarrow"],
["โจ‚", "\\bigotimes"], ["โจ…", "\\bigsqcap"], ["โจฏ", "\\times"],
["โฌ", "\\cdot"],
["โฌ", "\\cdot"], ["โ‹†", "\\star"],
// Flattened parentheses (U+27EE/U+27EF).
["โŸฎ", "\\lgroup"], ["โŸฏ", "\\rgroup"],
// Fraktur letters (U+1D504+ block) - mathlib uses these for ideals and
Expand All @@ -986,8 +986,8 @@ const MISSING_GLYPH_MATH = [
["โ„ฐ", "\\mathcal{E}"],
// Bold Latin capitals and lowercase (U+1D400+ block).
["๐ƒ", "\\mathbf{D}"], ["๐€", "\\mathbf{A}"], ["๐‡", "\\mathbf{H}"],
["๐‹", "\\mathbf{L}"], ["๐”", "\\mathbf{U}"], ["๐ฉ", "\\mathbf{p}"],
["๐ซ", "\\mathbf{r}"], ["๐ฑ", "\\mathbf{x}"],
["๐‹", "\\mathbf{L}"], ["๐", "\\mathbf{N}"], ["๐”", "\\mathbf{U}"], ["๐ฉ", "\\mathbf{p}"],
["๐š", "\\mathbf{a}"], ["๐ซ", "\\mathbf{r}"], ["๐ฑ", "\\mathbf{x}"],
// Double-struck (blackboard bold, U+1D538+ block) - see also ๐•œ โ†’ \Bbbk
// above, which has its own dedicated LaTeX command instead of \mathbb.
["๐•‚", "\\mathbb{K}"], ["๐••", "\\mathbb{d}"],
Expand Down