Bug#1085873: Fail to load agda-stdlib modules from agda2-mode

[Kei Hibino]

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.hibino at gmail.com