Arch Linux

Description:

Since version 2.5+, AGDA has used a new packaging system in which an AGDA repository can be made into a package by adding a file with the extension .agda-lib to the root directory.

The upstream vesion of agda-stdlib provides such a file (standard-library.agda-lib) for use with the standard library, but the Arch package ignores this file and only copies the source files into the system directory. This works fine until you try to use the packaging system to include different packages, at which point AGDA claims that it cannot find the standard library.

(The problem arises if a library has a dependency on the standard library. In that case, AGDA needs the standard library to be installed using the packaging system in order to find it.)

Workaround (the fix should be along these lines):

# cat >/usr/share/agda/lib/prim/standard-library.agda-lib
name: standard-library
include: .
$ cat >> ~/.agda/libraries
/usr/share/agda/lib/prim/standard-library.agda-lib
$ cat >> ~/.agda/defaults
standard-library

Additional info:
* arch-stdlib 0.14-1


Steps to reproduce:

1. Create a file, test.agda-lib, with the following contents:

name: test-library
depend: standard-library
include: .

2. Edit ~/.agda/libraries, inserting the full path to test.agda-lib as a line in the file.

3. Run the command
$ agda -l test-library Dummy.agda

3a. Alternatively, add the line 'test-library' to ~/.agda/defaults, then open any AGDA file in Emacs-mode and try to type check it.