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
    paths-ignore:
      - 'README.org'
      - 'Notes/*'
  pull_request:
    branches:
      - main
    paths-ignore:
      - 'README.org'
      - '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.6.4
  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



# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
  line-lengths:
    runs-on: ubuntu-latest

    steps:
    - uses: actions/checkout@v3

    - name: Set up Python 3.8
      uses: actions/setup-python@v2
      with:
        python-version: 3.8

    - name: Install dependencies
      run: |
        python -m pip install --upgrade pip
        pip install wcwidth

    - name: Check line lengths
      run: 'make check-line-lengths'

  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 cubical-categorical-logic
        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: Set up Agda dependencies
        run : |
          mkdir ~/.agda
          touch ~/.agda/libraries
          echo "$CUBICAL_DIR/cubical.agda-lib" >> ~/.agda/libraries
          echo "$GITHUB_WORKSPACE/cubical-categorical-logic.agda-lib" >> ~/.agda/libraries


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

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

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

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

      - name: Test cubical-categorical-logic
        run: |
          make test \
            AGDA='~/.cabal/bin/agda +RTS -M6G -RTS -WnoUnsupportedIndexedMatch -W error' \