I'm trying to compile an Agda file, but I'm having trouble getting it to find the standard library. I've seen the documentation here.
I've used Stack to install it:
> which agda
/home/joey/.local/bin/agda
And I've set the environment variable for my Agda directory:
> echo $AGDA_DIR
/home/joey/.agda
Which is populated with the correct files:
/home/joey/agda/agda-stdlib/standard-library.agda-lib
> cat "$AGDA_DIR"/libraries
/home/joey/agda/agda-stdlib/standard-library.agda-lib
> cat "$AGDA_DIR"/defaults
standard-library
> cat /home/joey/agda/agda-stdlib/standard-library.agda-lib
name: standard-library
include: src
However, when I go to compile an Agda file, I get the following error:
Failed to find source of module Function in any of the following
locations:
/home/joey/agda/AutoInAgda/src/Function.agda
/home/joey/agda/AutoInAgda/src/Function.lagda
/home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.agda
/home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.lagda
when scope checking the declaration
open import Function
How can I tell Agda where to look for the standard library? Is this a problem because of Stack?
I'm on Ubuntu 17.10, if that makes a difference.
It turns out that if you have a .agda-lib file in your root directory, it will completely ignore the defaults file. So the key was to include standard-library explicitly in that file.
A dumb thing for me to miss, but hopefully others with the same problem will find this answer.