FS#67354 - [agda-stdlib] library files not usable

Attached to Project: Community Packages
Opened by Felix E. Klee (feklee) - Wednesday, 22 July 2020, 09:17 GMT
Last edited by freswa (frederik) - Sunday, 11 October 2020, 14:53 GMT
Task Type Bug Report
Category Packages
Status Closed
Assigned To Felix Yan (felixonmars)
Architecture All
Severity High
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 0
Private No

Details

Description:

The library files are not compiled. Therefore they cannot be used.

Additional info:

* package version(s): 1.3-1

Steps to reproduce:

1. Create `/tmp/hello-world.agda`:

https://agda.readthedocs.io/en/v2.6.0.1/getting-started/hello-world.html

2. Run `agda --compile hello-world.agda` or `agda --local-interfaces
--compile draft.agda`. I get permission denied for directories under
`/usr`. This is because stdlib is not compiled with the installed
version of Agda.
This task depends upon

Closed by  freswa (frederik)
Sunday, 11 October 2020, 14:53 GMT
Reason for closing:  Fixed
Comment by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:20 GMT
Please try again with:

agda >= 2.6.1-68
agda-stdlib >= 1.3-2

Note that according to agda-stdlib's library management system you'll need the following configurations:

$ cat .agda/libraries
/usr/share/agda/lib/standard-library.agda-lib
$ cat .agda/defaults
standard-library
Comment by Felix E. Klee (feklee) - Monday, 03 August 2020, 04:07 GMT
Thanks, it now works, asides from another issue:

https://bugs.archlinux.org/task/67470

Also thanks for pointing out the need for the configuration files. These I had.

Loading...