use pack DB HEAD in CI (#382)

joelberkeley · Jan 5, 2024 · cc49d9b · cc49d9b
1 parent c1bde4a
commit cc49d9b
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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