ci-ubuntu.yml

## Adapted from the agda/agda-stdlib workflow

name: Ubuntu build
on:
  push:
    branches:
      - master
  pull_request:
    branches:
      - master

########################################################################
## CONFIGURATION
##
## See SETTINGS for the most important configuration variable: AGDA_BRANCH.
## It has to be defined as a build step because it is potentially branch
## dependent.
##
## As for the rest:
##
## Basically do not touch GHC_VERSION and CABAL_VERSION as long as
## they aren't a problem in the build. If you have time to waste, it
## could be worth investigating whether newer versions of ghc produce
## more efficient Agda executable and could cut down the build time.
## Just be aware that actions are flaky and small variations are to be
## expected.
##
## The CABAL_INSTALL variable only passes `-O1` optimisations to ghc
## because github actions cannot currently handle a build using `-O2`.
## To be experimented with again in the future to see if things have
## gotten better.
##
########################################################################

########################################################################
## SETTINGS
##
## AGDA_BRANCH picks the branch of Agda to use to build the library.
## It doesn't really track the branch, so you have to drop caches to
## get a new branch version if it changes. This will be fixed in the
## next PR.
########################################################################

env:
  AGDA_BRANCH: v2.6.4.1
  GHC_VERSION: 9.4.7
  CABAL_VERSION: 3.6.2.0
  CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
  CACHE_PATHS: |
    ~/.cabal/packages
    ~/.cabal/store
    ~/.cabal/bin

jobs:
  test-cubical:
    runs-on: ubuntu-latest
    steps:
      - name: Install cabal
        uses: haskell-actions/setup@v2
        with:
          ghc-version: ${{ env.GHC_VERSION }}
          cabal-version: ${{ env.CABAL_VERSION }}
          cabal-update: true

      # This caching step allows us to save a lot of building time by only
      # rebuilding Agda, and re-checking unchanged library files if
      # absolutely necessary i.e. if we change either the version of Agda,
      # ghc, or cabal that we want to use for the build.
      - name: Restore external dependencies cache
        uses: actions/cache/restore@v3
        id: cache-external-restore
        with:
          path: ${{ env.CACHE_PATHS }}
          key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}

      ########################################################################
      ## INSTALLATION STEPS
      ########################################################################

      - name: Download and install Agda from github
        if: steps.cache-external-restore.outputs.cache-hit != 'true'
        run: |
          git clone https://github.com/agda/agda --branch ${{ env.AGDA_BRANCH }} --depth=1
          cd agda
          mkdir -p doc
          touch doc/user-manual.pdf
          ${{ env.CABAL_INSTALL }}
          cd ..
          rm -rf agda

      - name: Download and install fix-whitespace
        if: steps.cache-external-restore.outputs.cache-hit != 'true'
        run: |
          git clone https://github.com/agda/fix-whitespace --depth=1
          cd fix-whitespace
          ${{ env.CABAL_INSTALL }} fix-whitespace.cabal
          cd ..

      - name: Save external dependencies cache
        if: steps.cache-external-restore.outputs.cache-hit != 'true'
        uses: actions/cache/save@v3
        id: cache-external-save
        with:
          path: ${{ env.CACHE_PATHS }}
          key: ${{ steps.cache-external-restore.outputs.cache-primary-key }}

      ########################################################################
      ## CHECKOUT
      ########################################################################

      # By default github actions do not pull the repo
      - name: Checkout cubical
        uses: actions/checkout@v3

      ########################################################################
      ## TESTING
      ########################################################################

      - name: Restore library cache
        uses: actions/cache/restore@v3
        id: cache-library-restore
        with:
          path: ./_build
          key: library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-${{ hashFiles('Cubical/**', 'cubical.agda-lib', 'Everythings.hs') }}
          restore-keys: |
            library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-

      - name: Put cabal programs in PATH
        run: echo "~/.cabal/bin" >> "${GITHUB_PATH}"

      - name: Test cubical
        run: |
          make test \
            AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \
            FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \
            EVERYTHINGS='cabal run Everythings'

      - name: Save library cache
        if: steps.cache-library-restore.outputs.cache-hit != 'true'
        uses: actions/cache/save@v3
        id: cache-library-save
        with:
          path: ./_build
          key: ${{ steps.cache-library-restore.outputs.cache-primary-key }}

      ########################################################################
      ## HTML GENERATION
      ########################################################################

      - name: Htmlize cubical
        if: github.event_name == 'push' && github.ref_name == 'master'
        run: |
          make listings \
            AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \
            FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \
            EVERYTHINGS='cabal run Everythings'

      - name: Deploy to GitHub Pages
        if: github.event_name == 'push' && github.ref_name == 'master'
        uses: JamesIves/github-pages-deploy-action@4.1.8
        with:
          branch: gh-pages
          folder: html