Package: agda-stdlib
Version: 2.1-1
Severity: important
When using agda2-mode to verify .agda files that use agda-stdlib,
it fails to load the library modules.
Here is information on related packages:
```
% env LANGUAGE=C dpkg --no-pager -l emacs-lucid emacs-el agda
agda-bin agda-stdlib elpa-agda2-mode
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.4.3-1 all dependently typed
functional programming language
ii agda-bin 2.6.4.3-1 amd64 commandline interface to Agda
ii agda-stdlib 2.1-1 all standard library for Agda
ii elpa-agda2-mode 2.6.4.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)
```
Here are the steps to reproduce the problem:
```
% cat foo.agda
open import Data.Nat
```
open foo.agda in emacs, and `C-c C-l` gives errors like below in emacs
*Error* buffer:
```
/home/hibi/src/agda/debian-bug/foo.agda:1,1-21
Failed to find source of module Data.Nat in any of the following
locations:
/home/hibi/src/agda/debian-bug/Data/Nat.agda
/home/hibi/src/agda/debian-bug/Data/Nat.lagda
/usr/share/agda-stdlib/Data/Nat.agda
/usr/share/agda-stdlib/Data/Nat.lagda
/usr/share/libghc-agda-dev/lib/prim/Data/Nat.agda
/usr/share/libghc-agda-dev/lib/prim/Data/Nat.lagda
when scope checking the declaration
open import Data.Nat
```
I have confirmed that the following patch resolves the issue:
```
--- debian/60agda-stdlib.el.old 2022-08-07 01:32:51.000000000 +0900
+++ debian/60agda-stdlib.el 2024-10-23 15:13:04.296257932 +0900
@@ -2,4 +2,4 @@
;; variable in his/her own session. But that is probably the intended behaviour
;; anyway.
-(setq agda2-program-args '("-i." "-i/usr/share/agda-stdlib"))
+(setq agda2-program-args '("-i." "-i/usr/share/agda-stdlib/src"))
```
--
Kei Hibino
ex8k.hib...@gmail.com
