6

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.

jmite
  • 8,171
  • 6
  • 40
  • 81
  • What happens if you pass explicitly `--library=standard-library` as a command-line option? – gallais Oct 30 '17 at 09:21
  • @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 Oct 31 '17 at 20:11
  • 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 Oct 31 '17 at 21:09
  • 1
    @gallais Thanks for the help, turns out it was a stupid mistake – jmite Oct 31 '17 at 21:45

2 Answers2

6

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.

jmite
  • 8,171
  • 6
  • 40
  • 81
1

For anyone else having this issue, this is solved by adding the following line to your .agda-lib file:

depend: standard-library
Fredrik Bakke
  • 31
  • 7