bump version to v0.0.5 (#321)

* migrate to pack package manager
* update Idris version to latest

.github/workflows/checks.yml

@@ -15,39 +15,35 @@ on:
   pull_request:
     branches: master
 
+env:
+  PACK_DIR: /root/.pack
+
 jobs:
   test-unit:
     runs-on: ubuntu-latest
+    container: ghcr.io/stefan-hoeck/idris2-pack
     steps:
     - uses: actions/checkout@v2
-    - run: /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
-    - run: |
-        eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"
-        brew install idris2
-        wget -qO- https://github.com/elixir-nx/xla/releases/download/v0.3.0/xla_extension-x86_64-linux-cpu.tar.gz | tar xvz -C backend/
-
-        sudo apt install -y apt-transport-https curl gnupg
+    - name: Install Bazel
+      run: |
+        apt update && apt upgrade -y && apt install -y apt-transport-https curl gnupg
         curl -fsSL https://bazel.build/bazel-release.pub.gpg | gpg --dearmor > bazel.gpg
-        sudo mv bazel.gpg /etc/apt/trusted.gpg.d/
-        echo "deb [arch=amd64] https://storage.googleapis.com/bazel-apt stable jdk1.8" | sudo tee /etc/apt/sources.list.d/bazel.list
-        sudo apt update && sudo apt install bazel
-
+        mv bazel.gpg /etc/apt/trusted.gpg.d/
+        echo "deb [arch=amd64] https://storage.googleapis.com/bazel-apt stable jdk1.8" | tee /etc/apt/sources.list.d/bazel.list
+        apt update && apt install -y bazel
+    - name: Install XLA
+      run: |
+        apt install -y wget
+        wget -qO- https://github.com/elixir-nx/xla/releases/download/v0.3.0/xla_extension-x86_64-linux-cpu.tar.gz | tar xvz -C backend/
         (cd backend; BAZEL_CXXOPTS='-std=c++14' bazel build //:c_xla_extension)
-        export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$(pwd)/backend/bazel-bin
-
-        ./install_deps.sh
-        idris2 --install spidr.ipkg
-        ./test/install_deps.sh
-        idris2 --install test.ipkg
-        ./build/exec/test
+    - name: Run tests
+      run: pack run test.ipkg
+      env:
+        LD_LIBRARY_PATH: $LD_LIBRARY_PATH:backend/bazel-bin
   tutorials:
     runs-on: ubuntu-latest
+    container: ghcr.io/stefan-hoeck/idris2-pack
     steps:
     - uses: actions/checkout@v2
-    - run: /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
-    - run: |
-        eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"
-        brew install idris2
-        ./install_deps.sh
-        idris2 --install spidr.ipkg
-        res=0; for f in tutorials/*.md; do idris2 --check -p contrib -p hashable "$f" || res=$?; done; $(exit $res)
+    - name: Type-check tutorials
+      run: res=0; for f in tutorials/*.ipkg; do pack typecheck $f || res=$?; done; $(exit $res)

.github/workflows/release.yml

@@ -13,16 +13,17 @@
 # limitations under the License.
 on: release
 
+env:
+  PACK_DIR: /root/.pack
+
 jobs:
   docs:
     runs-on: ubuntu-latest
+    container: ghcr.io/stefan-hoeck/idris2-pack
     steps:
     - uses: actions/checkout@v2
-    - run: /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
     - run: |
-        eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"
-        brew install idris2
-        idris2 --mkdoc spidr.ipkg
+        pack --with-docs install spidr
         mv build/docs .
     - run: |
         git add .

INSTALL.md

@@ -1,30 +1,50 @@
 # Installation
 
-**Note:** these instructions may have changed since the latest release. Navigate to the instructions at the latest git tag for accurate details.
-
 ## Install the Idris frontend
 
-1. Clone or download the spidr source code at tag v0.0.4 with, for example,
-   ```bash
-   git clone --depth 1 --branch v0.0.4 https://github.com/joelberkeley/spidr.git
+1. Install the Idris2 package manager [pack](https://github.com/stefan-hoeck/idris2-pack).
+2. Install spidr with
    ```
-   See the git history for installing earlier versions.
-2. [Install Idris 2](https://github.com/idris-lang/Idris2/blob/main/INSTALL.md). We recommend using [Homebrew](https://brew.sh/) if you're unsure which option to use.
-3. Install spidr's Idris dependencies by running `./install_deps.sh` located in the spidr root directory.
-4. In the spidr root directory, install spidr with
-   ```bash
-   idris2 --install spidr.ipkg
+   pack install spidr
    ```
-5. When building your Idris code that depends on spidr, either include `-p spidr` on the command line, or list spidr as a dependency in your project's configuration. In both cases, you will need to include spidr's dependencies with `-p hashable` on the command line or add `hashable` to your project's .ipkg `depends`.
 
 ## Install the XLA backend
 
-6. Download the XLA C interface from the [releases page](https://github.com/joelberkeley/spidr/releases), and extract the archive. The extracted directory can be placed anywhere you wish.
-7. Download an XLA binary from [elixir-nx/xla](https://github.com/elixir-nx/xla/releases), and extract the archive. See the spidr releases page for details of which versions are supported. Place the directory `xla_extension` into the same path as the directory `c_xla_extension` extracted in step 6.
-8. When running code that depends on spidr, you may need to set `LD_LIBRARY_PATH` to include the location of the libc_xla_extension.so shared library located in `c_xla_extension` extracted in step 6.
+### CPU only
 
-## Additional steps for execution on GPU
+If you intend to run spidr on GPU, skip to the [GPU instructions](#gpu)
 
-**Note:** We have only tested this on a machine with a single GPU.
+3. Install XLA
+   ```bash
+   wget https://github.com/elixir-nx/xla/releases/download/v0.3.0/xla_extension-x86_64-linux-cpu.tar.gz -qO- | sudo tar -C /usr/local/lib -xvz ./xla_extension/lib/libxla_extension.so
+   ```
+   ```bash
+   sudo bash -c 'echo "/usr/local/lib/xla_extension/lib" >> /etc/ld.so.conf.d/xla_extension.conf' && sudo ldconfig
+   ```
+4. Install the C interface to XLA
+   ```bash
+   wget https://github.com/joelberkeley/spidr/releases/download/v0.0.5/c_xla_extension-x86_64-linux-cpu.tar.gz -qO- | sudo tar -C /usr/local/lib -xvz ./c_xla_extension/lib/libc_xla_extension.so
+   ```
+   ```bash
+   sudo bash -c 'echo "/usr/local/lib/c_xla_extension/lib" >> /etc/ld.so.conf.d/c_xla_extension.conf' && sudo ldconfig
+   ```
 
-9. Install the NVIDIA prerequisites for running TensorFlow on GPU, as listed on the TensorFlow GPU [installation page](https://www.tensorflow.org/install/gpu). **There is no need to install TensorFlow itself**.
+### GPU
+
+If you do *not* intend to run spidr on GPU, skip this section.
+
+3. Install the NVIDIA prerequisites for running TensorFlow on GPU, as listed on the TensorFlow GPU [installation page](https://www.tensorflow.org/install/gpu). **There is no need to install TensorFlow itself**.
+4. Install XLA
+   ```bash
+   wget https://github.com/elixir-nx/xla/releases/download/v0.3.0/xla_extension-x86_64-linux-cuda111.tar.gz -qO- | sudo tar -C /usr/local/lib -xvz ./xla_extension/lib/libxla_extension.so
+   ```
+   ```bash
+   sudo bash -c 'echo "/usr/local/lib/xla_extension/lib" >> /etc/ld.so.conf.d/xla_extension.conf' && sudo ldconfig
+   ```
+5. Install the C interface to XLA
+   ```bash
+   wget https://github.com/joelberkeley/spidr/releases/download/v0.0.5/c_xla_extension-x86_64-linux-cuda111.tar.gz -qO- | sudo tar -C /usr/local/lib -xvz ./c_xla_extension/lib/libc_xla_extension.so
+   ```
+   ```bash
+   sudo bash -c 'echo "/usr/local/lib/c_xla_extension/lib" >> /etc/ld.so.conf.d/c_xla_extension.conf' && sudo ldconfig
+   ```

pack.toml

@@ -0,0 +1,4 @@
+[custom.all.spidr]
+type = "local"
+path = ""
+ipkg = "spidr.ipkg"

spidr.ipkg

@@ -1,5 +1,5 @@
 package spidr
-version = 0.0.4
+version = 0.0.5
 
 depends = contrib, hashable
 opts = "--total"

src/Tensor.idr

@@ -555,7 +555,7 @@ broadcast :
   Tensor from dtype ->
   Tensor to dtype
 broadcast xs with (xs)
-  _ | (MkTensor {shape=from} expr) = MkTensor $ Broadcast {dtype} from to expr
+  _ | (MkTensor {shape=_} expr) = MkTensor $ Broadcast {dtype} from to expr
 
 %hint
 export
@@ -938,7 +938,7 @@ namespace Scalarwise
   export
   (*) : Primitive.Num dtype => Tensor [] dtype -> Tensor (d :: ds) dtype -> Tensor (d :: ds) dtype
   l * r with (r)
-    _ | (MkTensor {shape=(d :: ds)} _) = (broadcast {shapesOK=scalarToAnyOk (d :: ds)} l) * r
+    _ | (MkTensor {shape=_ :: _} _) = (broadcast {shapesOK=scalarToAnyOk (d :: ds)} l) * r
 
 namespace Semigroup
   export
@@ -973,7 +973,7 @@ namespace Scalarwise
     Tensor [] dtype ->
     Tensor (d :: ds) dtype
   l / r with (l)
-    _ | (MkTensor {shape=(d :: ds)} _) = l / (broadcast {shapesOK=scalarToAnyOk (d :: ds)} r)
+    _ | (MkTensor {shape=_ :: _} _) = l / (broadcast {shapesOK=scalarToAnyOk (d :: ds)} r)
 
 ||| The element-wise reciprocal. For example, `recip (fromLiteral [-2, 0, 0.2])`
 ||| is `fromLiteral [-0.5, nan, 5]`.
@@ -1200,7 +1200,7 @@ namespace Vector
   export
   (|\) : Tensor [m, m] F64 -> Tensor [m] F64 -> Tensor [m] F64
   a |\ b with (b)
-    _ | MkTensor {shape=[m]} _ = squeeze (a |\ (expand 1 b))
+    _ | MkTensor {shape=[_]} _ = squeeze (a |\ (expand 1 b))
 
   ||| Solve the set of linear equations `a @@ x = b` for `x` where `a` is an upper-triangular
   ||| matrix. `a` is given by the upper-triangular elements of the first argument. Values in the
@@ -1212,7 +1212,7 @@ namespace Vector
   export
   (\|) : Tensor [m, m] F64 -> Tensor [m] F64 -> Tensor [m] F64
   a \| b with (b)
-    _ | MkTensor {shape=[m]} _ = squeeze (a \| (expand 1 b))
+    _ | MkTensor {shape=[_]} _ = squeeze (a \| (expand 1 b))
 
 ||| Sum the elements along the diagonal of the input. For example,
 ||| `trace (fromLiteral [[-1, 5], [1, 4]])` is `3`.
@@ -1223,7 +1223,7 @@ trace :
   Tensor [S n, S n] dtype ->
   Tensor [] dtype
 trace x with (x)
-  _ | MkTensor {shape=[S n, S n]} _ = reduce @{Sum} [0, 1] (x * identity)
+  _ | MkTensor {shape=[_, _]} _ = reduce @{Sum} [0, 1] (x * identity)
 
 ||| A `Rand a` produces a pseudo-random value of type `a` from a `Tensor [1] U64` state.
 ||| The state is updated each time a new value is generated.

src/Util.idr

@@ -63,37 +63,6 @@ namespace List
   enumerate : List a -> List (Nat, a)
   enumerate xs = toList (enumerate (fromList xs))
 
-  ||| Insert a value in a list. For example, `insertAt 1 [6, 7, 8] 9` is `[6, 9, 7, 8]`, and
-  ||| `insertAt 3 [6, 7, 8] 9` is `[6, 7, 8, 9]`.
-  |||
-  ||| @idx The index of the value in the resulting list.
-  ||| @xs The list to insert the value into.
-  ||| @x The value to insert.
-  public export
-  insertAt : (idx : Nat) -> (x : a) -> (xs : List a) -> {auto 0 prf : idx `LTE` length xs} -> List a
-  insertAt Z x xs = x :: xs
-  insertAt {prf=LTESucc _} (S n) x (y :: ys) = y :: (insertAt n x ys)
-
-  ||| Replace an element in a list. For example, `replaceAt 2 6 [1, 2, 3, 4]` is `[1, 2, 6, 4]`.
-  |||
-  ||| @idx The index of the value to replace.
-  ||| @x The value to insert.
-  ||| @xs The list in which to replace an element.
-  public export
-  replaceAt : (idx : Nat) -> a -> (xs : List a) -> {auto 0 prf : InBounds idx xs} -> List a
-  replaceAt Z y (_ :: xs) {prf=InFirst} = y :: xs
-  replaceAt (S k) y (x :: xs) {prf=InLater _} = x :: replaceAt k y xs
-
-  ||| Delete a value from a list at the specified index. For example, `deleteAt 1 [3, 4, 5]` is
-  ||| `[3, 5]`.
-  |||
-  ||| @idx The index of the value to delete.
-  ||| @xs The list to delete the value from.
-  public export
-  deleteAt : (idx : Nat) -> (xs : List a) -> {auto 0 prf : InBounds idx xs} -> List a
-  deleteAt {prf=InFirst} Z (_ :: xs) = xs
-  deleteAt {prf=InLater _} (S k) (x :: xs) = x :: deleteAt k xs
-
   namespace All
     ||| Map a constrained function over a list given a list of constraints.
     public export
@@ -115,20 +84,19 @@ namespace List
     ||| A list is sorted if its tail is sorted and the head is sorted w.r.t. the head of the tail.
     SCons : (y : a) -> f y x -> Sorted f (x :: xs) -> Sorted f (y :: x :: xs)
 
-  namespace Many
-    ||| Delete values from a list at specified indices. For example `deleteAt [0, 2] [5, 6, 7, 8]
-    ||| is `[6, 8]`.
-    |||
-    ||| @idxs The indices of the values to delete.
-    ||| @xs The list to delete values from.
-    public export
-    deleteAt :
-      (idxs : List Nat) ->
-      (xs : List a) ->
-      {auto 0 unique : Sorted LT idxs} ->
-      {auto 0 inBounds : All (flip InBounds xs) idxs} ->
-      List a
-    deleteAt idxs xs = go 0 idxs xs where
-      go : Nat -> List Nat -> List a -> List a
-      go j (i :: is) (x :: xs) = ifThenElse (i == j) (go (S j) is xs) (x :: go (S j) (i :: is) xs)
-      go _ _ xs = xs
+  ||| Delete values from a list at specified indices. For example `deleteAt [0, 2] [5, 6, 7, 8]
+  ||| is `[6, 8]`.
+  |||
+  ||| @idxs The indices of the values to delete.
+  ||| @xs The list to delete values from.
+  public export
+  deleteAt :
+    (idxs : List Nat) ->
+    (xs : List a) ->
+    {auto 0 unique : Sorted LT idxs} ->
+    {auto 0 inBounds : All (flip InBounds xs) idxs} ->
+    List a
+  deleteAt idxs xs = go 0 idxs xs where
+    go : Nat -> List Nat -> List a -> List a
+    go j (i :: is) (x :: xs) = ifThenElse (i == j) (go (S j) is xs) (x :: go (S j) (i :: is) xs)
+    go _ _ xs = xs

test.ipkg

@@ -1,13 +1,13 @@
 package test
 
 depends =
-  contrib,
+  spidr,
   hashable,
-  elab-util,
+  contrib,
   hedgehog,
+  elab-util,
   pretty-show,
-  sop,
-  spidr
+  sop
 
 opts = "--total"
 sourcedir = "test"

test/Unit/TestTensor.idr

@@ -1282,7 +1282,7 @@ normal = withTests 20 . property $ do
 
       ksTest := iidKolmogorovSmirnov samples normalCdf
 
-  diff (toLiteral ksTest) (<) 0.017
+  diff (toLiteral ksTest) (<) 0.02
 
 covering
 normalSeedIsUpdated : Property