Community Packages

Please read this before reporting a bug:

Do NOT report bugs when a package is just outdated, or it is in the AUR. Use the 'flag out of date' link on the package page, or the Mailing List.

REPEAT: Do NOT report bugs for outdated packages!

FS#56637 - [agda-stdlib] Cannot be used as a dependency with the AGDA packaging system

Attached to Project: Community Packages
Opened by William John Gowers (johngowers) - Friday, 08 December 2017, 17:38 GMT
Last edited by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:28 GMT
Task Type Bug Report
Category Packages
Status Closed
Assigned To Felix Yan (felixonmars)
Architecture All
Severity Low
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 1
Private No



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
$ cat >> ~/.agda/defaults

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.
This task depends upon

Closed by  Felix Yan (felixonmars)
Friday, 31 July 2020, 07:28 GMT
Reason for closing:  Fixed
Comment by Fabian (bafain) - Tuesday, 13 February 2018, 10:20 GMT Comment by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:28 GMT
I believe it's implemented in latest agda-stdlib. Please reopen if it's still an issue, thanks!