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
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
|
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
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
https://bugs.archlinux.org/task/67470
Also thanks for pointing out the need for the configuration files. These I had.