Skip to content

Merge branch 'main' into prepare_release #29

Merge branch 'main' into prepare_release

Merge branch 'main' into prepare_release #29

Workflow file for this run

# Workflow for building and deploying versioned MkDocs site to GitHub Pages
name: Deploy Documentation to GitHub Pages
on:
push:
branches:
- "main"
- "develop"
- "prepare_release" # For testing release infrastructure
workflow_dispatch:
permissions:
contents: write
pages: write
id-token: write
concurrency:
group: "pages"
cancel-in-progress: false
jobs:
deploy:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
with:
fetch-depth: 0 # Fetch all history for mike to work properly
- name: Set up Python
uses: actions/setup-python@v5
with:
python-version: "3.12"
- name: Configure Git
run: |
git config --global user.name "github-actions[bot]"
git config --global user.email "github-actions[bot]@users.noreply.github.com"
- name: Install MkDocs and dependencies
run: |
python -m pip install --upgrade pip
pip install mkdocs
pip install mkdocs_gen_files
pip install "mkdocstrings[python]"
pip install mkdocs-awesome-nav
pip install mkdocs-material
pip install mkdocs-include-dir-to-nav
pip install python-markdown-math
pip install mike>=2.0.0
- name: Get current version
id: get_version
run: |
# Extract version from workflow/__init__.py
VERSION=$(python -c "exec(open('workflow/__init__.py').read()); print(__version__)")
echo "VERSION=${VERSION}" >> $GITHUB_OUTPUT
echo "Deploying documentation for version: ${VERSION}"
- name: Determine deployment alias
id: deployment
run: |
if [ "${{ github.ref }}" = "refs/heads/main" ]; then
echo "ALIAS=dev" >> $GITHUB_OUTPUT
echo "TITLE=Development (main)" >> $GITHUB_OUTPUT
echo "SET_DEFAULT=true" >> $GITHUB_OUTPUT
elif [ "${{ github.ref }}" = "refs/heads/develop" ]; then
echo "ALIAS=develop" >> $GITHUB_OUTPUT
echo "TITLE=Development (develop)" >> $GITHUB_OUTPUT
echo "SET_DEFAULT=false" >> $GITHUB_OUTPUT
elif [ "${{ github.ref }}" = "refs/heads/prepare_release" ]; then
echo "ALIAS=test-release" >> $GITHUB_OUTPUT
echo "TITLE=Test Release" >> $GITHUB_OUTPUT
echo "SET_DEFAULT=false" >> $GITHUB_OUTPUT
else
echo "ALIAS=preview" >> $GITHUB_OUTPUT
echo "TITLE=Preview" >> $GITHUB_OUTPUT
echo "SET_DEFAULT=false" >> $GITHUB_OUTPUT
fi
- name: Deploy development docs with mike
run: |
VERSION="${{ steps.get_version.outputs.VERSION }}"
ALIAS="${{ steps.deployment.outputs.ALIAS }}"
TITLE="${{ steps.deployment.outputs.TITLE }}"
# Deploy current version with appropriate alias
if [ "${{ steps.deployment.outputs.SET_DEFAULT }}" = "true" ]; then
# For main branch: deploy as both alias and latest, then set latest as default
mike deploy --push --update-aliases "$ALIAS" latest "$TITLE"
mike set-default --push latest
else
# For other branches: just deploy with the alias
mike deploy --push --update-aliases "$ALIAS" "$TITLE"
fi