FS#65489 - [agda] Fails to check a file
Attached to Project:
Community Packages
Opened by Elkin (helq) - Thursday, 13 February 2020, 20:16 GMT
Last edited by freswa (frederik) - Sunday, 11 October 2020, 15:00 GMT
Opened by Elkin (helq) - Thursday, 13 February 2020, 20:16 GMT
Last edited by freswa (frederik) - Sunday, 11 October 2020, 15:00 GMT
|
Details
Description:
Agda is failing to check any file. Additional info: * package version: 2.6.0.1.20191219-9 Steps to reproduce: $ touch empty.agda $ agda empty.agda /usr/share/agda/lib/_build: createDirectory: permission denied (Permission denied) |
This task depends upon
Here is the line that helped me:
$ sudo rm -rf /usr/share/agda/lib/_build
It followed by complete recheck of agda standard library, and then everything worked fine.
/usr/share/agda/lib/_build: createDirectory: permission denied
(Permission denied)
Tried your rm command, but I'm a complete noob (never installed agda before) so didn't know how to do a "complete recheck of agda standard library". Can you advise please?
Linux somehow sets wrong access permission to agda lib dir, and thats why agda can't create temporary directory for built source code.
So I suggest you to change owner for this lib dir by the following command (I double checked, this one should work):
$ sudo chown -R $USER /usr/share/agda/lib
By complete recheck I mean that agda will compile all standard library source code. It will be done automatically at your first attempt to check some agda file, for example, when you type commands from this ticket description.
https://bugs.archlinux.org/task/61904
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