From 3209050628b89811a5cd247dac44d19bd555aab2 Mon Sep 17 00:00:00 2001 From: Reily Siegel Date: Wed, 4 Sep 2024 15:46:08 -0400 Subject: [PATCH] [ 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. --- .github/workflows/ci-lib.yml | 286 +++++++++++++++++------------------ pack.toml | 11 -- src/Crypto/Random/JS.idr | 8 +- src/Network/TLS/Parsing.idr | 2 +- src/Utils/Bytes.idr | 4 +- 5 files changed, 147 insertions(+), 164 deletions(-) delete mode 100644 pack.toml diff --git a/.github/workflows/ci-lib.yml b/.github/workflows/ci-lib.yml index 59a8786..2a92e07 100644 --- 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,8 +25,8 @@ 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 @@ -38,143 +34,141 @@ jobs: - 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 deleted file mode 100644 index 20a585a..0000000 --- a/pack.toml +++ /dev/null @@ -1,11 +0,0 @@ -[custom.all.elab-util] -type = "git" -url = "https://github.com/stefan-hoeck/idris2-elab-util" -commit = "latest:main" -ipkg = "elab-util.ipkg" - -[custom.all.sop] -type = "git" -url = "https://github.com/stefan-hoeck/idris2-sop" -commit = "latest:main" -ipkg = "sop.ipkg" diff --git a/src/Crypto/Random/JS.idr b/src/Crypto/Random/JS.idr index 548198d..2d3df9b 100644 --- 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 index 42e033e..0125297 100644 --- 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 index 21b2132..ad51ac6 100644 --- 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)