Package: agda-stdlib
Version: 1.7.3-1
Severity: serious
When using the agda command to verify .agda, which uses the agda-stdlib package,
it tries to write to the library directory, resulting in a `permission
denied` error.
Here is information on related packages:
```
% dpkg --no-pager -l emacs-lucid emacs-el agda agda-bin agda-stdlib
agda-stdlib-doc elpa-agda2-mode libghc-agda-dev
Desired=Unknown/Install/Remove/Purge/Hold
| Status=Not/Inst/Conf-files/Unpacked/halF-conf/Half-inst/trig-aWait/Trig-pend
|/ Err?=(none)/Reinst-required (Status,Err: uppercase=bad)
||/ Name Version Architecture Description
+++-===============-============-============-================================================================
ii agda 2.6.3-1 all dependently typed
functional programming language
ii agda-bin 2.6.3-1+b3 amd64 commandline interface to Agda
ii agda-stdlib 1.7.3-1 all standard library for Agda
ii agda-stdlib-doc 1.7.3-1 all standard library for
Agda — documentation
ii elpa-agda2-mode 2.6.3-1 all dependently typed
functional programming language — emacs mode
ii emacs-el 1:29.4+1-3 all GNU Emacs LISP (.el) files
ii emacs-lucid 1:29.4+1-3 amd64 GNU Emacs editor (with
Lucid GUI support)
ii libghc-agda-dev 2.6.3-1+b3 amd64 dependently typed
functional programming language
```
Here are the steps to reproduce the problem:
```
% cat foo.agda
open import Data.Nat
```
```
% agda -i. -i/usr/share/agda-stdlib foo.agda
Checking foo (/home/hibi/src/agda/foo.agda).
Checking Data.Nat (/usr/share/agda-stdlib/Data/Nat.agda).
Checking Data.Nat.Base (/usr/share/agda-stdlib/Data/Nat/Base.agda).
Checking Data.Bool.Base (/usr/share/agda-stdlib/Data/Bool/Base.agda).
Checking Data.Unit.Base (/usr/share/agda-stdlib/Data/Unit/Base.agda).
Failed to write interface /usr/share/agda-stdlib/Data/Unit/Base.agdai.
/usr/share/agda-stdlib/Data/Bool/Base.agda:11,1-37
/usr/share/agda-stdlib/Data/Unit/Base.agdai: removeLink: permission
denied (Permission denied)
```
open foo.agda in emacs, and `C-c C-l` gives errors like below in emacs
*Error* buffer:
```
/usr/share/agda-stdlib/Data/Bool/Base.agda:11,1-37
/usr/share/agda-stdlib/Data/Unit/Base.agdai: removeLink: permission
denied (Permission denied)
```
--
Kei Hibino
[email protected]
