ci.yaml

name: agda-unimath CI
on:
  # To run this workflow manually
  workflow_dispatch:
    inputs:
      ref:
        description: the repository ref to build
        required: true
        default: master

  push:
    branches:
      - master
  pull_request:
    branches:
      - master
    types:
      - opened
      - reopened
      - synchronize
      - ready_for_review

# Cancel previous runs of the same branch
concurrency:
  group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}'
  cancel-in-progress: true

jobs:
  typecheck:
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        os: [macOS-13, ubuntu-latest]
        agda: ['2.6.4']
    steps:
      - name: Checkout our repository
        uses: actions/checkout@v3
        with:
          path: master
      - name: Setup Agda
        uses: wenkokke/setup-agda@v2.1.0
        with:
          agda-version: ${{ matrix.agda }}

      - uses: actions/cache/restore@v3
        id: cache-agda-formalization
        name: Restore Agda formalization cache
        with:
          path: master/_build
          key:
            ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-${{
            hashFiles('master/src/**') }}
          restore-keys: |
            ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-
            ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}-

      - name: Typecheck library
        run: |
          cd master
          make check

      - name: Save Agda build cache
        uses: actions/cache/save@v3
        with:
          path: master/_build
          key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'

      # Install Python and friends for website generation only where needed
      - uses: actions/setup-python@v4
        if: ${{ matrix.os == 'ubuntu-latest' }}
        with:
          python-version: '3.8'
          check-latest: true
          cache: 'pip'

      - run: python3 -m pip install -r master/scripts/requirements.txt
        if: ${{ matrix.os == 'ubuntu-latest' }}

      # We need to run the sources through Agda not only to get the highlighting
      # (which is irrelevant for checking links), but because it flattens the
      # directory structure to a format which is expected in the links we write.
      # We don't need to produce this artifact for more than one configuration.
      - name: Produce syntax highlighted markdown
        if: ${{ matrix.os == 'ubuntu-latest' }}
        run: |
          cd master
          make website-prepare

      # The lifetime of this cache is for one CI run only, so it's indexed by
      # the run ID. According to the docs, caches are immutable, so we can't
      # keep the same key for a branch and update it on pushes.
      - name: Save pre-website cache
        if: ${{ matrix.os == 'ubuntu-latest' }}
        uses: actions/cache/save@v3
        with:
          key: pre-website-${{ github.run_id }}
          path: master/docs

  # We're only running the linkcheck renderer, so we don't need to install
  # any other packages; that gives a warning during building, but doesn't
  # fail the build.
  link-check:
    needs: typecheck
    permissions:
      actions: write
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3
        with:
          path: master

      - uses: peaceiris/actions-mdbook@v1
        with:
          mdbook-version: '0.4.34'

      - uses: baptiste0928/cargo-install@v2
        with:
          crate: mdbook-linkcheck
          version: '0.7.7'

      # Install Python and friends for website generation only where needed
      - uses: actions/setup-python@v4
        with:
          python-version: '3.8'
          check-latest: true
          cache: 'pip'

      - run: python3 -m pip install -r master/scripts/requirements.txt

      - uses: actions/cache/restore@v3
        with:
          key: pre-website-${{ github.run_id }}
          path: master/docs

      # Tell mdbook to use only the linkcheck backend
      - name: Check website links and bibtex references
        env:
          MDBOOK_OUTPUT: '{"linkcheck":{}}'
        run: |
          cd master
          mdbook build

      - name: Delete website cache
        if: ${{ always() }}
        env:
          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        # Note that the cleanup currently fails, because we don't give the
        # `actions:write` permission to actions; hence the `set +e` to ignore
        # the error
        run: |
          gh extension install actions/gh-actions-cache
          REPO=${{ github.repository }}
          BRANCH="refs/pull/${{ github.event.pull_request.number }}/merge"

          set +e
          gh actions-cache delete pre-website-${{ github.run_id }} -R $REPO -B $BRANCH --confirm

          # The previous command failing would report an error even with `set -e`
          exit 0

  pre-commit:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3

      - uses: actions/setup-python@v4
        with:
          python-version: '3.8'
          check-latest: true
          cache: 'pip'

      - run: python3 -m pip install -r scripts/requirements.txt

      - uses: pre-commit/action@v3.0.0