main.yml

# This workflow inspired by the workflow at
# jonsterling/agda-calf
on: [push]

jobs:
  build:
    runs-on: ubuntu-latest
    timeout-minutes: 60

    strategy:
      matrix:
        agda-ref: ["v2.6.4"]
        ghc-ver: ["8.10.2"]
        cabal-ver: ["3.4.0.0"]
        cubical-ref: ["rahulc29/realizability"]
    steps:
    - uses: actions/cache@v2
      name: Cache cabal packages
      id: cache-cabal
      with:
        path: |
          ~/.cabal/packages
          ~/.cabal/store
          ~/.cabal/bin
          ~/.local/bin
          dist-newstyle
        key: ${{ runner.os }}-${{ matrix.ghc-ver }}-${{ matrix.cabal-ver }}-${{ matrix.agda-ref }}
    - name: Install cabal
      if: steps.cache-cabal.outputs.cache != 'true'
      uses: actions/setup-haskell@v1.1.3
      with:
        ghc-version: ${{ matrix.ghc-ver }}
        cabal-version: ${{ matrix.cabal-ver }}
    - name: Put cabal binaries in PATH
      run: echo "~/.cabal/bin" >> $GITHUB_PATH
    - name: Download Agda from Github
      if: steps.cache-cabal.outputs.cache-hit != 'true'
      uses: actions/checkout@v2
      with:
        repository: agda/agda
        path: agda
        ref: ${{ matrix.agda-ref }}
    - name: Install Agda
      if: steps.cache-cabal.outputs.cache-hit != 'true'
      run: |
        cabal update
        cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' alex-3.2.5
        cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' happy-1.19.12
        cd agda
        mkdir -p doc
        touch doc/user-manual.pdf
        cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
    - name: Checkout realizability fork of Cubical
      uses: actions/checkout@v4
      with:
        repository: rahulc29/cubical
        ref: ${{ matrix.cubical-ref }}
    - name: Put cubical library in Agda library list
      run: |
        mkdir -p ~/.agda/
        touch ~/.agda/libraries
        echo "$GITHUB_WORKSPACE/cubical/cubical.agda-lib" > ~/.agda/libraries
    - name: Checkout master
      uses: actions/checkout@v4
      with:
        path: master

    - name: Compile main library
      run: |
        cd master
        cd src
        agda --html --html-dir=../docs index.agda