ci-ubuntu.yml

## Adapted from the agda/agda-stdlib workflow

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

########################################################################
## 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
  CUBICAL_BRANCH: v0.7
  GHC_VERSION: 9.2.5
  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:
    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: 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
        uses: actions/checkout@v4
        with:
          path: symmetries

      - name: Checkout cubical
        uses: actions/checkout@v4
        with:
          repository: agda/cubical
          path: cubical
          ref: ${{ env.CUBICAL_BRANCH }}

      - name: Register cubical
        run: |
          mkdir ~/.agda
          echo "$GITHUB_WORKSPACE/cubical/cubical.agda-lib" >> ~/.agda/libraries

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

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

      - name: Generate Everything.agda
        run: |
          cd symmetries
          chmod +x create-everything.sh
          ./create-everything.sh

      - name: Test
        run: |
          cd symmetries
          agda Everything.agda