Search code examples
installationpackageidris

INTERNAL ERROR when installing local package

I'm getting

Uncaught error: INTERNAL ERROR: Can't make directory foo

when trying to install my local library. I'm running idris2 --install foo.ipkg in a directory

.
+-foo.ipkg
+-src
  +-Util.idr

with file contents

package foo 
version = "0.0.1"

sourcedir = "src"
modules = Util

and

module Util

I've been following these docs and I'm wondering whether this has something to do with write permissions and the $PREFIX they mention. Setting PREFIX=<some_dir> idris2 --install foo.ipkg didn't help.

Solution

  • Apparently it's cos the compiler doesn't create the necessary directories yet (fix is pending). It can be fixed by creating the directories manually and setting the $IDRIS2_PREFIX ($PREFIX is for when using make)

    mkdir -p out/idris2-0.3.0
IDRIS2_PREFIX=$(pwd)/out idris2 --install foo.ipkg

    I don't understand why this means I can then use the foo package in my executables (from the docs I'd have thought I need to put them in a depends directory, or perhaps export IDRIS2_PREFIX=$(pwd)/out) but I can.

    Presumably this will also mean other dependencies aren't accessible if they're not in out/. I've only got one dependency here so I haven't tried.