main.yml

# This is a basic workflow to help you get started with Actions

name: CI

# Controls when the workflow will run
on:
  # Triggers the workflow on push or pull request events but only for the "main" branch
  push:
    branches:
      - main
      - impl
    paths-ignore:
      - 'paper/*'
      - 'notes/*'
  pull_request:
    branches:
      - main
    paths-ignore:
      - 'paper/*'
      - 'notes/*'

  # Allows you to run this workflow manually from the Actions tab
  workflow_dispatch:

########################################################################
## 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.7.0.1
  GHC_VERSION: 9.8.2
  CABAL_VERSION: 3.10.2.1
  CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
  CACHE_PATHS: |
    ~/.cabal/packages
    ~/.cabal/store
    ~/.cabal/bin

# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
  check-whitespace:
    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
      ########################################################################
      ## INSTALLATION STEPS
      ########################################################################
      - name: Download and install fix-whitespace
        run: |
          cd ~
          git clone https://github.com/agda/fix-whitespace --depth=1
          cd fix-whitespace
          ${{ env.CABAL_INSTALL }} fix-whitespace.cabal
          cd ..
      ########################################################################
      ## CHECKOUT
      ########################################################################

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

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

      - name: Test whitespace
        run: |
          ~/.cabal/bin/fix-whitespace --check

  compile-agda:
    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
      ########################################################################
      ## INSTALLATION STEPS
      ########################################################################

      - name: Download and install Agda from github
        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 Cubical from github
        run : |
          cd ~
          git clone https://github.com/agda/cubical --branch master
          cd cubical
          git checkout 581748b01bc43a25295993347bdc8c7cb2166090
          cd ..
          echo "CUBICAL_DIR=$PWD/cubical" >> "$GITHUB_ENV"

      - name: Download categorical-logic from github
        run : |
          cd ~
          git clone https://github.com/maxsnew/cubical-categorical-logic --branch main
          cd cubical-categorical-logic
          git checkout 4e7b1c3a2ba7ed528b3cd9a4c3a5e7be3ff3449d
          cd ..
          echo "CATLOG_DIR=$PWD/cubical-categorical-logic" >> "$GITHUB_ENV"

      - name: Set up Agda dependencies
        run : |
          mkdir ~/.agda
          touch ~/.agda/libraries
          echo "$CUBICAL_DIR/cubical.agda-lib" >> ~/.agda/libraries
          echo "$CATLOG_DIR/cubical-categorical-logic.agda-lib" >> ~/.agda/libraries
          echo "$GITHUB_WORKSPACE/code/cubical/grammar.agda-lib" >> ~/.agda/libraries

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

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

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

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

      - name: Test grammars-and-semantic-actions
        run: |
          cd code/cubical && make quicktest \
            AGDA='~/.cabal/bin/agda +RTS -M6G -RTS -WnoUnsupportedIndexedMatch -W error' \