[ ci ] Use pack for dependency management instead of pinned commits (#12

) * Fix indentation error. * Export infixr for <*>>. This resolves a build warning. * Replace deprecated functions. * Use pack for dependencies.
idris-community · Sep 4, 2024 · 3209050 · 3209050
1 parent c3ea8c3
commit 3209050
Show file tree

Hide file tree

Showing 5 changed files with 147 additions and 164 deletions.
diff --git a/.github/workflows/ci-lib.yml b/.github/workflows/ci-lib.yml
@@ -12,11 +12,7 @@ on:
 ########################################################################
 
 env:
-  IDRIS2_COMMIT: v0.6.0
   SCHEME: scheme
-  ELAB_COMMIT: 87f9d910f4669b38d9d2cd67b5a63922dffb1ab1
-  SOP_COMMIT: 87a30cf81117f387824f945374081ffa2effa8a0
-
 jobs:
   ubuntu-chez:
     runs-on: ubuntu-latest
@@ -29,152 +25,150 @@ jobs:
       - name: Checkout idris2-tls
         uses: actions/checkout@v2
 
-      - name: Install idris2-sop
-        run: pack install sop
+      - name: Install idris deps
+        run: pack install-deps tls.ipkg
 
       - name: Build package
         run: make install
 
       - name: Test package
         run: make test
 
