[ ci ] Use the latest Agda but check cubical without `NoEquivWhenSp…

…litting` warnings (#697)

As title.

.github/workflows/ci-ubuntu.yml

@@ -33,81 +33,72 @@ on:
 ########################################################################
 
 env:
-  GHC_VERSION: 8.6.5
-  CABAL_VERSION: 3.2.0.0
-  CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
+  GHC_VERSION: 8.10.7
+  CABAL_VERSION: latest
+  CABAL_BIN : $HOME/.local/bin
+  CABAL_INSTALL: cabal install --installdir=$HOME/.local/bin --overwrite-policy=always --ghc-options='+RTS -M6G -RTS'
+  AGDA_COMMIT: 382861b1967b7ced0806343b8410709b2ce91df0
 
 jobs:
   test-cubical:
     runs-on: ubuntu-latest
     steps:
 
-      ########################################################################
-      ## SETTINGS
-      ##
-      ## 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).
-      ########################################################################
-
-      - name: Initialise variables
-        run: |
-          # Pick Agda version
-          echo "AGDA_BRANCH=v2.6.2" >> $GITHUB_ENV
-
       ########################################################################
       ## 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: Cache cabal packages
         uses: actions/cache@v2
-        id: cache-cabal
+        id: cache
         with:
           path: |
-            ~/.ghcup/bin
-            ~/.cabal/packages
-            ~/.cabal/store
-            ~/.cabal/bin
-          key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}
+            $HOME/.local/bin
+            ~/.local/bin
+            ~/.cabal/
+          key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}
 
       ########################################################################
       ## INSTALLATION STEPS
       ########################################################################
+      #
 
-      - name: Install cabal
-        if: steps.cache-cabal.outputs.cache-hit != 'true'
-        uses: actions/setup-haskell@v1.1.3
+      - name: Set up the GHC environment
+        if: ${{ !steps.cache.outputs.cache-hit }}
+        id: ghc-setup
+        uses: haskell/actions/setup@v1
         with:
           ghc-version: ${{ env.GHC_VERSION }}
           cabal-version: ${{ env.CABAL_VERSION }}
 
-      - name: Put cabal programs in PATH
-        run: echo "~/.cabal/bin" >> $GITHUB_PATH
+      - name: Create directory for binary
+        run: |
+          mkdir -p ${{ env.CABAL_BIN }}
+          echo ${{ env.CABAL_BIN }} >> $GITHUB_PATH
 
-      - name: Cabal update
-        run: cabal update
+      - name: Install fix-whitespace
+        if: ${{ !steps.cache.outputs.cache-hit }}
+        run: |
+          ${{ env.CABAL_INSTALL }} fix-whitespace
+          strip ${{ env.CABAL_BIN }}/fix-whitespace
+
+      - name: Check out Agda from GitHub
+        uses: actions/checkout@v2
+        if: ${{ !steps.cache.outputs.cache-hit }}
+        with:
+          repository: agda/agda
+          ref: ${{ env.AGDA_COMMIT }}
+          path: agda
 
-      - name: Download and install Agda from github
-        if: steps.cache-cabal.outputs.cache-hit != 'true'
+      - name: Install Agda
+        if: ${{ !steps.cache.outputs.cache-hit }}
         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 ..
-
-      - name: Download and install fix-whitespace
-        if: steps.cache-cabal.outputs.cache-hit != 'true'
-        run: |
-          git clone https://github.com/agda/fix-whitespace --depth=1
-          cd fix-whitespace
-          ${{ env.CABAL_INSTALL }} fix-whitespace.cabal
-          cd ..
+          strip ${{ env.CABAL_BIN }}/agda
 
       ########################################################################
       ## TESTING
@@ -119,17 +110,11 @@ jobs:
 
       - name: Test cubical
         run: |
-          make test \
-            AGDA_EXEC='~/.cabal/bin/agda -W error' \
-            FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \
-            RUNHASKELL='~/.ghcup/bin/runhaskell'
+          make test
 
       - name: Htmlize cubical
         run: |
-          make listings \
-            AGDA_EXEC='~/.cabal/bin/agda -W error' \
-            FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \
-            RUNHASKELL='~/.ghcup/bin/runhaskell'
+          make listings
 
       - name: Deploy to GitHub Pages
         if: github.event_name == 'push' && github.ref_name == 'master'

GNUmakefile

@@ -1,18 +1,18 @@
-AGDA_BIN?=agda
-AGDA_FLAGS?=-W error
-AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS)
-FIX_WHITESPACE?=fix-whitespace
-RTS_OPTIONS=+RTS -H3G -RTS
-AGDA=$(AGDA_EXEC) $(RTS_OPTIONS)
-RUNHASKELL?=runhaskell
-EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs
+AGDA_BIN    ?= agda
+AGDA_FLAGS  ?= -W noNoEquivWhenSplitting -W error
+AGDA_EXEC   ?= $(AGDA_BIN) $(AGDA_FLAGS)
+RTS_OPTIONS = +RTS -H3G -RTS
+AGDA        = $(AGDA_EXEC) $(RTS_OPTIONS)
+
+FIX_WHITESPACE ?= fix-whitespace
+RUNHASKELL     ?= runhaskell
+EVERYTHINGS    =  $(RUNHASKELL) ./Everythings.hs
 
 .PHONY : all
 all : build
 
 .PHONY : build
-build :
-	$(MAKE) AGDA_EXEC=$(AGDA_BIN) gen-everythings check
+build : gen-everythings check
 
 .PHONY : test
 test : check-whitespace gen-and-check-everythings check-README check