From cc49d9b811a03e3c44f6ed548f6582d601b51705 Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Fri, 5 Jan 2024 21:07:40 +0000
Subject: [PATCH] use pack DB HEAD in CI (#382)

---
 .github/workflows/checks.yml       | 12 +++++++++---
 .github/workflows/release-docs.yml |  1 +
 src/Util.idr                       |  6 ------
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml
index a2e276e4c..67256b941 100644
--- a/.github/workflows/checks.yml
+++ b/.github/workflows/checks.yml
@@ -30,7 +30,9 @@ jobs:
         ./install_bazel.sh
         ./build.sh cpu
     - name: Build tests
-      run: pack --no-prompt build test.ipkg
+      run: |
+        pack switch HEAD
+        pack --no-prompt build test.ipkg
     - name: Run tests
       run: pack run test.ipkg
       env:
@@ -41,11 +43,15 @@ jobs:
     steps:
     - uses: actions/checkout@v3
     - name: Type-check README
-      run: pack --no-prompt typecheck readme.ipkg
+      run: |
+        pack switch HEAD
+        pack --no-prompt typecheck readme.ipkg
   tutorials:
     runs-on: ubuntu-latest
     container: ghcr.io/stefan-hoeck/idris2-pack
     steps:
     - uses: actions/checkout@v3
     - name: Type-check tutorials
-      run: res=0; for f in tutorials/*.ipkg; do pack --no-prompt typecheck $f || res=$?; done; $(exit $res)
+      run: |
+        pack switch HEAD
+        res=0; for f in tutorials/*.ipkg; do pack --no-prompt typecheck $f || res=$?; done; $(exit $res)
diff --git a/.github/workflows/release-docs.yml b/.github/workflows/release-docs.yml
index a529817b1..303e4ea97 100644
--- a/.github/workflows/release-docs.yml
+++ b/.github/workflows/release-docs.yml
@@ -27,6 +27,7 @@ jobs:
     steps:
     - uses: actions/checkout@v3
     - run: |
+        pack switch HEAD
         pack --no-prompt --with-docs install spidr
         mv build/docs .
     - run: |
diff --git a/src/Util.idr b/src/Util.idr
index 2ba17c52d..8821a940f 100644
--- a/src/Util.idr
+++ b/src/Util.idr
@@ -146,12 +146,6 @@ namespace List
   inBoundsCons _ InFirst = InFirst
   inBoundsCons (_ :: ys) (InLater prf) = InLater (inBoundsCons ys prf)
 
-||| Concatenate lists of proofs.
-public export
-(++) : All p xs -> All p ys -> All p (xs ++ ys)
-[] ++ pys = pys
-(px :: pxs) ++ pys = px :: (pxs ++ pys)
-
 ||| Apply a function to the environment of a reader.
 export
 (>$<) : (env' -> env) -> Reader env a -> Reader env' a