Skip to content

Update workflow security and consistency #256

Update workflow security and consistency

Update workflow security and consistency #256

Workflow file for this run

name: build-docs
on:
push:
branches:
- main
pull_request:
branches:
- main
types:
- opened
- reopened
- synchronize
- labeled # requires the `build-docs` label
- ready_for_review
workflow_dispatch: # manual trigger
env:
CACHE_NUMBER: 0 # increase to reset cache manually
DEPLOY_BRANCH: gh-pages # deployed docs branch
HDF5_USE_FILE_LOCKING: "FALSE" # disable file locking
concurrency:
group: ${{ github.workflow }}-${{ github.head_ref || github.ref }}
cancel-in-progress: true
defaults:
run:
shell: bash -le {0}
jobs:
check-for-changes:
runs-on: ubuntu-latest
if: ${{ !github.event.pull_request.draft }}
outputs:
trigger-check-outcome: ${{ steps.trigger_check.outcome }}
docs-check-outcome: ${{ steps.docs_check.outcome }}
steps:
- uses: actions/checkout@v4
if: github.event_name != 'pull_request'
- name: Checkout pull/${{ github.event.number }}
uses: actions/checkout@v4
with:
fetch-depth: 0
ref: ${{ github.event.pull_request.head.sha }}
if: github.event_name == 'pull_request'
- name: Check for trigger by push event, manual dispatch, build-docs label on a PR
id: trigger_check
if: github.event_name == 'push' || github.event_name == 'workflow_dispatch' || github.event_name == 'pull_request' && contains(github.event.pull_request.labels.*.name, 'build-docs')
run: |
echo "Building docs as a test."
exit 0
continue-on-error: true
- name: Check for changes in documentation
run: |
if git diff origin/main..."$(git rev-parse --abbrev-ref HEAD)" --name-only | cat | grep '^docs/' | grep -q .; then
num_files=$(git diff --name-only origin/main...HEAD | grep '^docs/' | wc -l)
echo "Changes found in documentation files: $num_files"
exit 0
else
echo "No changes found in documentation files - will stop running the pipeline."
exit 1
fi
id: docs_check
if: steps.trigger_check.outcome != 'success'
continue-on-error: true
build-sphinx-html:
if: (github.repository == 'tardis-sn/stardis' && (github.head_ref || github.ref_name) == 'main') || github.repository_owner != 'tardis-sn'
# The above line makes this action run if it is either not on the upstream/main or the main branch of upstream/main.
# If there is a better way to implement this, I'd like someone to please share.
# The context to get the branch name is from https://stackoverflow.com/a/71158878
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
if: github.event_name != 'pull_request'
- name: Checkout pull/${{ github.event.number }}
uses: actions/checkout@v4
with:
fetch-depth: 0
ref: ${{ github.event.pull_request.head.sha }}
if: github.event_name == 'pull_request'
- name: Setup environment
uses: ./.github/actions/setup_env
with:
os-label: linux-64
- name: Install TARDIS
id: install-tardis
# shell: bash -l {0}
run: |
pip install git+https://github.com/tardis-sn/tardis.git@release-2024.08.25
- name: Install STARDIS
id: install-stardis
# shell: bash -l {0}
run: |
pip install -e .[docs]
- name: Make Sphinx HTML
id: make-sphinx-html
run: |
make -C docs html
- name: Upload documentation artifact
if: github.event_name == 'pull_request'
uses: actions/upload-artifact@v4
with:
name: docs-build-${{ github.event.pull_request.head.sha }}
path: docs/_build/html
- name: Set destination directory
if: github.event_name != 'pull_request'
run: |
BRANCH=$(echo ${GITHUB_REF#refs/heads/})
if [[ $EVENT == push ]] || [[ $EVENT == workflow_dispatch ]]; then
if [[ $BRANCH == $DEFAULT ]]; then
echo "DEST_DIR=" >> $GITHUB_ENV
else
echo "DEST_DIR=branch/$BRANCH" >> $GITHUB_ENV
fi
else
echo "Unexpected event trigger $EVENT"
exit 1
fi
cat $GITHUB_ENV
env:
DEFAULT: ${{ github.event.repository.default_branch }}
EVENT: ${{ github.event_name }}
PR: ${{ github.event.number }}
- name: Set clean branch option
if: github.event_name != 'pull_request'
run: |
if [[ $EVENT == workflow_dispatch ]]; then
echo "CLEAN_BRANCH=true" >> $GITHUB_ENV
else
echo "CLEAN_BRANCH=false" >> $GITHUB_ENV
fi
cat $GITHUB_ENV
env:
EVENT: ${{ github.event_name }}
- name: Deploy ${{ env.DEST_DIR }}
if: github.event_name != 'pull_request'
uses: peaceiris/actions-gh-pages@v4
with:
github_token: ${{ secrets.BOT_TOKEN }}
publish_branch: ${{ env.DEPLOY_BRANCH }}
publish_dir: ./docs/_build/html
destination_dir: ${{ env.DEST_DIR }}
keep_files: true
force_orphan: ${{ env.CLEAN_BRANCH }}
user_name: "TARDIS Bot"
user_email: "tardis.sn.bot@gmail.com"