ci-ubuntu.yml

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

########################################################################
## CONFIGURATION
##
## Key variables:
##
## AGDA_COMMIT picks the version of Agda to use to build the library.
## It can either be a hash of a specific commit (to target a bugfix for
## instance) or a tag e.g. tags/v2.6.1.3 (to target a released version).
##
## STDLIB_VERSION picks the version of the stdlib to pull. The current
## design requires that the number corresponds to a released version
## but we could change that to a commit-based approach if you need to.
##
## 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.
##
## The AGDA variable specifies the command to use to build the library.
## It currently passes the flag `-Werror` to ensure maximal compliance
## with e.g. not relying on deprecated definitions.
## The rest are some arbitrary runtime arguments that shape the way Agda
## allocates and garbage collects memory. It should make things faster.
## Limits can be bumped if the builds start erroring with out of memory
## errors.
##
########################################################################

env:
  AGDA_COMMIT: tags/v2.6.4
  STDLIB_VERSION: "2.0"

  GHC_VERSION: 8.10.7
  CABAL_VERSION: 3.6.2.0
  CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' --installdir $HOME/.cabal/bin
  AGDA: agda --auto-inline -Werror +RTS -M6G -H3.5G -A128M -RTS -i . -i src/

jobs:
  test-categories:
    runs-on: ubuntu-latest
    steps:

      # By default github actions do not pull the repo
      - name: Checkout agda-categories
        uses: actions/checkout@v4

########################################################################
## SETTINGS
########################################################################

      - name: Initialise variables
        run: |
          # Only deploy if the build follows from pushing to master
          if [[ '${{ github.ref }}' == 'refs/heads/master' ]]; then
             echo "AGDA_DEPLOY=true" >> $GITHUB_ENV
          fi

      # The script won't be able to find Agda if we don't tell it to look at the
      # content of ~/.cabal/bin
      - name: Put cabal programs in PATH
        run: echo "$HOME/.cabal/bin" >> $GITHUB_PATH

########################################################################
## CACHING
########################################################################

      # This caching step allows us to save a lot of building time by only
      # downloading ghc and cabal and rebuilding Agda 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: Open cache
        uses: actions/cache@v4
        id: cache-everything
        with:
          path: |
            ~/.cabal/packages
            ~/.cabal/store
            ~/.cabal/bin
            ~/.cabal/share
            ~/.agda-build-cache
          key: agda-categories-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}-cache

      # If a build cache exists for agda-categories, use it, but don't fail if
      # there isn't.
      - name: Unpack agda-categories build cache
        if: steps.cache-everything.outputs.cache-hit == 'true'
        run: |
          cp -rpv ~/.agda-build-cache/agda-categories ./_build/ || exit 0

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

      - name: Install ghc and cabal
        if: steps.cache-everything.outputs.cache-hit != 'true'
        uses: haskell-actions/setup@v2
        with:
          ghc-version: ${{ env.GHC_VERSION }}
          cabal-version: ${{ env.CABAL_VERSION }}

      - name: Cabal update
        if: steps.cache-everything.outputs.cache-hit != 'true'
        run: cabal update

      - name: Download and install Agda from github
        if: steps.cache-everything.outputs.cache-hit != 'true'
        run: |
          git clone https://github.com/agda/agda
          cd agda
          git checkout ${{ env.AGDA_COMMIT }}
          mkdir -p doc
          touch doc/user-manual.pdf
          # make sure it exists
          mkdir -p $HOME/.cabal/bin
          ${{ env.CABAL_INSTALL }}
          cd ..

      - name: Install stdlib
        run: |
          mkdir -p $HOME/.agda
          cd $HOME/.agda
          wget https://github.com/agda/agda-stdlib/archive/v${{ env.STDLIB_VERSION }}.tar.gz
          tar -xzvf v${{ env.STDLIB_VERSION }}.tar.gz
          mv agda-stdlib-${{ env.STDLIB_VERSION }} agda-stdlib
          echo "~/.agda/agda-stdlib/standard-library.agda-lib" > libraries
          cd -

      # If a build cache exists for agda-stdlib, use it, but don't fail if there
      # isn't.
      - name: Unpack agda-stdlib build cache
        if: steps.cache-everything.outputs.cache-hit == 'true'
        run: |
          cp -rpv ~/.agda-build-cache/agda-stdlib ~/.agda/agda-stdlib/_build/ || exit 0

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

      # Generate a fresh Everything.agda & index.agda and start building!
      - name: Test agda-categories
        run: |
          cp travis/* .
          ./everything.sh
          ${{ env.AGDA }} Everything.agda
          ${{ env.AGDA }} index.agda

      # Note that if you want to deploy html for different versions like the
      # standard library does, you will need to be a bit more subtle in this
      # step.
      - name: Generate HTML
        run: |
          ${{ env.AGDA }} --html --html-dir html index.agda

########################################################################
## PACKAGE BUILD CACHING
########################################################################

      # Package type-checked agda-stdlib and agda-categories libraries for
      # future CI runs.
      - name: "Pack Agda build cache"
        run: |
          mkdir -p ~/.agda-build-cache/
          cp -rpv ./_build/ ~/.agda-build-cache/agda-categories/ || exit 0
          cp -rpv ~/.agda/agda-stdlib/_build/ ~/.agda-build-cache/agda-stdlib/ || exit 0

########################################################################
## DEPLOYMENT
########################################################################

      - name: Deploy HTML
        uses: JamesIves/github-pages-deploy-action@v4.6.8
        if: ${{ success() && env.AGDA_DEPLOY }}
        with:
          branch: gh-pages
          folder: html