errors on loading the simplest agda source files
Task Info (Flyspray) | |
---|---|
Opened By | Marko Schütz-Schmuck (okram) |
Task ID | 61904 |
Type | Bug Report |
Project | Community Packages |
Category | Packages |
Version | None |
OS | All |
Opened | 2019-03-03 14:51:35 UTC |
Status | Assigned |
Assignee | Felix Yan (felixonmars) |
Details
Description: 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 2.5.99.20190207-5 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/Data/Nat/Base.agda:9,1-29 /usr/share/agda/lib/stdlib/Level.agdai: removeLink: permission denied (Permission denied)