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#61904 - [agda] errors on loading the simplest agda source files

Attached to Project: Community Packages
Opened by Marko Schütz-Schmuck (okram) - Sunday, 03 March 2019, 14:51 GMT
Last edited by Balló György (City-busz) - Monday, 18 March 2019, 08:05 GMT
Task Type Bug Report
Category Packages
Status Assigned
Assigned To Felix Yan (felixonmars)
Architecture All
Severity High
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 0%
Votes 0
Private No


After a recent upgrade of agda and agda-stdlib, I am now getting errors on loading the simplest agda source files.

Additional info:
* versions:
agda-stdlib 0.17-1

Steps to reproduce:
- enter a file in emacs with

module ex01 where

open import Data.Nat

in it.
- save as ex01.agda
- try to load it into agda with C-c C-l
- an error occurs

/usr/share/agda/lib/stdlib/Level.agdai: removeLink: permission denied (Permission denied)
This task depends upon

Comment by Marko Schütz-Schmuck (okram) - Sunday, 03 March 2019, 15:02 GMT
oops, where can I edit?
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
$ cat .agda/defaults