-  windows-chez:
-    runs-on: windows-latest
-    env:
-      MSYSTEM: MINGW64
-      MSYS2_PATH_TYPE: inherit
-      SCHEME: scheme
-      CC: gcc
-    steps:
-      - name: Init
-        run: |
-          git config --global core.autocrlf false
-      - name: Checkout
-        uses: actions/checkout@v2
-      # This caching step allows us to save a lot of building time by only
-      # rebuilding Idris2 from boostrap if absolutely necessary
-      - name: Cache Idris2
-        uses: actions/cache@v2
-        id: cache-idris2
-        with:
-          path: |
-            ChezScheme
-            .idris2
-          key: ${{ runner.os }}-${{ env.IDRIS2_COMMIT }}
-      - name: Get Chez Scheme
-        if: steps.cache-idris2.outputs.cache-hit != 'true'
-        run: |
-          git clone --depth 1 https://github.com/cisco/ChezScheme
-          c:\msys64\usr\bin\bash -l -c "pacman -S --noconfirm tar make mingw-w64-x86_64-gcc"
-          echo "PWD=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
-      - name: Configure and Build Chez Scheme
-        if: steps.cache-idris2.outputs.cache-hit != 'true'
-        run: |
-          c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd ChezScheme && ./configure --threads && make"
-      - name: Set Path
-        run: |
-          $chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt"
-          $idris="$(pwd)\.idris2"
-          echo "$chez" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
-          echo "$idris\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
-          echo "IDRIS_PREFIX=$idris" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
-          echo "PREFIX=$(c:\msys64\usr\bin\cygpath -u $idris)" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
-      - name: Test Scheme
-        run: |
-          scheme --version
-      - name: Install Idris2
-        if: steps.cache-idris2.outputs.cache-hit != 'true'
-        run: |
-          git clone https://github.com/idris-lang/idris2
-          cd idris2
-          git checkout ${{ env.IDRIS2_COMMIT }}
-          c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd idris2 && make bootstrap && make install"
-      - name: Install idris2-elab-util
-        run: |
-          git clone https://github.com/stefan-hoeck/idris2-elab-util
-          cd idris2-elab-util
-          git checkout ${{ env.ELAB_COMMIT }}
-          make install
-
-      - name: Install idris2-sop
-        run: |
-          git clone https://github.com/stefan-hoeck/idris2-sop
-          cd idris2-sop
-          git checkout ${{ env.SOP_COMMIT }}
-          idris2 --install sop.ipkg
-
-      - name: Checkout idris2-tls
-        uses: actions/checkout@v2
-        with:
-          path: tls
-
-      - name: Build package
-        run: |
-          cd tls
-          echo "TLS=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
-          make install
-
-      - name: Test package
-        run: c:\msys64\usr\bin\bash -l -c "cd $env:TLS && make test"
-
-  macos-chez:
-    runs-on: macos-latest
-    env:
-      SCHEME: chez
-    steps:
-      # This caching step allows us to save a lot of building time by only
-      # rebuilding Idris2 from boostrap if absolutely necessary
-      - name: Cache Idris2
-        uses: actions/cache@v2
-        id: cache-idris2
-        with:
-          path: |
-            ~/.idris2
-          key: ${{ runner.os }}-${{ env.IDRIS2_COMMIT }}
-
-      - name: Install Idris2 build dependencies
-        run: |
-          brew install chezscheme
-          brew install coreutils
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-
-      - name: Build Idris 2 from bootstrap
-        if: steps.cache-idris2.outputs.cache-hit != 'true'
-        run: |
-          git clone https://github.com/idris-lang/idris2
-          cd idris2
-          git checkout ${{ env.IDRIS2_COMMIT }}
-          chmod -R a-w bootstrap
-          make bootstrap && make install
-        shell: bash
-
-      - name: Install idris2-elab-util
-        run: |
-          git clone https://github.com/stefan-hoeck/idris2-elab-util
-          cd idris2-elab-util
-          git checkout ${{ env.ELAB_COMMIT }}
-          make install
-        shell: bash
-
-      - name: Install idris2-sop
-        run: |
-          git clone https://github.com/stefan-hoeck/idris2-sop
-          cd idris2-sop
-          git checkout ${{ env.SOP_COMMIT }}
-          idris2 --install sop.ipkg
-        shell: bash
-
-      - name: Checkout idris2-tls
-        uses: actions/checkout@v2
-        with:
-          path: tls
-
-      - name: Build package
-        run: |
-          cd tls
-          make install
-
-      - name: Test package
-        run: |
-          cd tls
-          make test
+  # windows-chez:
+  #   runs-on: windows-latest
+  #   env:
+  #     MSYSTEM: MINGW64
+  #     MSYS2_PATH_TYPE: inherit
+  #     SCHEME: scheme
+  #     CC: gcc
+  #   steps:
+  #     - name: Init
+  #       run: |
+  #         git config --global core.autocrlf false
+  #     - name: Checkout
+  #       uses: actions/checkout@v2
+  #     # This caching step allows us to save a lot of building time by only
+  #     # rebuilding Idris2 from boostrap if absolutely necessary
+  #     - name: Cache Idris2
+  #       uses: actions/cache@v2
+  #       id: cache-idris2
+  #       with:
+  #         path: |
+  #           ChezScheme
+  #           .idris2
+  #         key: ${{ runner.os }}-${{ env.IDRIS2_COMMIT }}
+  #     - name: Get Chez Scheme
+  #       if: steps.cache-idris2.outputs.cache-hit != 'true'
+  #       run: |
+  #         git clone --depth 1 https://github.com/cisco/ChezScheme
+  #         c:\msys64\usr\bin\bash -l -c "pacman -S --noconfirm tar make mingw-w64-x86_64-gcc"
+  #         echo "PWD=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
+  #     - name: Configure and Build Chez Scheme
+  #       if: steps.cache-idris2.outputs.cache-hit != 'true'
+  #       run: |
+  #         c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd ChezScheme && ./configure --threads && make"
+  #     - name: Set Path
+  #       run: |
+  #         $chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt"
+  #         $idris="$(pwd)\.idris2"
+  #         echo "$chez" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
+  #         echo "$idris\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
+  #         echo "IDRIS_PREFIX=$idris" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
+  #         echo "PREFIX=$(c:\msys64\usr\bin\cygpath -u $idris)" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
+  #     - name: Test Scheme
+  #       run: |
+  #         scheme --version
+  #     - name: Install Idris2
+  #       if: steps.cache-idris2.outputs.cache-hit != 'true'
+  #       run: |
+  #         git clone https://github.com/idris-lang/idris2
+  #         cd idris2
+  #         git checkout ${{ env.IDRIS2_COMMIT }}
+  #         c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd idris2 && make bootstrap && make install"
+  #     - name: Install idris2-elab-util
+  #       run: |
+  #         git clone https://github.com/stefan-hoeck/idris2-elab-util
+  #         cd idris2-elab-util
+  #         git checkout ${{ env.ELAB_COMMIT }}
+  #         make install
+
+  #     - name: Checkout idris2-tls
+  #       uses: actions/checkout@v2
+  #       with:
+  #         path: tls
+
+  #     - name: Install idris deps
+  #       run: |
+  #         cd tls
+
+
+  #     - name: Build package
+  #       run: |
+  #         cd tls
+  #         echo "TLS=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
+  #         make install
+
+  #     - name: Test package
+  #       run: c:\msys64\usr\bin\bash -l -c "cd $env:TLS && make test"
+
+  # macos-chez:
+  #   runs-on: macos-latest
+  #   env:
+  #     SCHEME: chez
+  #   steps:
+  #     # This caching step allows us to save a lot of building time by only
+  #     # rebuilding Idris2 from boostrap if absolutely necessary
+  #     - name: Cache Idris2
+  #       uses: actions/cache@v2
+  #       id: cache-idris2
+  #       with:
+  #         path: |
+  #           ~/.idris2
+  #         key: ${{ runner.os }}-${{ env.IDRIS2_COMMIT }}
+
+  #     - name: Install Idris2 build dependencies
+  #       run: |
+  #         brew install chezscheme
+  #         brew install coreutils
+  #         echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+
+  #     - name: Build Idris 2 from bootstrap
+  #       if: steps.cache-idris2.outputs.cache-hit != 'true'
+  #       run: |
+  #         git clone https://github.com/idris-lang/idris2
+  #         cd idris2
+  #         git checkout ${{ env.IDRIS2_COMMIT }}
+  #         chmod -R a-w bootstrap
+  #         make bootstrap && make install
+  #       shell: bash
+
+  #     - name: Install idris2-elab-util
+  #       run: |
+  #         git clone https://github.com/stefan-hoeck/idris2-elab-util
+  #         cd idris2-elab-util
+  #         git checkout ${{ env.ELAB_COMMIT }}
+  #         make install
+  #       shell: bash
+
+  #     - name: Install idris2-sop
+  #       run: |
+  #         git clone https://github.com/stefan-hoeck/idris2-sop
+  #         cd idris2-sop
+  #         git checkout ${{ env.SOP_COMMIT }}
+  #         idris2 --install sop.ipkg
+  #       shell: bash
+
+  #     - name: Checkout idris2-tls
+  #       uses: actions/checkout@v2
+  #       with:
+  #         path: tls
+
+  #     - name: Build package
+  #       run: |
+  #         cd tls
+  #         make install
+
+  #     - name: Test package
+  #       run: |
+  #         cd tls
+  #         make test
diff --git a/pack.toml b/pack.toml
diff --git a/src/Crypto/Random/JS.idr b/src/Crypto/Random/JS.idr
@@ -23,7 +23,7 @@ public export
 HasIO io => MonadRandom io where
   random_bytes Z = pure []
   random_bytes n =
-  case codegen of
-    "node" => buffer_content prim_io__randomBytes n
-    "javascript" => buffer_content prim_io__getRandomValues n
-    _ => assert_total $ idris_crash "no random backend availible"
+    case codegen of
+      "node" => buffer_content prim_io__randomBytes n
+      "javascript" => buffer_content prim_io__getRandomValues n
+      _ => assert_total $ idris_crash "no random backend availible"
diff --git a/src/Network/TLS/Parsing.idr b/src/Network/TLS/Parsing.idr
@@ -14,7 +14,7 @@ namespace Parserializer
     encode : a -> List c
     decode : Parser i e a
 
-  infixr 5 <*>>
+  export infixr 5 <*>>
 
   export
   apair : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (a, b)

diff --git a/src/Utils/Bytes.idr b/src/Utils/Bytes.idr
@@ -140,9 +140,9 @@ shiftR' x i = maybe_a_a zeroBits $ do
 export
 rotl : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
 rotl FZ x = x
-rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ invFin $ coerce prf $ weaken i)
+rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ complement $ coerce prf $ weaken i)
 
 export
 rotr : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
 rotr FZ x = x
-rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ invFin $ coerce prf $ weaken i)
+rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ complement $ coerce prf $ weaken i)