Agda: Can't find std-lib when installing with Stack

Question

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.

What happens if you pass explicitly --library=standard-library as a command-line option? — gallais
@gallais When I add that, I get an error: The name of the top level module does not match the file name. The module Auto should be defined in one of the following files: /home/joey/agda/agda-stdlib/src/Auto.agda . It looks like it's trying to treat my project as the standard library, instead of using the standard library — jmite
Oh but now it seems to know about the location of standard-library which is good! I'd guess that throwing in an additional -i . (if Auto.agda is indeed at the root of the project) should make it work. I don't know what the problem with the defaults are but you may want to rename ~/.agda/libraries to ~/.agda/libraries-VERSIONNUMBER. — gallais
@gallais Thanks for the help, turns out it was a stupid mistake — jmite

jmite jmite · Accepted Answer · 2017-10-31T21:15:14

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.

Agda: Can't find std-lib when installing with Stack

1 Answers