Community Packages

Please read this before reporting a bug:

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

REPEAT: Do NOT report bugs for outdated packages!

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
Task Type Bug Report
Category Packages
Status Closed
Assigned To Felix Yan (felixonmars)
Architecture x86_64
Severity High
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 3
Private No



Agda is failing to check any file.

Additional info:
* package version:

Steps to reproduce:

$ touch empty.agda
$ agda empty.agda
/usr/share/agda/lib/_build: createDirectory: permission denied
(Permission denied)
This task depends upon

Closed by  freswa (frederik)
Sunday, 11 October 2020, 15:00 GMT
Reason for closing:  No response
Comment by Konstantin Nisht (knisht) - Saturday, 29 February 2020, 21:46 GMT
I have the same issue.

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.
Comment by Catalin Hritcu (catalin_hritcu) - Monday, 06 April 2020, 14:09 GMT
@Konstantin: This still fails for me with agda 2.6.1-12 and agda-stdlib 1.3-1:
/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?
Comment by Konstantin Nisht (knisht) - Monday, 06 April 2020, 14:33 GMT
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.
Comment by Catalin Hritcu (catalin_hritcu) - Monday, 06 April 2020, 14:40 GMT
@Konstantin: Your chown command helped, thank you. Not sure it's good security-wise, but I'm on a single-user laptop, so I don't care that much.
Comment by Catalin Hritcu (catalin_hritcu) - Monday, 06 April 2020, 16:01 GMT
And this similar to another open bug report, by the way:
Comment by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:26 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
$ cat .agda/defaults